chore: use grw, gcongr even more (#30632)

Also delete a redundant instance.

Author: YaelDillies

Archive/Imo/Imo1982Q1.lean

@@ -114,7 +114,7 @@ lemma imo1982_q1 {f : ℕ+ → ℕ} (hf : IsGood f) : f 1982 = 660 := by
   suffices h : 3334 ≤ 3333 by simp at h
   calc
     3334 = 5 * f 1982 + 29 * f 3 + f 2 := by rw [hf.f₃, hf.f₂, hr, add_zero, mul_one]
-    (5 : ℕ+) * f 1982 + (29 : ℕ+) * f 3 + f 2 ≤ f (5 * 1982 + 29 * 3) + f 2 :=
-      add_le_add_right hf.superlinear _
+    (5 : ℕ+) * f 1982 + (29 : ℕ+) * f 3 + f 2 ≤ f (5 * 1982 + 29 * 3) + f 2 := by
+      grw [hf.superlinear]
     _ ≤ f (5 * 1982 + 29 * 3 + 2) := hf.superadditive
     _ = 3333 := hf.f_9999

Archive/Imo/Imo2013Q5.lean

@@ -178,7 +178,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
       calc
         ↑(pn + 2) * f x = (↑pn + 1 + 1) * f x := by norm_cast
         _ = (↑pn + 1) * f x + f x := by ring
-        _ ≤ f (↑pn.succ * x) + f x := mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
+        _ ≤ f (↑pn.succ * x) + f x := by norm_cast; grw [hpn pn.succ_pos]
         _ ≤ f ((↑pn + 1) * x + x) := by exact_mod_cast H2 _ _ (mul_pos pn.cast_add_one_pos hx) hx
         _ = f ((↑pn + 1 + 1) * x) := by ring_nf
         _ = f (↑(pn + 2) * x) := by norm_cast

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -184,12 +184,8 @@ lemma apply_nat_le_self [IsOrderedRing S] (n : ℕ) : abv n ≤ n := by
   · simp [Subsingleton.eq_zero (n : R)]
   induction n with
   | zero => simp
-  | succ n hn =>
-    simp only [Nat.cast_succ]
-    calc
-      abv (n + 1) ≤ abv n + abv 1 := abv.add_le ..
-      _ = abv n + 1 := congrArg (abv n + ·) abv.map_one
-      _ ≤ n + 1 := add_le_add_right hn 1
+  | succ n ih =>
+  · grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]
 
 end IsDomain
 

Mathlib/Algebra/Order/GroupWithZero/WithZero.lean

@@ -32,22 +32,22 @@ instance {α : Type*} [Mul α] [Preorder α] [MulLeftStrictMono α] :
     PosMulStrictMono (WithZero α) where
   mul_lt_mul_of_pos_left
   | (x : α), hx, 0, (b : α), _ => by simpa only [mul_zero] using WithZero.zero_lt_coe _
-  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; exact mul_lt_mul_left' h x
+  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; gcongr
 
 open Function in
 instance {α : Type*} [Mul α] [Preorder α] [MulRightStrictMono α] :
     MulPosStrictMono (WithZero α) where
   mul_lt_mul_of_pos_right
   | (x : α), hx, 0, (b : α), _ => by simpa only [mul_zero] using WithZero.zero_lt_coe _
-  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; exact mul_lt_mul_right' h x
+  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; gcongr
 
 instance {α : Type*} [Mul α] [Preorder α] [MulLeftMono α] :
     PosMulMono (WithZero α) where
   mul_le_mul_of_nonneg_left
   | 0, _, a, b, _ => by simp
   | (x : α), _, 0, _, _ => by simp
   | (x : α), _, (a : α), 0, h => by simp at h
-  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; exact mul_le_mul_left' h x
+  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; gcongr
 
 -- This makes `lt_mul_of_le_of_one_lt'` work on `ℤᵐ⁰`
 open Function in
@@ -57,7 +57,7 @@ instance {α : Type*} [Mul α] [Preorder α] [MulRightMono α] :
   | 0, _, a, b, _ => by simp
   | (x : α), _, 0, _, _ => by simp
   | (x : α), _, (a : α), 0, h => by simp at h
-  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; exact mul_le_mul_right' h x
+  | (x : α), hx, (a : α), (b : α), h => by norm_cast at h ⊢; gcongr
 
 section Units
 

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -86,12 +86,12 @@ theorem degree_list_sum_le (l : List S[X]) : degree l.sum ≤ (l.map natDegree).
 theorem natDegree_list_prod_le (l : List S[X]) : natDegree l.prod ≤ (l.map natDegree).sum := by
   induction l with
   | nil => simp
-  | cons hd tl IH => simpa using natDegree_mul_le.trans (add_le_add_left IH _)
+  | cons p l ih => dsimp; grw [natDegree_mul_le, ih]
 
 theorem degree_list_prod_le (l : List S[X]) : degree l.prod ≤ (l.map degree).sum := by
   induction l with
   | nil => simp
-  | cons hd tl IH => simpa using (degree_mul_le _ _).trans (add_le_add_left IH _)
+  | cons p l ih => dsimp; grw [degree_mul_le, ih]
 
 theorem coeff_list_prod_of_natDegree_le (l : List S[X]) (n : ℕ) (hl : ∀ p ∈ l, natDegree p ≤ n) :
     coeff (List.prod l) (l.length * n) = (l.map fun p => coeff p n).prod := by

Mathlib/Algebra/Polynomial/Degree/Definitions.lean

@@ -479,9 +479,7 @@ natDegree_mul_le.trans <| add_le_add ‹_› ‹_›
 theorem natDegree_pow_le {p : R[X]} {n : ℕ} : (p ^ n).natDegree ≤ n * p.natDegree := by
   induction n with
   | zero => simp
-  | succ i hi =>
-    rw [pow_succ, Nat.succ_mul]
-    apply le_trans natDegree_mul_le (add_le_add_right hi _)
+  | succ n ih => grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]
 
 theorem natDegree_pow_le_of_le (n : ℕ) (hp : natDegree p ≤ m) :
     natDegree (p ^ n) ≤ n * m :=

Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

@@ -704,11 +704,6 @@ variable {G : Type*} [NormedAddCommGroup G]
 theorem coeFn_le [PartialOrder G] (f g : Lp.simpleFunc G p μ) : (f : α → G) ≤ᵐ[μ] g ↔ f ≤ g := by
   rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]
 
-instance instAddLeftMono [PartialOrder G] [IsOrderedAddMonoid G] :
-    AddLeftMono (Lp.simpleFunc G p μ) := by
-  refine ⟨fun f g₁ g₂ hg₁₂ => ?_⟩
-  exact add_le_add_left hg₁₂ f
-
 variable (p μ G)
 
 theorem coeFn_zero : (0 : Lp.simpleFunc G p μ) =ᵐ[μ] (0 : α → G) :=

Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean

@@ -106,8 +106,8 @@ theorem sum_trapezoidal_error_adjacent_intervals {f : ℝ → ℝ} {N : ℕ} {a
     suffices ∀ {k : ℕ}, k ≤ N → a + k * h ∈ [[a, a + N * h]] from
       IntervalIntegrable.mono h_f_int (Set.uIcc_subset_uIcc (this hk.le) (this hk)) le_rfl
     rcases le_total h 0 with h_neg | h_pos <;> intro k hk <;> rw [← Nat.cast_le (α := ℝ)] at hk
-    · exact Set.mem_uIcc_of_ge (add_le_add_left (mul_le_mul_of_nonpos_right hk h_neg) a)
-        (add_le_of_nonpos_right (mul_nonpos_of_nonneg_of_nonpos k.cast_nonneg h_neg))
+    · simpa [Set.mem_uIcc] using .inr
+        ⟨mul_le_mul_of_nonpos_right hk h_neg, mul_nonpos_of_nonneg_of_nonpos k.cast_nonneg h_neg⟩
     · exact Set.mem_uIcc_of_le (le_add_of_nonneg_right (by positivity)) (by grw [hk])
 
 /-- The most basic case possible: two ordered points, with N = 1. This lemma is used in the proof of

Mathlib/RingTheory/PowerSeries/Order.lean

@@ -184,10 +184,7 @@ theorem le_order_mul (φ ψ : R⟦X⟧) : order φ + order ψ ≤ order (φ * ψ
 theorem le_order_pow (φ : R⟦X⟧) (n : ℕ) : n • order φ ≤ order (φ ^ n) := by
   induction n with
   | zero => simp
-  | succ n hn =>
-    simp only [add_smul, one_smul, pow_succ]
-    apply le_trans _ (le_order_mul _ _)
-    exact add_le_add_right hn φ.order
+  | succ n ih => grw [add_smul, one_smul, pow_succ, ih, le_order_mul]
 
 theorem le_order_prod {R : Type*} [CommSemiring R] {ι : Type*} (φ : ι → R⟦X⟧) (s : Finset ι) :
     ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order := by

Mathlib/SetTheory/Ordinal/NaturalOps.lean

@@ -531,11 +531,13 @@ theorem nmul_lt_nmul_of_pos_left (h₁ : a < b) (h₂ : 0 < c) : c ⨳ a < c ⨳
 theorem nmul_lt_nmul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a ⨳ c < b ⨳ c :=
   lt_nmul_iff.2 ⟨a, h₁, 0, h₂, by simp⟩
 
+@[gcongr]
 theorem nmul_le_nmul_left (h : a ≤ b) (c) : c ⨳ a ≤ c ⨳ b := by
   rcases lt_or_eq_of_le h with (h₁ | rfl) <;> rcases (eq_zero_or_pos c).symm with (h₂ | rfl)
   · exact (nmul_lt_nmul_of_pos_left h₁ h₂).le
   all_goals simp
 
+@[gcongr]
 theorem nmul_le_nmul_right (h : a ≤ b) (c) : a ⨳ c ≤ b ⨳ c := by
   rw [nmul_comm, nmul_comm b]
   exact nmul_le_nmul_left h c
@@ -727,7 +729,7 @@ theorem mul_le_nmul (a b : Ordinal.{u}) : a * b ≤ a ⨳ b := by
     rcases eq_zero_or_pos a with (rfl | ha)
     · simp
     · rw [(isNormal_mul_right ha).apply_of_isSuccLimit hc, Ordinal.iSup_le_iff]
-      rintro ⟨i, hi⟩
-      exact (H i hi).trans (nmul_le_nmul_left hi.le a)
+      rintro ⟨i, (hi : i < c)⟩
+      grw [H i hi, hi]
 
 end Ordinal