fix: improve the Lean.Grind.OrderedAdd instance (leanprover-community#35563)

This PR makes changes the entry point of the `grind` class `Lean.Grind.OrderedAdd` to be `IsOrderedCancelAddMonoid`, rather than the more granular type classes `AddRightMono` and `AddRightReflectLE`. Note that the doc-strings of these type classes explicitly say not to use them. This should improve `grind` performance.

See [#general > grind failure/performance issue: timing out on slow instance](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/grind.20failure.2Fperformance.20issue.3A.20timing.20out.20on.20slow.20instance/with/574912682)

Author: JovanGerb

Mathlib/Algebra/Order/Monoid/Defs.lean

@@ -66,6 +66,12 @@ class IsOrderedCancelMonoid (α : Type*) [CommMonoid α] [PartialOrder α] exten
   protected le_of_mul_le_mul_right : ∀ a b c : α, b * a ≤ c * a → b ≤ c := fun a b c h ↦ by
     rw [mul_comm _ a, mul_comm _ a] at h; exact le_of_mul_le_mul_left a b c h
 
+instance [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] :
+    Lean.Grind.OrderedAdd α where
+  add_le_left_iff {a b} c := ⟨
+    fun h ↦ IsOrderedAddMonoid.add_le_add_left a b h c,
+    IsOrderedCancelAddMonoid.le_of_add_le_add_right c a b⟩
+
 section IsOrderedCancelMonoid
 variable [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α]
 

Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean

@@ -257,10 +257,6 @@ abbrev AddRightReflectLE [Add M] [LE M] : Prop :=
 
 attribute [to_additive existing] MulLeftReflectLE MulRightReflectLE
 
-instance [Add M] [Preorder M] [i₁ : AddRightMono M] [i₂ : AddRightReflectLE M] :
-    Lean.Grind.OrderedAdd M where
-  add_le_left_iff := fun c => ⟨i₁.elim c, i₂.elim c⟩
-
 theorem rel_iff_cov [CovariantClass M N μ r] [ContravariantClass M N μ r] (m : M) {a b : N} :
     r (μ m a) (μ m b) ↔ r a b :=
   ⟨ContravariantClass.elim _, CovariantClass.elim _⟩

Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

@@ -675,14 +675,14 @@ lemma Integrable.measure_ge_lt_top {f : α → β} [Lattice β] [HasSolidNorm β
     μ {a : α | ε ≤ f a} < ∞ :=
   lt_of_le_of_lt (measure_mono fun x hx => norm_le_norm_of_abs_le_abs <|
     (abs_of_nonneg ε_pos.le).symm ▸ hx.trans (le_abs_self (f x)))
-    (hf.measure_norm_ge_lt_top (by simp; grind))
+    (hf.measure_norm_ge_lt_top (by positivity [ε_pos.ne']))
 
 /-- If `f` is integrable, then for any `c < 0` the set `{x | f x ≤ c}` has finite
 measure. -/
 lemma Integrable.measure_le_lt_top {f : α → β} [Lattice β] [HasSolidNorm β] [AddLeftMono β]
     (hf : Integrable f μ) {c : β} (c_neg : c < 0) :
     μ {a : α | f a ≤ c} < ∞ := by
-  have : 0 < ‖c‖ := by simp; grind
+  have : 0 < ‖c‖ := by positivity [c_neg.ne]
   refine lt_of_le_of_lt (measure_mono fun x hx => ?_) (hf.measure_norm_ge_lt_top this)
   have : -c ≤ -f x := by simp; grind
   exact norm_le_norm_of_abs_le_abs <| abs_of_nonpos c_neg.le ▸ this.trans (neg_le_abs _)