diff --git a/Mathlib/Algebra/Order/SMul.lean b/Mathlib/Algebra/Order/SMul.lean
index 8ff6632e74aab..c603e62fc7833 100644
--- a/Mathlib/Algebra/Order/SMul.lean
+++ b/Mathlib/Algebra/Order/SMul.lean
@@ -13,6 +13,7 @@ import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.Order.Monoid.Prod
 import Mathlib.Algebra.Order.Pi
 import Mathlib.Data.Set.Pointwise.SMul
+import Mathlib.Tactic.GCongr.Core
 import Mathlib.Tactic.Positivity
 
 /-!
@@ -88,11 +89,11 @@ section OrderedSMul
 variable [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M] [OrderedSMul R M]
   {s : Set M} {a b : M} {c : R}
 
-theorem smul_lt_smul_of_pos : a < b → 0 < c → c • a < c • b :=
+@[gcongr] theorem smul_lt_smul_of_pos : a < b → 0 < c → c • a < c • b :=
   OrderedSMul.smul_lt_smul_of_pos
 #align smul_lt_smul_of_pos smul_lt_smul_of_pos
 
-theorem smul_le_smul_of_nonneg (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c • a ≤ c • b := by
+@[gcongr] theorem smul_le_smul_of_nonneg (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c • a ≤ c • b := by
   rcases h₁.eq_or_lt with (rfl | hab)
   · rfl
   · rcases h₂.eq_or_lt with (rfl | hc)
diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
index 6b46eb08a0643..c547617dcbb37 100644
--- a/Mathlib/Analysis/Analytic/Basic.lean
+++ b/Mathlib/Analysis/Analytic/Basic.lean
@@ -206,7 +206,7 @@ theorem isLittleO_of_lt_radius (h : ↑r < p.radius) :
   calc
     |‖p n‖ * (r : ℝ) ^ n| = ‖p n‖ * (t : ℝ) ^ n * (r / t : ℝ) ^ n := by
       field_simp [mul_right_comm, abs_mul, this.ne']
-    _ ≤ C * (r / t : ℝ) ^ n := mul_le_mul_of_nonneg_right (hC n) (pow_nonneg (div_nonneg r.2 t.2) _)
+    _ ≤ C * (r / t : ℝ) ^ n := by gcongr; apply hC
 #align formal_multilinear_series.is_o_of_lt_radius FormalMultilinearSeries.isLittleO_of_lt_radius
 
 /-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ = o(1)`. -/
@@ -665,16 +665,16 @@ theorem HasFPowerSeriesOnBall.uniform_geometric_approx' {r' : ℝ≥0}
     mul_le_of_le_one_right ha.1.le (div_le_one_of_le yr'.le r'.coe_nonneg)
   suffices ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / r')) ^ n / (1 - a * (‖y‖ / r')) by
     refine' this.trans _
-    apply_rules [div_le_div_of_le_left, sub_pos.2, div_nonneg, mul_nonneg, pow_nonneg, hC.lt.le,
-        ha.1.le, norm_nonneg, NNReal.coe_nonneg, ha.2, (sub_le_sub_iff_left _).2]
+    have : 0 < a := ha.1
+    gcongr
+    apply_rules [sub_pos.2, ha.2]
   apply norm_sub_le_of_geometric_bound_of_hasSum (ya.trans_lt ha.2) _ (hf.hasSum this)
   intro n
   calc
     ‖(p n) fun _ : Fin n => y‖
     _ ≤ ‖p n‖ * ∏ _i : Fin n, ‖y‖ := ContinuousMultilinearMap.le_op_norm _ _
     _ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by field_simp [hr'0.ne', mul_right_comm]
-    _ ≤ C * a ^ n * (‖y‖ / r') ^ n :=
-      (mul_le_mul_of_nonneg_right (hp n) (pow_nonneg (div_nonneg (norm_nonneg _) r'.coe_nonneg) _))
+    _ ≤ C * a ^ n * (‖y‖ / r') ^ n := by gcongr ?_ * _; apply hp
     _ ≤ C * (a * (‖y‖ / r')) ^ n := by rw [mul_pow, mul_assoc]
 #align has_fpower_series_on_ball.uniform_geometric_approx' HasFPowerSeriesOnBall.uniform_geometric_approx'
 
@@ -689,7 +689,7 @@ theorem HasFPowerSeriesOnBall.uniform_geometric_approx {r' : ℝ≥0}
     hf.uniform_geometric_approx' h
   refine' ⟨a, ha, C, hC, fun y hy n => (hp y hy n).trans _⟩
   have yr' : ‖y‖ < r' := by rwa [ball_zero_eq] at hy
-  refine' mul_le_mul_of_nonneg_left (pow_le_pow_of_le_left _ _ _) hC.lt.le
+  gcongr
   exacts [mul_nonneg ha.1.le (div_nonneg (norm_nonneg y) r'.coe_nonneg),
     mul_le_of_le_one_right ha.1.le (div_le_one_of_le yr'.le r'.coe_nonneg)]
 #align has_fpower_series_on_ball.uniform_geometric_approx HasFPowerSeriesOnBall.uniform_geometric_approx
@@ -752,10 +752,12 @@ theorem HasFPowerSeriesOnBall.isBigO_image_sub_image_sub_deriv_principal
           ring
         -- porting note: the two `↑` in `↑r'` are new, without them, Lean fails to synthesize
         -- instances `HDiv ℝ ℝ≥0 ?m` or `HMul ℝ ℝ≥0 ?m`
-        _ ≤ C * a ^ (n + 2) / ↑r' ^ (n + 2) * ↑r' ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) :=
-          by apply_rules [mul_le_mul_of_nonneg_right, mul_le_mul, hp, pow_le_pow_of_le_left, hy'.le,
-            norm_nonneg, pow_nonneg, div_nonneg, mul_nonneg, Nat.cast_nonneg, hC.le, r'.coe_nonneg,
-            ha.1.le]
+        _ ≤ C * a ^ (n + 2) / ↑r' ^ (n + 2)
+            * ↑r' ^ n * (↑(n + 2) * ‖y - (x, x)‖ * ‖y.1 - y.2‖) := by
+          have : 0 < a := ha.1
+          gcongr
+          · apply hp
+          · apply hy'.le
         _ = B n := by
           -- porting note: in the original, `B` was in the `field_simp`, but now Lean does not
           -- accept it. The current proof works in Lean 4, but does not in Lean 3.
@@ -971,8 +973,7 @@ theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {n : ℕ} {p :
         simpa only [inv_smul_smul₀ (norm_pos_iff.mp k_pos), norm_smul, Finset.prod_const,
           Finset.card_fin] using
           congr_arg norm (p.map_smul_univ (fun _ : Fin n.succ => k⁻¹) fun _ : Fin n.succ => k • y)
-      _ ≤ ‖k⁻¹ ^ n.succ‖ * (‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))) :=
-        (mul_le_mul_of_nonneg_left h₂ (norm_nonneg _))
+      _ ≤ ‖k⁻¹ ^ n.succ‖ * (‖k‖ ^ n.succ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1)))) := by gcongr
       _ = ‖(k⁻¹ * k) ^ n.succ‖ * (‖k‖ * (c * ‖y‖ ^ (n.succ + 1))) := by
         rw [← mul_assoc]
         simp [norm_mul, mul_pow]
diff --git a/Mathlib/Analysis/Calculus/FDerivMeasurable.lean b/Mathlib/Analysis/Calculus/FDerivMeasurable.lean
index cf509d553d104..1d57711ae08fd 100644
--- a/Mathlib/Analysis/Calculus/FDerivMeasurable.lean
+++ b/Mathlib/Analysis/Calculus/FDerivMeasurable.lean
@@ -179,10 +179,7 @@ theorem mem_a_of_differentiable {ε : ℝ} (hε : 0 < ε) {x : E} (hx : Differen
       (norm_sub_le _ _)
     _ ≤ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ :=
       (add_le_add (hR _ (lt_trans (mem_ball.1 hz) hr.2)) (hR _ (lt_trans (mem_ball.1 hy) hr.2)))
-    _ ≤ ε / 2 * r + ε / 2 * r :=
-      (add_le_add
-        (mul_le_mul_of_nonneg_left (le_of_lt (mem_ball_iff_norm.1 hz)) (le_of_lt (half_pos hε)))
-        (mul_le_mul_of_nonneg_left (le_of_lt (mem_ball_iff_norm.1 hy)) (le_of_lt (half_pos hε))))
+    _ ≤ ε / 2 * r + ε / 2 * r := by rw [mem_ball_iff_norm] at hz hy; gcongr
     _ = ε * r := by ring
 #align fderiv_measurable_aux.mem_A_of_differentiable FDerivMeasurableAux.mem_a_of_differentiable
 
@@ -297,8 +294,7 @@ theorem d_subset_differentiable_set {K : Set (E →L[𝕜] F)} (hK : IsComplete
     rw [dist_comm, dist_eq_norm]
     calc
       ‖L0 e - L0 e'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e := M _ _ _ _ _ _ le_rfl le_rfl le_rfl le_rfl he'
-      _ < 12 * ‖c‖ * (ε / (12 * ‖c‖)) :=
-        (mul_lt_mul' le_rfl he (le_of_lt P) (mul_pos (by norm_num) cpos))
+      _ < 12 * ‖c‖ * (ε / (12 * ‖c‖)) := by gcongr
       _ = ε := by field_simp [(by norm_num : (12 : ℝ) ≠ 0), ne_of_gt cpos] ; ring
   -- As it is Cauchy, the sequence `L0` converges, to a limit `f'` in `K`.
   obtain ⟨f', f'K, hf'⟩ : ∃ f' ∈ K, Tendsto L0 atTop (𝓝 f') :=
@@ -316,8 +312,7 @@ theorem d_subset_differentiable_set {K : Set (E →L[𝕜] F)} (hK : IsComplete
       this makes it possible to cover all scales, and thus to obtain a good linear approximation in
       the whole ball of radius `(1/2)^(n e)`. -/
     intro ε εpos
-    have pos : 0 < 4 + 12 * ‖c‖ :=
-      add_pos_of_pos_of_nonneg (by norm_num) (mul_nonneg (by norm_num) (norm_nonneg _))
+    have pos : 0 < 4 + 12 * ‖c‖ := by positivity
     obtain ⟨e, he⟩ : ∃ e : ℕ, (1 / 2) ^ e < ε / (4 + 12 * ‖c‖) :=
       exists_pow_lt_of_lt_one (div_pos εpos pos) (by norm_num)
     rw [eventually_nhds_iff_ball]
@@ -365,10 +360,7 @@ theorem d_subset_differentiable_set {K : Set (E →L[𝕜] F)} (hK : IsComplete
         (norm_add_le_of_le J2
           ((le_op_norm _ _).trans (mul_le_mul_of_nonneg_right (Lf' _ _ m_ge) (norm_nonneg _))))
       _ = (4 + 12 * ‖c‖) * ‖y‖ * (1 / 2) ^ e := by ring
-      _ ≤ (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖)) :=
-        (mul_le_mul_of_nonneg_left he.le
-          (mul_nonneg (add_nonneg (by norm_num) (mul_nonneg (by norm_num) (norm_nonneg _)))
-            (norm_nonneg _)))
+      _ ≤ (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖)) := by gcongr
       _ = ε * ‖y‖ := by field_simp [ne_of_gt pos]; ring
   rw [← this.fderiv] at f'K
   exact ⟨this.differentiableAt, f'K⟩
@@ -554,11 +546,9 @@ theorem mem_a_of_differentiable {ε : ℝ} (hε : 0 < ε) {x : ℝ}
       (add_le_add (hm ⟨hz.1, hz.2.trans_lt (by linarith [hr.2])⟩)
         (hm ⟨hy.1, hy.2.trans_lt (by linarith [hr.2])⟩))
     _ ≤ ε / 2 * r + ε / 2 * r := by
-      apply add_le_add
-      · apply mul_le_mul_of_nonneg_left _ (le_of_lt (half_pos hε))
-        rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
-      · apply mul_le_mul_of_nonneg_left _ (le_of_lt (half_pos hε))
-        rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]
+      gcongr
+      · rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
+      · rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]
     _ = ε * r := by ring
 #align right_deriv_measurable_aux.mem_A_of_differentiable RightDerivMeasurableAux.mem_a_of_differentiable
 
@@ -650,7 +640,7 @@ theorem d_subset_differentiable_set {K : Set F} (hK : IsComplete K) :
         by congr 1; abel
       _ ≤ ‖L e p q - L e p r‖ + ‖L e p r - L e' p' r‖ + ‖L e' p' r - L e' p' q'‖ :=
         (le_trans (norm_add_le _ _) (add_le_add_right (norm_add_le _ _) _))
-      _ ≤ 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e := add_le_add (add_le_add J1 J2) J3
+      _ ≤ 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e := by gcongr
         -- Porting note: proof was `by apply_rules [add_le_add]`
       _ = 12 * (1 / 2) ^ e := by ring
 
diff --git a/Mathlib/Analysis/Calculus/FDerivSymmetric.lean b/Mathlib/Analysis/Calculus/FDerivSymmetric.lean
index d40ed8e33e429..7702ea13f5259 100644
--- a/Mathlib/Analysis/Calculus/FDerivSymmetric.lean
+++ b/Mathlib/Analysis/Calculus/FDerivSymmetric.lean
@@ -136,9 +136,7 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s)
         _ = h * ‖v‖ + t * (h * ‖w‖) := by
           simp only [norm_smul, Real.norm_eq_abs, hpos.le, abs_of_nonneg, abs_mul, ht.left,
             mul_assoc]
-        _ ≤ h * ‖v‖ + 1 * (h * ‖w‖) :=
-          (add_le_add le_rfl
-            (mul_le_mul_of_nonneg_right ht.2.le (mul_nonneg hpos.le (norm_nonneg _))))
+        _ ≤ h * ‖v‖ + 1 * (h * ‖w‖) := by gcongr; exact ht.2.le
         _ = h * (‖v‖ + ‖w‖) := by ring
     calc
       ‖g' t‖ = ‖(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)‖ := by
@@ -157,10 +155,9 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s)
           exact I.trans_lt hδ
         simpa only [mem_setOf_eq, add_assoc x, add_sub_cancel'] using sδ H
       _ ≤ ε * (‖h • v‖ + ‖h • w‖) * ‖h • w‖ := by
-        apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
-        apply mul_le_mul_of_nonneg_left _ εpos.le
+        gcongr
         apply (norm_add_le _ _).trans
-        refine' add_le_add le_rfl _
+        gcongr
         simp only [norm_smul, Real.norm_eq_abs, abs_mul, abs_of_nonneg, ht.1, hpos.le, mul_assoc]
         exact mul_le_of_le_one_left (mul_nonneg hpos.le (norm_nonneg _)) ht.2.le
       _ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2 := by
diff --git a/Mathlib/Analysis/Calculus/Inverse.lean b/Mathlib/Analysis/Calculus/Inverse.lean
index 0999448fa2f16..c0309d5902e1d 100644
--- a/Mathlib/Analysis/Calculus/Inverse.lean
+++ b/Mathlib/Analysis/Calculus/Inverse.lean
@@ -201,10 +201,10 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
   · refine' ⟨b, by simp [ε0], _⟩
     have : dist y (f b) ≤ 0 :=
       (mem_closedBall.1 hy).trans (mul_nonpos_of_nonpos_of_nonneg (by linarith) ε0)
-    simp only [dist_le_zero] at this 
+    simp only [dist_le_zero] at this
     rw [this]
   have If' : (0 : ℝ) < f'symm.nnnorm := by rw [← inv_pos]; exact (NNReal.coe_nonneg _).trans_lt hc
-  have Icf' : (c : ℝ) * f'symm.nnnorm < 1 := by rwa [inv_eq_one_div, lt_div_iff If'] at hc 
+  have Icf' : (c : ℝ) * f'symm.nnnorm < 1 := by rwa [inv_eq_one_div, lt_div_iff If'] at hc
   have Jf' : (f'symm.nnnorm : ℝ) ≠ 0 := ne_of_gt If'
   have Jcf' : (1 : ℝ) - c * f'symm.nnnorm ≠ 0 := by apply ne_of_gt; linarith
   /- We have to show that `y` can be written as `f x` for some `x ∈ closed_ball b ε`.
@@ -214,7 +214,7 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
     is nonlinear, this map is not contracting (it is not even continuous), but still the proof of
     the contraction theorem holds: `uₙ = gⁿ b` is a Cauchy sequence, converging exponentially fast
     to the desired point `x`. Instead of appealing to general results, we check this by hand.
-  
+
     The main point is that `f (u n)` becomes exponentially close to `y`, and therefore
     `dist (u (n+1)) (u n)` becomes exponentally small, making it possible to get an inductive
     bound on `dist (u n) b`, from which one checks that `u n` stays in the ball on which one has a
@@ -244,7 +244,7 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
           sub_add_cancel]
       _ ≤ c * ‖z + v - z‖ := (hf _ (hε hgz) _ (hε hz))
       _ ≤ c * (f'symm.nnnorm * dist (f z) y) := by
-        apply mul_le_mul_of_nonneg_left _ (NNReal.coe_nonneg c)
+        gcongr
         simpa [dist_eq_norm'] using f'symm.bound (y - f z)
       _ = c * f'symm.nnnorm * dist (f z) y := by ring
   -- Third bound: a complicated bound on `dist w b` (that will show up in the induction) is enough
@@ -259,14 +259,15 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
           f'symm.nnnorm * dist (f b) y * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) :=
         by ring
       _ ≤ f'symm.nnnorm * dist (f b) y * 1 := by
-        apply mul_le_mul_of_nonneg_left _ (mul_nonneg (NNReal.coe_nonneg _) dist_nonneg)
+        gcongr
         rw [sub_le_self_iff]
-        exact pow_nonneg (mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _)) _
+        positivity
       _ ≤ f'symm.nnnorm * (((f'symm.nnnorm : ℝ)⁻¹ - c) * ε) := by
         rw [mul_one]
-        exact mul_le_mul_of_nonneg_left (mem_closedBall'.1 hy) (NNReal.coe_nonneg _)
+        gcongr
+        exact mem_closedBall'.1 hy
       _ = ε * (1 - c * f'symm.nnnorm) := by field_simp; ring
-      
+
   /- Main inductive control: `f (u n)` becomes exponentially close to `y`, and therefore
     `dist (u (n+1)) (u n)` becomes exponentally small, making it possible to get an inductive
     bound on `dist (u n) b`, from which one checks that `u n` remains in the ball on which we
@@ -283,8 +284,7 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
         _ ≤ f'symm.nnnorm * dist (f (u n)) y + dist (u n) b := (add_le_add (A _) le_rfl)
         _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) +
               f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) / (1 - c * f'symm.nnnorm) *
-                dist (f b) y :=
-          (add_le_add (mul_le_mul_of_nonneg_left IH.1 (NNReal.coe_nonneg _)) IH.2)
+                dist (f b) y := by gcongr; exact IH.1; exact IH.2
         _ = f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n.succ) /
               (1 - (c : ℝ) * f'symm.nnnorm) * dist (f b) y := by
           field_simp [Jcf', pow_succ]; ring
@@ -292,8 +292,9 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
     calc
       dist (f (g (u n))) y ≤ c * f'symm.nnnorm * dist (f (u n)) y :=
         B _ (C n _ IH.2) (C n.succ _ Ign)
-      _ ≤ (c : ℝ) * f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) :=
-        (mul_le_mul_of_nonneg_left IH.1 (mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _)))
+      _ ≤ (c : ℝ) * f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
+        gcongr
+        apply IH.1
       _ = ((c : ℝ) * f'symm.nnnorm) ^ n.succ * dist (f b) y := by simp only [pow_succ']; ring
   -- Deduce from the inductive bound that `uₙ` is a Cauchy sequence, therefore converging.
   have : CauchySeq u
@@ -301,8 +302,9 @@ theorem surjOn_closedBall_of_nonlinearRightInverse (hf : ApproximatesLinearOn f
     calc
       dist (u n) (u (n + 1)) = dist (g (u n)) (u n) := by rw [usucc, dist_comm]
       _ ≤ f'symm.nnnorm * dist (f (u n)) y := (A _)
-      _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) :=
-        (mul_le_mul_of_nonneg_left (D n).1 (NNReal.coe_nonneg _))
+      _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
+        gcongr
+        exact (D n).1
       _ = f'symm.nnnorm * dist (f b) y * ((c : ℝ) * f'symm.nnnorm) ^ n := by ring
   obtain ⟨x, hx⟩ : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete this
   -- As all the `uₙ` belong to the ball `closed_ball b ε`, so does their limit `x`.
@@ -434,7 +436,7 @@ theorem to_inv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Sub
       abel
     _ ≤ N * (c * ‖y' - x'‖) := (mul_le_mul_of_nonneg_left (hf _ y's _ x's) (NNReal.coe_nonneg _))
     _ ≤ N * (c * (((N⁻¹ - c)⁻¹ : ℝ≥0) * ‖A y' - A x'‖)) := by
-      apply_rules [mul_le_mul_of_nonneg_left, NNReal.coe_nonneg]
+      gcongr
       rw [← dist_eq_norm, ← dist_eq_norm]
       exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩
     _ = (N * (N⁻¹ - c)⁻¹ * c : ℝ≥0) * ‖A x' - A y'‖ := by
@@ -542,7 +544,7 @@ theorem approximates_deriv_on_nhds {f : E → F} {f' : E →L[𝕜] F} {a : E}
   · refine' ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => _⟩
     simp [@Subsingleton.elim E hE x y]
   have := hf.def hc
-  rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this 
+  rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this
   rcases this with ⟨s, has, hs⟩
   exact ⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩
 #align has_strict_fderiv_at.approximates_deriv_on_nhds HasStrictFDerivAt.approximates_deriv_on_nhds
@@ -797,4 +799,3 @@ theorem to_localInverse {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a)
 #align cont_diff_at.to_local_inverse ContDiffAt.to_localInverse
 
 end ContDiffAt
-
diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean
index c892362425e81..4d104ca272a76 100644
--- a/Mathlib/Analysis/Calculus/Taylor.lean
+++ b/Mathlib/Analysis/Calculus/Taylor.lean
@@ -353,10 +353,8 @@ theorem taylor_mean_remainder_bound {f : ℝ → E} {a b C x : ℝ} {n : ℕ} (h
     -- The rest is a trivial calculation
     rw [abs_mul, abs_pow, abs_inv, Nat.abs_cast]
     -- Porting note: was `mono* with 0 ≤ (n ! : ℝ)⁻¹; any_goals positivity; linarith [hx.1, hyx]`
-    have : 0 ≤ (n ! : ℝ)⁻¹ := by simp only [inv_nonneg, Nat.cast_nonneg]
-    refine' mul_le_mul_of_nonneg_left (pow_le_pow_of_le_left _ _ n) this
-    · simp only [abs_nonneg]
-    · rw [abs_of_nonneg, abs_of_nonneg] <;> linarith
+    gcongr
+    rw [abs_of_nonneg, abs_of_nonneg] <;> linarith
   -- Apply the mean value theorem for vector valued functions:
   have A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
       (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t := by
diff --git a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
index c8a761d4119e0..9c0bbc5dd4fcb 100644
--- a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
+++ b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
@@ -478,7 +478,7 @@ theorem UniformCauchySeqOnFilter.one_smulRight {l' : Filter 𝕜}
   simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
     ContinuousLinearMap.one_apply]
   rw [← smul_sub, norm_smul, mul_comm]
-  exact mul_le_mul hn.le rfl.le (norm_nonneg _) hq.le
+  gcongr
 #align uniform_cauchy_seq_on_filter.one_smul_right UniformCauchySeqOnFilter.one_smulRight
 
 theorem uniformCauchySeqOnFilter_of_deriv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
@@ -526,7 +526,7 @@ theorem hasDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
     simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.smulRight_apply,
       ContinuousLinearMap.one_apply]
     rw [← smul_sub, norm_smul, mul_comm]
-    exact mul_le_mul hn.le rfl.le (norm_nonneg _) hq.le
+    gcongr
   exact hasFDerivAt_of_tendstoUniformlyOnFilter hf' hf hfg
 #align has_deriv_at_of_tendsto_uniformly_on_filter hasDerivAt_of_tendstoUniformlyOnFilter
 
diff --git a/Mathlib/Analysis/Convex/Function.lean b/Mathlib/Analysis/Convex/Function.lean
index 99aa4d2b46afe..db1e48c2b1581 100644
--- a/Mathlib/Analysis/Convex/Function.lean
+++ b/Mathlib/Analysis/Convex/Function.lean
@@ -9,6 +9,7 @@ Authors: Alexander Bentkamp, François Dupuis
 ! if you have ported upstream changes.
 -/
 import Mathlib.Analysis.Convex.Basic
+import Mathlib.Tactic.GCongr
 
 /-!
 # Convex and concave functions
@@ -235,8 +236,7 @@ theorem ConvexOn.convex_le (hf : ConvexOn 𝕜 s f) (r : β) : Convex 𝕜 ({ x
   ⟨hf.1 hx.1 hy.1 ha hb hab,
     calc
       f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
-      _ ≤ a • r + b • r :=
-        (add_le_add (smul_le_smul_of_nonneg hx.2 ha) (smul_le_smul_of_nonneg hy.2 hb))
+      _ ≤ a • r + b • r := by gcongr; exact hx.2; exact hy.2
       _ = r := Convex.combo_self hab r
       ⟩
 #align convex_on.convex_le ConvexOn.convex_le
@@ -251,7 +251,7 @@ theorem ConvexOn.convex_epigraph (hf : ConvexOn 𝕜 s f) :
   refine' ⟨hf.1 hx hy ha hb hab, _⟩
   calc
     f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
-    _ ≤ a • r + b • t := add_le_add (smul_le_smul_of_nonneg hr ha) (smul_le_smul_of_nonneg ht hb)
+    _ ≤ a • r + b • t := by gcongr
 #align convex_on.convex_epigraph ConvexOn.convex_epigraph
 
 theorem ConcaveOn.convex_hypograph (hf : ConcaveOn 𝕜 s f) :
@@ -387,8 +387,7 @@ theorem StrictConvexOn.convex_lt (hf : StrictConvexOn 𝕜 s f) (r : β) :
     ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
       calc
         f (a • x + b • y) < a • f x + b • f y := hf.2 hx.1 hy.1 hxy ha hb hab
-        _ ≤ a • r + b • r :=
-          (add_le_add (smul_lt_smul_of_pos hx.2 ha).le (smul_lt_smul_of_pos hy.2 hb).le)
+        _ ≤ a • r + b • r := by gcongr; exact hx.2.le; exact hy.2.le
         _ = r := Convex.combo_self hab r
         ⟩
 #align strict_convex_on.convex_lt StrictConvexOn.convex_lt
@@ -601,12 +600,10 @@ theorem ConvexOn.sup (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) : ConvexO
   refine' ⟨hf.left, fun x hx y hy a b ha hb hab => sup_le _ _⟩
   · calc
       f (a • x + b • y) ≤ a • f x + b • f y := hf.right hx hy ha hb hab
-      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) :=
-        add_le_add (smul_le_smul_of_nonneg le_sup_left ha) (smul_le_smul_of_nonneg le_sup_left hb)
+      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_left
   · calc
       g (a • x + b • y) ≤ a • g x + b • g y := hg.right hx hy ha hb hab
-      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) :=
-        add_le_add (smul_le_smul_of_nonneg le_sup_right ha) (smul_le_smul_of_nonneg le_sup_right hb)
+      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_right
 #align convex_on.sup ConvexOn.sup
 
 /-- The pointwise minimum of concave functions is concave. -/
@@ -621,14 +618,10 @@ theorem StrictConvexOn.sup (hf : StrictConvexOn 𝕜 s f) (hg : StrictConvexOn 
     max_lt
       (calc
         f (a • x + b • y) < a • f x + b • f y := hf.2 hx hy hxy ha hb hab
-        _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) :=
-          add_le_add (smul_le_smul_of_nonneg le_sup_left ha.le)
-            (smul_le_smul_of_nonneg le_sup_left hb.le))
+        _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_left)
       (calc
         g (a • x + b • y) < a • g x + b • g y := hg.2 hx hy hxy ha hb hab
-        _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) :=
-          add_le_add (smul_le_smul_of_nonneg le_sup_right ha.le)
-            (smul_le_smul_of_nonneg le_sup_right hb.le))⟩
+        _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_right)⟩
 #align strict_convex_on.sup StrictConvexOn.sup
 
 /-- The pointwise minimum of strictly concave functions is strictly concave. -/
@@ -642,9 +635,10 @@ theorem ConvexOn.le_on_segment' (hf : ConvexOn 𝕜 s f) {x y : E} (hx : x ∈ s
     (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : f (a • x + b • y) ≤ max (f x) (f y) :=
   calc
     f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
-    _ ≤ a • max (f x) (f y) + b • max (f x) (f y) :=
-      (add_le_add (smul_le_smul_of_nonneg (le_max_left _ _) ha)
-        (smul_le_smul_of_nonneg (le_max_right _ _) hb))
+    _ ≤ a • max (f x) (f y) + b • max (f x) (f y) := by
+      gcongr
+      · apply le_max_left
+      · apply le_max_right
     _ = max (f x) (f y) := Convex.combo_self hab _
 #align convex_on.le_on_segment' ConvexOn.le_on_segment'
 
@@ -674,9 +668,10 @@ theorem StrictConvexOn.lt_on_open_segment' (hf : StrictConvexOn 𝕜 s f) {x y :
     f (a • x + b • y) < max (f x) (f y) :=
   calc
     f (a • x + b • y) < a • f x + b • f y := hf.2 hx hy hxy ha hb hab
-    _ ≤ a • max (f x) (f y) + b • max (f x) (f y) :=
-      (add_le_add (smul_le_smul_of_nonneg (le_max_left _ _) ha.le)
-        (smul_le_smul_of_nonneg (le_max_right _ _) hb.le))
+    _ ≤ a • max (f x) (f y) + b • max (f x) (f y) := by
+      gcongr
+      · apply le_max_left
+      · apply le_max_right
     _ = max (f x) (f y) := Convex.combo_self hab _
 #align strict_convex_on.lt_on_open_segment' StrictConvexOn.lt_on_open_segment'
 
diff --git a/Mathlib/Analysis/Convex/Segment.lean b/Mathlib/Analysis/Convex/Segment.lean
index 218dc1641f6d6..832c5844e2e11 100644
--- a/Mathlib/Analysis/Convex/Segment.lean
+++ b/Mathlib/Analysis/Convex/Segment.lean
@@ -12,7 +12,7 @@ import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.SMul
 import Mathlib.LinearAlgebra.AffineSpace.Midpoint
 import Mathlib.LinearAlgebra.Ray
-import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.GCongr
 
 /-!
 # Segments in vector spaces
@@ -349,7 +349,7 @@ theorem mem_segment_iff_div :
     use a, b, ha, hb
     simp [*]
   · rintro ⟨a, b, ha, hb, hab, rfl⟩
-    refine' ⟨a / (a + b), b / (a + b), div_nonneg ha hab.le, div_nonneg hb hab.le, _, rfl⟩
+    refine' ⟨a / (a + b), b / (a + b), by positivity, by positivity, _, rfl⟩
     rw [← add_div, div_self hab.ne']
 #align mem_segment_iff_div mem_segment_iff_div
 
@@ -431,9 +431,9 @@ theorem segment_subset_Icc (h : x ≤ y) : [x -[𝕜] y] ⊆ Icc x y := by
   constructor
   calc
     x = a • x + b • x := (Convex.combo_self hab _).symm
-    _ ≤ a • x + b • y := add_le_add_left (smul_le_smul_of_nonneg h hb) _
+    _ ≤ a • x + b • y := by gcongr
   calc
-    a • x + b • y ≤ a • y + b • y := add_le_add_right (smul_le_smul_of_nonneg h ha) _
+    a • x + b • y ≤ a • y + b • y := by gcongr
     _ = y := Convex.combo_self hab _
 #align segment_subset_Icc segment_subset_Icc
 
@@ -448,9 +448,9 @@ theorem openSegment_subset_Ioo (h : x < y) : openSegment 𝕜 x y ⊆ Ioo x y :=
   constructor
   calc
     x = a • x + b • x := (Convex.combo_self hab _).symm
-    _ < a • x + b • y := add_lt_add_left (smul_lt_smul_of_pos h hb) _
+    _ < a • x + b • y := by gcongr
   calc
-    a • x + b • y < a • y + b • y := add_lt_add_right (smul_lt_smul_of_pos h ha) _
+    a • x + b • y < a • y + b • y := by gcongr
     _ = y := Convex.combo_self hab _
 #align open_segment_subset_Ioo openSegment_subset_Ioo
 
diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
index 70ab9fd2ea717..0ebb23c972e5f 100644
--- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
+++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
@@ -56,16 +56,16 @@ theorem strictConvexOn_exp : StrictConvexOn ℝ univ exp := by
     calc
       exp y - exp x = exp y - exp y * exp (x - y) := by rw [← exp_add]; ring_nf
       _ = exp y * (1 - exp (x - y)) := by ring
-      _ < exp y * -(x - y) := (mul_lt_mul_of_pos_left ?_ y.exp_pos)
+      _ < exp y * -(x - y) := by gcongr; linarith [add_one_lt_exp_of_nonzero h2.ne]
       _ = exp y * (y - x) := by ring
-    linarith [add_one_lt_exp_of_nonzero h2.ne]
   · have h1 : 0 < z - y := by linarith
     rw [lt_div_iff h1]
     calc
-      exp y * (z - y) < exp y * (exp (z - y) - 1) := mul_lt_mul_of_pos_left ?_ y.exp_pos
+      exp y * (z - y) < exp y * (exp (z - y) - 1) := by
+        gcongr _ * ?_
+        linarith [add_one_lt_exp_of_nonzero h1.ne']
       _ = exp (z - y) * exp y - exp y := by ring
       _ ≤ exp z - exp y := by rw [← exp_add]; ring_nf; rfl
-    linarith [add_one_lt_exp_of_nonzero h1.ne']
 #align strict_convex_on_exp strictConvexOn_exp
 
 /-- `Real.exp` is convex on the whole real line. -/
@@ -85,15 +85,15 @@ theorem convexOn_pow (n : ℕ) : ConvexOn ℝ (Ici 0) fun x : ℝ => x ^ n := by
   have H := IH.2 ha hb hμ hν h
   have : 0 ≤ (b ^ k - a ^ k) * (b - a) * μ * ν := by
     cases' le_or_lt a b with hab hab
-    · have : a ^ k ≤ b ^ k := pow_le_pow_of_le_left ha hab k
+    · have : a ^ k ≤ b ^ k := by gcongr
       have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
       positivity
-    · have : b ^ k ≤ a ^ k := pow_le_pow_of_le_left hb hab.le k
+    · have : b ^ k ≤ a ^ k := by gcongr
       have : 0 ≤ (b ^ k - a ^ k) * (b - a) := by nlinarith
       positivity
   calc
     (μ * a + ν * b) ^ k.succ = (μ * a + ν * b) * (μ * a + ν * b) ^ k := pow_succ _ _
-    _ ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) := (mul_le_mul_of_nonneg_left H (by positivity))
+    _ ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) := by gcongr; exact H
     _ ≤ (μ * a + ν * b) * (μ * a ^ k + ν * b ^ k) + (b ^ k - a ^ k) * (b - a) * μ * ν := by linarith
     _ = (μ + ν) * (μ * a ^ k.succ + ν * b ^ k.succ) := by rw [Nat.succ_eq_add_one]; ring
     _ = μ * a ^ k.succ + ν * b ^ k.succ := by rw [h]; ring
@@ -112,13 +112,12 @@ nonrec theorem Even.convexOn_pow {n : ℕ} (hn : Even n) :
   have : (0 : ℝ) ≤ (a - b) ^ 2 * μ * ν := by positivity
   calc
     (μ * a + ν * b) ^ (2 * k) = ((μ * a + ν * b) ^ 2) ^ k := by rw [pow_mul]
-    _ ≤ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k := (pow_le_pow_of_le_left (by positivity) ?_ k)
+    _ ≤ ((μ + ν) * (μ * a ^ 2 + ν * b ^ 2)) ^ k := by gcongr; linarith
     _ = (μ * a ^ 2 + ν * b ^ 2) ^ k := by rw [h]; ring
     _ ≤ μ * (a ^ 2) ^ k + ν * (b ^ 2) ^ k := ?_
     _ ≤ μ * a ^ (2 * k) + ν * b ^ (2 * k) := by ring_nf; rfl
-  · linarith
-  · -- Porting note: `rw [mem_Ici]` was `dsimp`
-    refine' (convexOn_pow k).2 _ _ hμ hν h <;> rw [mem_Ici] <;> positivity
+  -- Porting note: `rw [mem_Ici]` was `dsimp`
+  refine' (convexOn_pow k).2 _ _ hμ hν h <;> rw [mem_Ici] <;> positivity
 #align even.convex_on_pow Even.convexOn_pow
 
 open Int in
@@ -139,15 +138,15 @@ theorem convexOn_zpow : ∀ m : ℤ, ConvexOn ℝ (Ioi 0) fun x : ℝ => x ^ m
     · -- Porting note: added type ascription to LHS
       calc
         (1 : ℝ) * (a ^ (n + 1) * b ^ (n + 1)) = ((μ + ν) ^ 2 * (a * b)) ^ (n + 1) := by rw [h]; ring
-        _ ≤ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1) := (pow_le_pow_of_le_left ?_ ?_ _)
+        _ ≤ ((μ * b + ν * a) * (μ * a + ν * b)) ^ (n + 1) := ?_
         _ = (μ * b + ν * a) ^ (n + 1) * (μ * a + ν * b) ^ (n + 1) := by rw [mul_pow]
         _ ≤ (μ * b ^ (n + 1) + ν * a ^ (n + 1)) * (μ * a + ν * b) ^ (n + 1) := ?_
-      · positivity
       · -- Porting note: added type ascription to LHS
+        gcongr (?_ : ℝ) ^ _
         have : (0 : ℝ) ≤ μ * ν * (a - b) ^ 2 := by positivity
         linarith
-      · apply mul_le_mul_of_nonneg_right ((convexOn_pow (n + 1)).2 hb.le ha.le hμ hν h)
-        positivity
+      · gcongr
+        apply (convexOn_pow (n + 1)).2 hb.le ha.le hμ hν h
     · have : 0 < μ * a + ν * b := by cases le_or_lt a b <;> nlinarith
       positivity
     · positivity
diff --git a/Mathlib/Analysis/Convex/Star.lean b/Mathlib/Analysis/Convex/Star.lean
index 7c36b9dc4835d..09952b049c7bb 100644
--- a/Mathlib/Analysis/Convex/Star.lean
+++ b/Mathlib/Analysis/Convex/Star.lean
@@ -9,6 +9,7 @@ Authors: Yaël Dillies
 ! if you have ported upstream changes.
 -/
 import Mathlib.Analysis.Convex.Segment
+import Mathlib.Tactic.GCongr
 
 /-!
 # Star-convex sets
@@ -431,16 +432,16 @@ theorem Set.OrdConnected.starConvex [OrderedSemiring 𝕜] [OrderedAddCommMonoid
   · refine' hs.out hx hy (mem_Icc.2 ⟨_, _⟩)
     calc
       x = a • x + b • x := (Convex.combo_self hab _).symm
-      _ ≤ a • x + b • y := add_le_add_left (smul_le_smul_of_nonneg hxy hb) _
+      _ ≤ a • x + b • y := by gcongr
     calc
-      a • x + b • y ≤ a • y + b • y := add_le_add_right (smul_le_smul_of_nonneg hxy ha) _
+      a • x + b • y ≤ a • y + b • y := by gcongr
       _ = y := Convex.combo_self hab _
   · refine' hs.out hy hx (mem_Icc.2 ⟨_, _⟩)
     calc
       y = a • y + b • y := (Convex.combo_self hab _).symm
-      _ ≤ a • x + b • y := add_le_add_right (smul_le_smul_of_nonneg hyx ha) _
+      _ ≤ a • x + b • y := by gcongr
     calc
-      a • x + b • y ≤ a • x + b • x := add_le_add_left (smul_le_smul_of_nonneg hyx hb) _
+      a • x + b • y ≤ a • x + b • x := by gcongr
       _ = x := Convex.combo_self hab _
 #align set.ord_connected.star_convex Set.OrdConnected.starConvex
 
diff --git a/Mathlib/Analysis/Convex/Uniform.lean b/Mathlib/Analysis/Convex/Uniform.lean
index 713c021ab76b4..29eda3c9d3609 100644
--- a/Mathlib/Analysis/Convex/Uniform.lean
+++ b/Mathlib/Analysis/Convex/Uniform.lean
@@ -86,10 +86,10 @@ theorem exists_forall_closed_ball_dist_add_le_two_sub (hε : 0 < ε) :
   have hxy' : ε / 3 ≤ ‖x' - y'‖ :=
     calc
       ε / 3 = ε - (ε / 3 + ε / 3) := by ring
-      _ ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) :=
-        (sub_le_sub hxy
-          (add_le_add ((h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _) <|
-            (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _))
+      _ ≤ ‖x - y‖ - (‖x' - x‖ + ‖y' - y‖) := by
+        gcongr
+        · exact (h₂ _ hx hx'.le).trans <| min_le_of_right_le <| min_le_left _ _
+        · exact (h₂ _ hy hy'.le).trans <| min_le_of_right_le <| min_le_left _ _
       _ ≤ _ := by
         have : ∀ x' y', x - y = x' - y' + (x - x') + (y' - y) := fun _ _ => by abel
         rw [sub_le_iff_le_add, norm_sub_rev _ x, ← add_assoc, this]
@@ -109,7 +109,8 @@ theorem exists_forall_closed_ball_dist_add_le_two_sub (hε : 0 < ε) :
       norm_num -- Porting note: these three extra lines needed to make `exact` work
       have : 3 * (δ / 3) * (1 / 3) = δ / 3 := by linarith
       rw [this, mul_comm]
-      exact mul_le_mul_of_nonneg_left (min_le_of_right_le <| min_le_right _ _) three_pos.le
+      gcongr
+      exact min_le_of_right_le <| min_le_right _ _
 #align exists_forall_closed_ball_dist_add_le_two_sub exists_forall_closed_ball_dist_add_le_two_sub
 
 theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (hε : 0 < ε) (r : ℝ) :
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean
index a588ed98e838f..b14b4ce9f1660 100644
--- a/Mathlib/Analysis/InnerProductSpace/Projection.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean
@@ -151,13 +151,11 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h
       exact add_halves 1
     have eq₁ : 4 * δ * δ ≤ 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
       simp_rw [mul_assoc]
-      exact mul_le_mul_of_nonneg_left (mul_self_le_mul_self zero_le_δ eq) zero_le_four
-    have eq₂ : ‖a‖ * ‖a‖ ≤ (δ + div) * (δ + div) :=
-      mul_self_le_mul_self (norm_nonneg _)
-        (le_trans (le_of_lt <| hw q) (add_le_add_left (Nat.one_div_le_one_div hq) _))
-    have eq₂' : ‖b‖ * ‖b‖ ≤ (δ + div) * (δ + div) :=
-      mul_self_le_mul_self (norm_nonneg _)
-        (le_trans (le_of_lt <| hw p) (add_le_add_left (Nat.one_div_le_one_div hp) _))
+      gcongr
+    have eq₂ : ‖a‖ ≤ δ + div :=
+        le_trans (le_of_lt <| hw q) (add_le_add_left (Nat.one_div_le_one_div hq) _)
+    have eq₂' : ‖b‖ ≤ δ + div :=
+        le_trans (le_of_lt <| hw p) (add_le_add_left (Nat.one_div_le_one_div hp) _)
     rw [dist_eq_norm]
     apply nonneg_le_nonneg_of_sq_le_sq
     · exact sqrt_nonneg _
@@ -165,15 +163,11 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h
     calc
       ‖wp - wq‖ * ‖wp - wq‖ =
           2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ := by
-        rw [← this]
-        simp
-      _ ≤ 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * δ * δ := (sub_le_sub_left eq₁ _)
-      _ ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ :=
-        (sub_le_sub_right (mul_le_mul_of_nonneg_left (add_le_add eq₂ eq₂') (by norm_num)) _)
+        simp [← this]
+      _ ≤ 2 * (‖a‖ * ‖a‖ + ‖b‖ * ‖b‖) - 4 * δ * δ := by gcongr
+      _ ≤ 2 * ((δ + div) * (δ + div) + (δ + div) * (δ + div)) - 4 * δ * δ := by gcongr
       _ = 8 * δ * div + 4 * div * div := by ring
-    exact
-      add_nonneg (mul_nonneg (mul_nonneg (by norm_num) zero_le_δ) (le_of_lt Nat.one_div_pos_of_nat))
-        (mul_nonneg (mul_nonneg (by norm_num) Nat.one_div_pos_of_nat.le) Nat.one_div_pos_of_nat.le)
+    positivity
     -- third goal : `Tendsto (fun (n : ℕ) => sqrt (b n)) atTop (𝓝 0)`
     apply Tendsto.comp (f := b) (g := sqrt)
     · have : Tendsto sqrt (nhds 0) (nhds (sqrt 0)) := continuous_sqrt.continuousAt
diff --git a/Mathlib/Analysis/LocallyConvex/Polar.lean b/Mathlib/Analysis/LocallyConvex/Polar.lean
index 891f19154d731..ef5548a01306d 100644
--- a/Mathlib/Analysis/LocallyConvex/Polar.lean
+++ b/Mathlib/Analysis/LocallyConvex/Polar.lean
@@ -151,7 +151,7 @@ theorem polar_univ (h : SeparatingRight B) : B.polar Set.univ = {(0 : F)} := by
     ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
       rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv,
         mul_inv_cancel_left₀ hc.ne']
-    _ ≤ ε * 1 := (mul_le_mul hcε.le (hy _ trivial) (norm_nonneg _) hε.le)
+    _ ≤ ε * 1 := by gcongr; exact hy _ trivial
     _ = ε := mul_one _
 #align linear_map.polar_univ LinearMap.polar_univ
 
diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
index ab2cab6ab12c2..7539a53e23d29 100644
--- a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
+++ b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean
@@ -253,7 +253,8 @@ protected theorem LinearIndependent.eventually {ι} [Finite ι] {f : ι → E}
     Finset.sum_sub_distrib, ← smul_sub, ← sub_smul, NNReal.coe_sum, coe_nnnorm, Finset.sum_mul]
   refine' norm_sum_le_of_le _ fun i _ => _
   rw [norm_smul, mul_comm]
-  exact mul_le_mul_of_nonneg_left (norm_le_pi_norm (v - u) i) (norm_nonneg _)
+  gcongr
+  exact norm_le_pi_norm (v - u) i
 #align linear_independent.eventually LinearIndependent.eventually
 
 theorem isOpen_setOf_linearIndependent {ι : Type _} [Finite ι] :
@@ -279,15 +280,13 @@ theorem Basis.op_nnnorm_le {ι : Type _} [Fintype ι] (v : Basis ι 𝕜 E) {u :
       _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp [u.map_sum, LinearMap.map_smul]
       _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := (nnnorm_sum_le _ _)
       _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
-      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M :=
-        (Finset.sum_le_sum fun i _ => mul_le_mul_of_nonneg_left (hu i) (zero_le _))
+      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
       _ = (∑ i, ‖v.equivFun e i‖₊) * M := Finset.sum_mul.symm
-      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M :=
-        (suffices _ from mul_le_mul_of_nonneg_right this (zero_le M)
+      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
+        gcongr
         calc
           (∑ i, ‖v.equivFun e i‖₊) ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
           _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_of_le_right (φ.le_op_nnnorm e) _
-          )
       _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]
 #align basis.op_nnnorm_le Basis.op_nnnorm_le
 
@@ -460,7 +459,7 @@ theorem finiteDimensional_of_isCompact_closed_ball₀ {r : ℝ} (rpos : 0 < r)
     intro n
     simp only [norm_smul, dist_zero_right, Metric.mem_closedBall]
     calc
-      ‖c‖ * ‖f n‖ ≤ r / R * R := mul_le_mul hc.2.le (fle n) (norm_nonneg _) rRpos.le
+      ‖c‖ * ‖f n‖ ≤ r / R * R := by gcongr; exact hc.2.le; apply fle
       _ = r := by field_simp [(zero_lt_one.trans Rgt).ne']
   -- Porting note: moved type ascriptions because of exists_prop changes
   obtain ⟨x : E, _ : x ∈ Metric.closedBall (0 : E) r, φ : ℕ → ℕ, φmono : StrictMono φ,
@@ -473,7 +472,8 @@ theorem finiteDimensional_of_isCompact_closed_ball₀ {r : ℝ} (rpos : 0 < r)
     ‖c‖ ≤ dist (g (φ (N + 1))) (g (φ N)) := by
       conv_lhs => rw [← mul_one ‖c‖]
       simp only [dist_eq_norm, ← smul_sub, norm_smul]
-      apply mul_le_mul_of_nonneg_left (lef _ _ (ne_of_gt _)) (norm_nonneg _)
+      gcongr
+      apply lef _ _ (ne_of_gt _)
       exact φmono (Nat.lt_succ_self N)
     _ < ‖c‖ := hN (N + 1) (Nat.le_succ N)
 #align finite_dimensional_of_is_compact_closed_ball₀ finiteDimensional_of_isCompact_closed_ball₀
@@ -569,7 +569,7 @@ def ContinuousLinearEquiv.piRing (ι : Type _) [Fintype ι] [DecidableEq ι] :
       rw [smul_mul_assoc]
       refine' Finset.sum_le_card_nsmul _ _ _ fun i _ => _
       rw [norm_smul, mul_comm]
-      exact mul_le_mul (norm_le_pi_norm g i) (norm_le_pi_norm t i) (norm_nonneg _) (norm_nonneg g) }
+      gcongr <;> apply norm_le_pi_norm }
 #align continuous_linear_equiv.pi_ring ContinuousLinearEquiv.piRing
 
 /-- A family of continuous linear maps is continuous on `s` if all its applications are. -/
diff --git a/Mathlib/Analysis/NormedSpace/Multilinear.lean b/Mathlib/Analysis/NormedSpace/Multilinear.lean
index e7b2f34d4f721..c766e68adbc59 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear.lean
@@ -168,8 +168,9 @@ theorem norm_image_sub_le_of_bound' [DecidableEq ι] {C : ℝ} (hC : 0 ≤ C)
           simp [his]
         · simp [h]
       rw [B, A, ← f.map_sub]
-      apply le_trans (H _) (mul_le_mul_of_nonneg_left _ hC)
-      refine' prod_le_prod (fun j _ => norm_nonneg _) fun j _ => _
+      apply le_trans (H _)
+      gcongr with j
+      · exact fun j _ => norm_nonneg _
       by_cases h : j = i
       · rw [h]
         simp
@@ -221,8 +222,7 @@ theorem norm_image_sub_le_of_bound {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m
   calc
     ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
       f.norm_image_sub_le_of_bound' hC H m₁ m₂
-    _ ≤ C * ∑ i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) :=
-      (mul_le_mul_of_nonneg_left (sum_le_sum fun i _ => A i) hC)
+    _ ≤ C * ∑ i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by gcongr; apply A
     _ = C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ := by
       rw [sum_const, card_univ, nsmul_eq_mul]
       ring
@@ -242,15 +242,12 @@ theorem continuous_of_bound (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m
     continuousAt_of_locally_lipschitz zero_lt_one
       (D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1)) fun m' h' => _
   rw [dist_eq_norm, dist_eq_norm]
-  have : 0 ≤ max ‖m'‖ ‖m‖ := by simp
   have : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1 := by
     simp [zero_le_one, norm_le_of_mem_closedBall (le_of_lt h')]
   calc
     ‖f m' - f m‖ ≤ D * Fintype.card ι * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ :=
       f.norm_image_sub_le_of_bound D_pos H m' m
-    _ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by
-      apply_rules [mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, mul_nonneg, norm_nonneg,
-        Nat.cast_nonneg, pow_le_pow_of_le_left]
+    _ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by gcongr
 #align multilinear_map.continuous_of_bound MultilinearMap.continuous_of_bound
 
 /-- Constructing a continuous multilinear map from a multilinear map satisfying a boundedness
diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean
index f6f3e1f104624..fd523c3ad4ded 100644
--- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean
+++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean
@@ -355,7 +355,7 @@ protected theorem tmp_closedBall_div_subset {a b : ℝ} (ha : 0 < a) (hb : 0 < b
   rw [mem_closedBall_zero_iff] at hf hx⊢
   calc
     ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_op_norm _ _
-    _ ≤ a / b * b := (mul_le_mul hf hx (norm_nonneg _) (div_pos ha hb).le)
+    _ ≤ a / b * b := by gcongr
     _ = a := div_mul_cancel a hb.ne.symm
 #align continuous_linear_map.tmp_closed_ball_div_subset ContinuousLinearMap.tmp_closedBall_div_subset
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Bernstein.lean b/Mathlib/Analysis/SpecialFunctions/Bernstein.lean
index 0d296503785fc..b3ef30a2abd19 100644
--- a/Mathlib/Analysis/SpecialFunctions/Bernstein.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Bernstein.lean
@@ -69,11 +69,23 @@ theorem bernstein_apply (n ν : ℕ) (x : I) :
 
 theorem bernstein_nonneg {n ν : ℕ} {x : I} : 0 ≤ bernstein n ν x := by
   simp only [bernstein_apply]
-  exact
-    mul_nonneg (mul_nonneg (Nat.cast_nonneg _) (pow_nonneg (by unit_interval) _))
-      (pow_nonneg (by unit_interval) _)
+  have h₁ : (0:ℝ) ≤ x := by unit_interval
+  have h₂ : (0:ℝ) ≤ 1 - x := by unit_interval
+  positivity
 #align bernstein_nonneg bernstein_nonneg
 
+namespace Mathlib.Meta.Positivity
+
+open Lean Meta Qq Function
+
+@[positivity FunLike.coe _ _]
+def evalBernstein : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app (.app _coe (.app (.app _ n) ν)) x ← whnfR e | throwError "not bernstein polynomial"
+  let p ← mkAppOptM ``bernstein_nonneg #[n, ν, x]
+  pure (.nonnegative p)
+
+end Mathlib.Meta.Positivity
+
 /-!
 We now give a slight reformulation of `bernsteinPolynomial.variance`.
 -/
@@ -227,10 +239,8 @@ theorem bernsteinApproximation_uniform (f : C(I, ℝ)) :
   have nhds_zero := tendsto_const_div_atTop_nhds_0_nat (2 * ‖f‖ * δ ^ (-2 : ℤ))
   filter_upwards [nhds_zero.eventually (gt_mem_nhds (half_pos h)), eventually_gt_atTop 0] with n nh
     npos'
-  have npos : 0 < (n : ℝ) := by exact_mod_cast npos'
-  -- Two easy inequalities we'll need later:
-  have w₁ : 0 ≤ 2 * ‖f‖ := mul_nonneg (by norm_num) (norm_nonneg f)
-  have w₂ : 0 ≤ 2 * ‖f‖ * δ ^ (-2 : ℤ) := mul_nonneg w₁ (zpow_neg_two_nonneg _)
+  have npos : 0 < (n : ℝ) := by positivity
+  have w₂ : 0 ≤ δ ^ (-2:ℤ) := zpow_neg_two_nonneg _ -- TODO: need a positivity extension for `zpow`
   -- As `[0,1]` is compact, it suffices to check the inequality pointwise.
   rw [ContinuousMap.norm_lt_iff _ h]
   intro x
@@ -256,48 +266,40 @@ theorem bernsteinApproximation_uniform (f : C(I, ℝ)) :
   · -- We now work on the terms in `S`: uniform continuity and `bernstein.probability`
     -- quickly give us a bound.
     calc
-      (∑ k in S, |f k/ₙ - f x| * bernstein n k x) ≤ ∑ k in S, ε / 2 * bernstein n k x :=
-        Finset.sum_le_sum fun k m =>
-          mul_le_mul_of_nonneg_right (le_of_lt (lt_of_mem_S m)) bernstein_nonneg
+      (∑ k in S, |f k/ₙ - f x| * bernstein n k x) ≤ ∑ k in S, ε / 2 * bernstein n k x := by
+        gcongr with _ m
+        exact le_of_lt (lt_of_mem_S m)
       _ = ε / 2 * ∑ k in S, bernstein n k x := by rw [Finset.mul_sum]
       -- In this step we increase the sum over `S` back to a sum over all of `Fin (n+1)`,
       -- so that we can use `bernstein.probability`.
-      _ ≤
-          ε / 2 * ∑ k : Fin (n + 1), bernstein n k x :=
-        (mul_le_mul_of_nonneg_left (Finset.sum_le_univ_sum_of_nonneg fun k => bernstein_nonneg)
-          (le_of_lt (half_pos h)))
+      _ ≤ ε / 2 * ∑ k : Fin (n + 1), bernstein n k x := by
+        gcongr
+        exact Finset.sum_le_univ_sum_of_nonneg fun k => bernstein_nonneg
       _ = ε / 2 := by rw [bernstein.probability, mul_one]
   · -- We now turn to working on `Sᶜ`: we control the difference term just using `‖f‖`,
     -- and then insert a `δ^(-2) * (x - k/n)^2` factor
     -- (which is at least one because we are not in `S`).
     calc
-      (∑ k in Sᶜ, |f k/ₙ - f x| * bernstein n k x) ≤ ∑ k in Sᶜ, 2 * ‖f‖ * bernstein n k x :=
-        Finset.sum_le_sum fun k _ =>
-          mul_le_mul_of_nonneg_right (f.dist_le_two_norm _ _) bernstein_nonneg
+      (∑ k in Sᶜ, |f k/ₙ - f x| * bernstein n k x) ≤ ∑ k in Sᶜ, 2 * ‖f‖ * bernstein n k x := by
+        gcongr
+        apply f.dist_le_two_norm
       _ = 2 * ‖f‖ * ∑ k in Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
-      _ ≤ 2 * ‖f‖ * ∑ k in Sᶜ, δ ^ (-2 : ℤ) * ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x :=
-        (mul_le_mul_of_nonneg_left
-          (Finset.sum_le_sum fun k m => by
-            conv_lhs => rw [← one_mul (bernstein _ _ _)]
-            exact mul_le_mul_of_nonneg_right (le_of_mem_S_compl m) bernstein_nonneg)
-          w₁)
+      _ ≤ 2 * ‖f‖ * ∑ k in Sᶜ, δ ^ (-2 : ℤ) * ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x := by
+        gcongr with _ m
+        conv_lhs => rw [← one_mul (bernstein _ _ _)]
+        gcongr
+        exact le_of_mem_S_compl m
       -- Again enlarging the sum from `Sᶜ` to all of `Fin (n+1)`
-      _ ≤
-          2 * ‖f‖ * ∑ k : Fin (n + 1), δ ^ (-2 : ℤ) * ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x :=
-        (mul_le_mul_of_nonneg_left
-          (Finset.sum_le_univ_sum_of_nonneg fun k =>
-            mul_nonneg (mul_nonneg (zpow_neg_two_nonneg _) (sq_nonneg _)) bernstein_nonneg)
-          w₁)
+      _ ≤ 2 * ‖f‖ * ∑ k : Fin (n + 1), δ ^ (-2 : ℤ) * ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x := by
+        gcongr
+        refine Finset.sum_le_univ_sum_of_nonneg <| fun k => ?_
+        positivity
       _ = 2 * ‖f‖ * δ ^ (-2 : ℤ) * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x := by
         conv_rhs =>
           rw [mul_assoc, Finset.mul_sum]
           simp only [← mul_assoc]
       -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
-      _ =
-          2 * ‖f‖ * δ ^ (-2 : ℤ) * x * (1 - x) / n :=
-        by rw [variance npos]; ring
-      _ ≤ 2 * ‖f‖ * δ ^ (-2 : ℤ) / n :=
-        ((div_le_div_right npos).mpr <| by
-          refine' mul_le_of_le_of_le_one' (mul_le_of_le_one_right w₂ _) _ _ w₂ <;> unit_interval)
-      _ < ε / 2 := nh
+      _ = 2 * ‖f‖ * δ ^ (-2 : ℤ) * x * (1 - x) / n := by rw [variance npos]; ring
+      _ ≤ 2 * ‖f‖ * δ ^ (-2 : ℤ) * 1 * 1 / n := by gcongr <;> unit_interval
+      _ < ε / 2 := by simp only [mul_one]; exact nh
 #align bernstein_approximation_uniform bernsteinApproximation_uniform
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
index 1bf866ae266f2..7cd67a36e145c 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
@@ -39,7 +39,7 @@ theorem hasStrictDerivAt_log_of_pos (hx : 0 < x) : HasStrictDerivAt log x⁻¹ x
     (hasStrictDerivAt_exp <| log x).of_local_left_inverse (continuousAt_log hx.ne')
         (ne_of_gt <| exp_pos _) <|
       Eventually.mono (lt_mem_nhds hx) @exp_log
-  rwa [exp_log hx] at this 
+  rwa [exp_log hx] at this
 #align real.has_strict_deriv_at_log_of_pos Real.hasStrictDerivAt_log_of_pos
 
 theorem hasStrictDerivAt_log (hx : x ≠ 0) : HasStrictDerivAt log x⁻¹ x := by
@@ -252,10 +252,11 @@ theorem abs_log_sub_add_sum_range_le {x : ℝ} (h : |x| < 1) (n : ℕ) :
   have B : ∀ y ∈ Icc (-|x|) (|x|), |F' y| ≤ |x| ^ n / (1 - |x|) := fun y hy ↦
     calc
       |F' y| = |y| ^ n / |1 - y| := by simp [abs_div]
-      _ ≤ |x| ^ n / (1 - |x|) :=
+      _ ≤ |x| ^ n / (1 - |x|) := by
         have : |y| ≤ |x| := abs_le.2 hy
         have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
-        div_le_div (by positivity) (pow_le_pow_of_le_left (abs_nonneg _) ‹_› _) (sub_pos.2 h) ‹_›
+        gcongr
+        exact sub_pos.2 h
   -- third step: apply the mean value inequality
   have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖ := by
     refine Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
@@ -287,8 +288,8 @@ theorem hasSum_pow_div_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) :
         have : (0 : ℝ) ≤ i + 1 := le_of_lt (Nat.cast_add_one_pos i)
         rw [norm_eq_abs, abs_div, ← pow_abs, abs_of_nonneg this]
       _ ≤ |x| ^ (i + 1) / (0 + 1) := by
-        apply_rules [div_le_div_of_le_left, pow_nonneg, abs_nonneg, add_le_add_right, i.cast_nonneg]
-        norm_num
+        gcongr
+        exact i.cast_nonneg
       _ ≤ |x| ^ i := by
         simpa [pow_succ'] using mul_le_of_le_one_right (pow_nonneg (abs_nonneg x) i) (le_of_lt h)
 #align real.has_sum_pow_div_log_of_abs_lt_1 Real.hasSum_pow_div_log_of_abs_lt_1
@@ -310,7 +311,7 @@ theorem hasSum_log_sub_log_of_abs_lt_1 {x : ℝ} (h : |x| < 1) :
     convert h₁.add (hasSum_pow_div_log_of_abs_lt_1 h) using 1
     ring_nf
   · intro m hm
-    rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm 
+    rw [range_two_mul, Set.mem_setOf_eq, ← Nat.even_add_one] at hm
     dsimp
     rw [Even.neg_pow hm, neg_one_mul, neg_add_self]
 #align real.has_sum_log_sub_log_of_abs_lt_1 Real.hasSum_log_sub_log_of_abs_lt_1
@@ -337,4 +338,3 @@ theorem hasSum_log_one_add_inv {a : ℝ} (h : 0 < a) :
 #align real.has_sum_log_one_add_inv Real.hasSum_log_one_add_inv
 
 end Real
-
diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean
index 8faea2b0796b9..e6924617064cc 100644
--- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean
+++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean
@@ -505,8 +505,8 @@ theorem exists_pos_set_lintegral_lt_of_measure_lt {f : α → ℝ≥0∞} (h : (
     _ = C * μ s + ε₁ := by
       simp only [← SimpleFunc.lintegral_eq_lintegral, coe_const, lintegral_const,
         Measure.restrict_apply, MeasurableSet.univ, univ_inter, Function.const]
-    _ ≤ C * ((ε₂ - ε₁) / C) + ε₁ := (add_le_add_right (mul_le_mul_left' hs.le _) _)
-    _ ≤ ε₂ - ε₁ + ε₁ := (add_le_add mul_div_le le_rfl)
+    _ ≤ C * ((ε₂ - ε₁) / C) + ε₁ := by gcongr
+    _ ≤ ε₂ - ε₁ + ε₁ := by gcongr; apply mul_div_le
     _ = ε₂ := tsub_add_cancel_of_le hε₁₂.le
 #align measure_theory.exists_pos_set_lintegral_lt_of_measure_lt MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt
 
@@ -811,9 +811,9 @@ theorem lintegral_add_mul_meas_add_le_le_lintegral {f g : α → ℝ≥0∞} (hl
   calc
     (∫⁻ x, f x ∂μ) + ε * μ { x | f x + ε ≤ g x } = (∫⁻ x, φ x ∂μ) + ε * μ { x | f x + ε ≤ g x } :=
       by rw [hφ_eq]
-    _ ≤ (∫⁻ x, φ x ∂μ) + ε * μ { x | φ x + ε ≤ g x } :=
-      (add_le_add_left
-        (mul_le_mul_left' (measure_mono fun x => (add_le_add_right (hφ_le _) _).trans) _) _)
+    _ ≤ (∫⁻ x, φ x ∂μ) + ε * μ { x | φ x + ε ≤ g x } := by
+      gcongr
+      exact measure_mono fun x => (add_le_add_right (hφ_le _) _).trans
     _ = ∫⁻ x, φ x + indicator { x | φ x + ε ≤ g x } (fun _ => ε) x ∂μ := by
       rw [lintegral_add_left hφm, lintegral_indicator₀, set_lintegral_const]
       exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable
diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean
index 46201655b5ad4..d2a2d8a784934 100644
--- a/Mathlib/MeasureTheory/Integral/SetToL1.lean
+++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean
@@ -581,10 +581,9 @@ theorem norm_setToSimpleFunc_le_sum_mul_norm (T : Set α → F →L[ℝ] F') {C
   calc
     ‖f.setToSimpleFunc T‖ ≤ ∑ x in f.range, ‖T (f ⁻¹' {x})‖ * ‖x‖ :=
       norm_setToSimpleFunc_le_sum_op_norm T f
-    _ ≤ ∑ x in f.range, C * (μ (f ⁻¹' {x})).toReal * ‖x‖ :=
-      (sum_le_sum fun b _ =>
-        mul_le_mul_of_nonneg_right (hT_norm _ <| SimpleFunc.measurableSet_fiber _ _) <|
-          norm_nonneg _)
+    _ ≤ ∑ x in f.range, C * (μ (f ⁻¹' {x})).toReal * ‖x‖ := by
+      gcongr
+      exact hT_norm _ <| SimpleFunc.measurableSet_fiber _ _
     _ ≤ C * ∑ x in f.range, (μ (f ⁻¹' {x})).toReal * ‖x‖ := by simp_rw [mul_sum, ← mul_assoc]; rfl
 #align measure_theory.simple_func.norm_set_to_simple_func_le_sum_mul_norm MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm
 
@@ -599,11 +598,9 @@ theorem norm_setToSimpleFunc_le_sum_mul_norm_of_integrable (T : Set α → E →
       refine' Finset.sum_le_sum fun b hb => _
       obtain rfl | hb := eq_or_ne b 0
       · simp
-      exact
-        mul_le_mul_of_nonneg_right
-          (hT_norm _ (SimpleFunc.measurableSet_fiber _ _) <|
-            SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hb)
-          (norm_nonneg _)
+      gcongr
+      exact hT_norm _ (SimpleFunc.measurableSet_fiber _ _) <|
+        SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hb
     _ ≤ C * ∑ x in f.range, (μ (f ⁻¹' {x})).toReal * ‖x‖ := by simp_rw [mul_sum, ← mul_assoc]; rfl
 #align measure_theory.simple_func.norm_set_to_simple_func_le_sum_mul_norm_of_integrable MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable
 
diff --git a/Mathlib/MeasureTheory/Measure/Doubling.lean b/Mathlib/MeasureTheory/Measure/Doubling.lean
index 23e1dec3783d4..65d1720611f17 100644
--- a/Mathlib/MeasureTheory/Measure/Doubling.lean
+++ b/Mathlib/MeasureTheory/Measure/Doubling.lean
@@ -88,7 +88,7 @@ theorem exists_eventually_forall_measure_closedBall_le_mul (K : ℝ) :
       μ (closedBall x ((2 : ℝ) ^ (n + 1) * ε)) = μ (closedBall x ((2 : ℝ) ^ n * (2 * ε))) := by
         rw [pow_succ', mul_assoc]
       _ ≤ ↑(C ^ n) * μ (closedBall x (2 * ε)) := (hε.1 x)
-      _ ≤ ↑(C ^ n) * (C * μ (closedBall x ε)) := (ENNReal.mul_left_mono (hε.2 x))
+      _ ≤ ↑(C ^ n) * (C * μ (closedBall x ε)) := by gcongr; exact hε.2 x
       _ = ↑(C ^ (n + 1)) * μ (closedBall x ε) := by rw [← mul_assoc, pow_succ', ENNReal.coe_mul]
   rcases lt_or_le K 1 with (hK | hK)
   · refine' ⟨1, _⟩
diff --git a/Mathlib/NumberTheory/Liouville/Basic.lean b/Mathlib/NumberTheory/Liouville/Basic.lean
index 3bc24ec2342fe..14ef66e23830e 100644
--- a/Mathlib/NumberTheory/Liouville/Basic.lean
+++ b/Mathlib/NumberTheory/Liouville/Basic.lean
@@ -41,7 +41,7 @@ protected theorem irrational {x : ℝ} (h : Liouville x) : Irrational x := by
   -- By contradiction, `x = a / b`, with `a ∈ ℤ`, `0 < b ∈ ℕ` is a Liouville number,
   rintro ⟨⟨a, b, bN0, cop⟩, rfl⟩
   -- clear up the mess of constructions of rationals
-  rw [Rat.cast_mk', ← div_eq_mul_inv] at h 
+  rw [Rat.cast_mk', ← div_eq_mul_inv] at h
   -- Since `a / b` is a Liouville number, there are `p, q ∈ ℤ`, with `q1 : 1 < q`,
   -- `a0 : a / b ≠ p / q` and `a1 : |a / b - p / q| < 1 / q ^ (b + 1)`
   rcases h (b + 1) with ⟨p, q, q1, a0, a1⟩
@@ -66,7 +66,7 @@ protected theorem irrational {x : ℝ} (h : Liouville x) : Irrational x := by
   -- Actually, the absolute value of an integer is a natural number
   lift |a * ↑q - ↑b * p| to ℕ using abs_nonneg (a * ↑q - ↑b * p) with e he
   -- At a1, revert to natural numbers
-  rw [← Int.ofNat_mul, ← Int.coe_nat_pow, ← Int.ofNat_mul, Int.ofNat_lt] at a1 
+  rw [← Int.ofNat_mul, ← Int.coe_nat_pow, ← Int.ofNat_mul, Int.ofNat_lt] at a1
   -- Recall this is by contradiction: we obtained the inequality `b * q ≤ x * q ^ (b + 1)`, so
   -- we are done.
   exact not_le.mpr a1 (Nat.mul_lt_mul_pow_succ (Int.coe_nat_pos.mp ap) (Int.ofNat_lt.mp q1)).le
@@ -152,7 +152,7 @@ theorem exists_pos_real_of_irrational_root {α : ℝ} (ha : Irrational α) {f :
   · exact fun a => one_le_pow_of_one_le ((le_add_iff_nonneg_left 1).mpr a.cast_nonneg) _
   -- 2: the polynomial `fR` is Lipschitz at `α` -- as its derivative continuous;
   · rw [mul_comm]
-    rw [Real.closedBall_eq_Icc] at hy 
+    rw [Real.closedBall_eq_Icc] at hy
     -- apply the Mean Value Theorem: the bound on the derivative comes from differentiability.
     refine'
       Convex.norm_image_sub_le_of_norm_deriv_le (fun _ _ => fR.differentiableAt)
@@ -181,7 +181,7 @@ protected theorem transcendental {x : ℝ} (lx : Liouville x) : Transcendental 
   rintro ⟨f : ℤ[X], f0, ef0⟩
   -- Change `aeval x f = 0` to `eval (map _ f) = 0`, who knew.
   replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0;
-  · rwa [aeval_def, ← eval_map] at ef0 
+  · rwa [aeval_def, ← eval_map] at ef0
   -- There is a "large" real number `A` such that `(b + 1) ^ (deg f) * |f (x - a / (b + 1))| * A`
   -- is at least one.  This is obtained from lemma `exists_pos_real_of_irrational_root`.
   obtain ⟨A, hA, h⟩ : ∃ A : ℝ, 0 < A ∧ ∀ (a : ℤ) (b : ℕ),
@@ -198,23 +198,23 @@ protected theorem transcendental {x : ℝ} (lx : Liouville x) : Transcendental 
   -- recall, this is a proof by contradiction!
   refine' lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|) _
   -- clear denominators at `a1`
-  rw [lt_div_iff' (pow_pos b0 _), pow_add, mul_assoc] at a1 
+  rw [lt_div_iff' (pow_pos b0 _), pow_add, mul_assoc] at a1
   -- split the inequality via `1 / A`.
   refine' (_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le _
   -- This branch of the proof uses the Liouville condition and the Archimedean property
   · refine' (lt_div_iff' hA).mpr _
     refine' lt_of_le_of_lt _ a1
-    refine' mul_le_mul_of_nonneg_right _ (mul_nonneg (pow_nonneg b0.le _) (abs_nonneg _))
+    gcongr
     refine' hn.le.trans _
     rw [one_add_one_eq_two]
-    refine' pow_le_pow_of_le_left zero_le_two _ _
+    gcongr
     exact Int.cast_two.symm.le.trans (Int.cast_le.mpr (Int.add_one_le_iff.mpr b1))
   -- this branch of the proof exploits the "integrality" of evaluations of polynomials
   -- at ratios of integers.
   · lift b to ℕ using zero_le_one.trans b1.le
     specialize h a b.pred
     rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
-      div_le_iff hA] at h 
+      div_le_iff hA] at h
     exact Int.ofNat_lt.mp b1
 #align liouville.transcendental Liouville.transcendental
 
diff --git a/Mathlib/NumberTheory/Padics/Hensel.lean b/Mathlib/NumberTheory/Padics/Hensel.lean
index e01ff97185ce9..8d93942a09235 100644
--- a/Mathlib/NumberTheory/Padics/Hensel.lean
+++ b/Mathlib/NumberTheory/Padics/Hensel.lean
@@ -47,7 +47,7 @@ theorem padic_polynomial_dist {p : ℕ} [Fact p.Prime] (F : Polynomial ℤ_[p])
   let ⟨z, hz⟩ := F.evalSubFactor x y
   calc
     ‖F.eval x - F.eval y‖ = ‖z‖ * ‖x - y‖ := by simp [hz]
-    _ ≤ 1 * ‖x - y‖ := (mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _))
+    _ ≤ 1 * ‖x - y‖ := by gcongr; apply PadicInt.norm_le_one
     _ = ‖x - y‖ := by simp
 
 #align padic_polynomial_dist padic_polynomial_dist
@@ -155,8 +155,9 @@ private theorem calc_norm_le_one {n : ℕ} {z : ℤ_[p]} (hz : ih n z) :
         ‖(↑(F.eval z) : ℚ_[p])‖ / ‖(↑(F.derivative.eval z) : ℚ_[p])‖ :=
       norm_div _ _
     _ = ‖F.eval z‖ / ‖F.derivative.eval a‖ := by simp [hz.1]
-    _ ≤ ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n / ‖F.derivative.eval a‖ :=
-      ((div_le_div_right (deriv_norm_pos hnorm)).2 hz.2)
+    _ ≤ ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n / ‖F.derivative.eval a‖ := by
+      gcongr
+      apply hz.2
     _ = ‖F.derivative.eval a‖ * T ^ 2 ^ n := (div_sq_cancel _ _)
     _ ≤ 1 := mul_le_one (PadicInt.norm_le_one _) (T_pow_nonneg _) (le_of_lt (T_pow' hnorm _))
 
@@ -168,8 +169,9 @@ private theorem calc_deriv_dist {z z' z1 : ℤ_[p]} (hz' : z' = z - z1)
     ‖F.derivative.eval z' - F.derivative.eval z‖ ≤ ‖z' - z‖ := padic_polynomial_dist _ _ _
     _ = ‖z1‖ := by simp only [sub_eq_add_neg, add_assoc, hz', add_add_neg_cancel'_right, norm_neg]
     _ = ‖F.eval z‖ / ‖F.derivative.eval a‖ := hz1
-    _ ≤ ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n / ‖F.derivative.eval a‖ :=
-      ((div_le_div_right (deriv_norm_pos hnorm)).2 hz.2)
+    _ ≤ ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n / ‖F.derivative.eval a‖ := by
+      gcongr
+      apply hz.2
     _ = ‖F.derivative.eval a‖ * T ^ 2 ^ n := (div_sq_cancel _ _)
     _ < ‖F.derivative.eval a‖ := (mul_lt_iff_lt_one_right (deriv_norm_pos hnorm)).2
       (T_pow' hnorm _)
@@ -200,15 +202,14 @@ private def calc_eval_z' {z z' z1 : ℤ_[p]} (hz' : z' = z - z1) {n} (hz : ih n
 
 private def calc_eval_z'_norm {z z' z1 : ℤ_[p]} {n} (hz : ih n z) {q} (heq : F.eval z' = q * z1 ^ 2)
     (h1 : ‖(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)‖ ≤ 1) (hzeq : z1 = ⟨_, h1⟩) :
-    ‖F.eval z'‖ ≤ ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ (n + 1) :=
+    ‖F.eval z'‖ ≤ ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ (n + 1) := by
   calc
     ‖F.eval z'‖ = ‖q‖ * ‖z1‖ ^ 2 := by simp [heq]
-    _ ≤ 1 * ‖z1‖ ^ 2 :=
-      (mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (pow_nonneg (norm_nonneg _) _))
+    _ ≤ 1 * ‖z1‖ ^ 2 := by gcongr; apply PadicInt.norm_le_one
     _ = ‖F.eval z‖ ^ 2 / ‖F.derivative.eval a‖ ^ 2 := by simp [hzeq, hz.1, div_pow]
-    _ ≤ (‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n) ^ 2 / ‖F.derivative.eval a‖ ^ 2 :=
-      ((div_le_div_right (deriv_sq_norm_pos hnorm)).2
-      (pow_le_pow_of_le_left (norm_nonneg _) hz.2 _))
+    _ ≤ (‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n) ^ 2 / ‖F.derivative.eval a‖ ^ 2 := by
+      gcongr
+      exact hz.2
     _ = (‖F.derivative.eval a‖ ^ 2) ^ 2 * (T ^ 2 ^ n) ^ 2 / ‖F.derivative.eval a‖ ^ 2 := by
       simp only [mul_pow]
     _ = ‖F.derivative.eval a‖ ^ 2 * (T ^ 2 ^ n) ^ 2 := (div_sq_cancel _ _)
@@ -233,7 +234,7 @@ private def ih_n {n : ℕ} {z : ℤ_[p]} (hz : ih n z) : { z' : ℤ_[p] // ih (n
       rwa [norm_neg, hz.1] at this
     let ⟨q, heq⟩ := calc_eval_z' hnorm rfl hz h1 rfl
     have hnle : ‖F.eval z'‖ ≤ ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ (n + 1) :=
-      calc_eval_z'_norm hnorm hz heq h1 rfl
+      calc_eval_z'_norm hz heq h1 rfl
     ⟨hfeq, hnle⟩⟩
 
 -- Porting note: unsupported option eqn_compiler.zeta
@@ -478,7 +479,7 @@ private theorem a_soln_is_unique (ha : F.eval a = 0) (z' : ℤ_[p]) (hz' : F.eva
       lt_irrefl ‖F.derivative.eval a‖
         (calc
           ‖F.derivative.eval a‖ = ‖q‖ * ‖h‖ := by simp [this]
-          _ ≤ 1 * ‖h‖ := (mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _))
+          _ ≤ 1 * ‖h‖ := by gcongr; apply PadicInt.norm_le_one
           _ < ‖F.derivative.eval a‖ := by simpa
           )
   eq_of_sub_eq_zero (by rw [← this])
diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean
index 305fa72bd4544..4e8de8a551a14 100644
--- a/Mathlib/Topology/ContinuousFunction/Bounded.lean
+++ b/Mathlib/Topology/ContinuousFunction/Bounded.lean
@@ -415,8 +415,8 @@ def comp (G : β → γ) {C : ℝ≥0} (H : LipschitzWith C G) (f : α →ᵇ β
     ⟨max C 0 * D, fun x y =>
       calc
         dist (G (f x)) (G (f y)) ≤ C * dist (f x) (f y) := H.dist_le_mul _ _
-        _ ≤ max C 0 * dist (f x) (f y) := (mul_le_mul_of_nonneg_right (le_max_left C 0) dist_nonneg)
-        _ ≤ max C 0 * D := mul_le_mul_of_nonneg_left (hD _ _) (le_max_right C 0)
+        _ ≤ max C 0 * dist (f x) (f y) := by gcongr; apply le_max_left
+        _ ≤ max C 0 * D := by gcongr; apply hD
         ⟩⟩
 #align bounded_continuous_function.comp BoundedContinuousFunction.comp
 
@@ -427,7 +427,7 @@ theorem lipschitz_comp {G : β → γ} {C : ℝ≥0} (H : LipschitzWith C G) :
     (dist_le (mul_nonneg C.2 dist_nonneg)).2 fun x =>
       calc
         dist (G (f x)) (G (g x)) ≤ C * dist (f x) (g x) := H.dist_le_mul _ _
-        _ ≤ C * dist f g := mul_le_mul_of_nonneg_left (dist_coe_le_dist _) C.2
+        _ ≤ C * dist f g := by gcongr; apply dist_coe_le_dist
 #align bounded_continuous_function.lipschitz_comp BoundedContinuousFunction.lipschitz_comp
 
 /-- The composition operator (in the target) with a Lipschitz map is uniformly continuous. -/
diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
index 783b8b66b8bc0..c89bb1daea2c3 100644
--- a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
+++ b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
@@ -79,8 +79,7 @@ private def maxVar : ℝ≥0 :=
 private theorem one_le_maxVar : 1 ≤ maxVar X Y :=
   calc
     (1 : Real) = 2 * 0 + 1 + 2 * 0 := by simp
-    _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by
-      apply_rules [add_le_add, mul_le_mul_of_nonneg_left, diam_nonneg] <;> norm_num
+    _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by gcongr <;> positivity
 
 /-- The set of functions on `X ⊕ Y` that are candidates distances to realize the
 minimum of the Hausdorff distances between `X` and `Y` in a coupling. -/
@@ -119,8 +118,7 @@ private theorem maxVar_bound : dist x y ≤ maxVar X Y :=
       rw [isometry_inl.diam_range, isometry_inr.diam_range]
       rfl
     _ = 1 * diam (univ : Set X) + 1 + 1 * diam (univ : Set Y) := by simp
-    _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by
-      apply_rules [add_le_add, mul_le_mul_of_nonneg_right, diam_nonneg, le_refl] <;> norm_num
+    _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by gcongr <;> norm_num
 
 private theorem candidates_symm (fA : f ∈ candidates X Y) : f (x, y) = f (y, x) :=
   fA.1.1.1.2 x y
@@ -160,48 +158,40 @@ private theorem candidates_dist_bound (fA : f ∈ candidates X Y) :
       _ = dist (inl x) (inl y) := by
         rw [@Sum.dist_eq X Y]
         rfl
-      _ = 1 * dist (inl x) (inl y) := by simp
-      _ ≤ maxVar X Y * dist (inl x) (inl y) :=
-        mul_le_mul_of_nonneg_right (one_le_maxVar X Y) dist_nonneg
+      _ = 1 * dist (inl x) (inl y) := by ring
+      _ ≤ maxVar X Y * dist (inl x) (inl y) := by gcongr; exact one_le_maxVar X Y
   | inl x, inr y =>
     calc
       f (inl x, inr y) ≤ maxVar X Y := candidates_le_maxVar fA
       _ = maxVar X Y * 1 := by simp
-      _ ≤ maxVar X Y * dist (inl x) (inr y) :=
-        mul_le_mul_of_nonneg_left Sum.one_le_dist_inl_inr (le_trans zero_le_one (one_le_maxVar X Y))
+      _ ≤ maxVar X Y * dist (inl x) (inr y) := by gcongr; apply Sum.one_le_dist_inl_inr
   | inr x, inl y =>
     calc
       f (inr x, inl y) ≤ maxVar X Y := candidates_le_maxVar fA
       _ = maxVar X Y * 1 := by simp
-      _ ≤ maxVar X Y * dist (inl x) (inr y) :=
-        mul_le_mul_of_nonneg_left Sum.one_le_dist_inl_inr (le_trans zero_le_one (one_le_maxVar X Y))
+      _ ≤ maxVar X Y * dist (inl x) (inr y) := by gcongr; apply Sum.one_le_dist_inl_inr
   | inr x, inr y =>
     calc
       f (inr x, inr y) = dist x y := candidates_dist_inr fA x y
       _ = dist (inr x) (inr y) := by
         rw [@Sum.dist_eq X Y]
         rfl
-      _ = 1 * dist (inr x) (inr y) := by simp
-      _ ≤ maxVar X Y * dist (inr x) (inr y) :=
-        mul_le_mul_of_nonneg_right (one_le_maxVar X Y) dist_nonneg
+      _ = 1 * dist (inr x) (inr y) := by ring
+      _ ≤ maxVar X Y * dist (inr x) (inr y) := by gcongr; exact one_le_maxVar X Y
 
 /-- Technical lemma to prove that candidates are Lipschitz -/
 private theorem candidates_lipschitz_aux (fA : f ∈ candidates X Y) :
     f (x, y) - f (z, t) ≤ 2 * maxVar X Y * dist (x, y) (z, t) :=
   calc
-    f (x, y) - f (z, t) ≤ f (x, t) + f (t, y) - f (z, t) :=
-      sub_le_sub_right (candidates_triangle fA) _
-    _ ≤ f (x, z) + f (z, t) + f (t, y) - f (z, t) :=
-      (sub_le_sub_right (add_le_add_right (candidates_triangle fA) _) _)
+    f (x, y) - f (z, t) ≤ f (x, t) + f (t, y) - f (z, t) := by gcongr; exact candidates_triangle fA
+    _ ≤ f (x, z) + f (z, t) + f (t, y) - f (z, t) := by gcongr; exact candidates_triangle fA
     _ = f (x, z) + f (t, y) := by simp [sub_eq_add_neg, add_assoc]
-    _ ≤ maxVar X Y * dist x z + maxVar X Y * dist t y :=
-      (add_le_add (candidates_dist_bound fA) (candidates_dist_bound fA))
+    _ ≤ maxVar X Y * dist x z + maxVar X Y * dist t y := by
+      gcongr <;> apply candidates_dist_bound fA
     _ ≤ maxVar X Y * max (dist x z) (dist t y) + maxVar X Y * max (dist x z) (dist t y) := by
-      apply add_le_add
-      apply mul_le_mul_of_nonneg_left (le_max_left (dist x z) (dist t y))
-        (zero_le_one.trans (one_le_maxVar X Y))
-      apply mul_le_mul_of_nonneg_left (le_max_right (dist x z) (dist t y))
-        (zero_le_one.trans (one_le_maxVar X Y))
+      gcongr
+      · apply le_max_left
+      · apply le_max_right
     _ = 2 * maxVar X Y * max (dist x z) (dist y t) := by
       rw [dist_comm t y]
       ring
@@ -342,7 +332,7 @@ theorem HD_candidatesBDist_le :
       calc
         dist (inl x) (inr (default : Y)) = dist x (default : X) + 1 + dist default default := rfl
         _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
-          apply add_le_add (add_le_add _ le_rfl) <;>
+          gcongr <;>
             exact dist_le_diam_of_mem bounded_of_compactSpace (mem_univ _) (mem_univ _)
     exact le_trans A B
   · have A : (⨅ x, candidatesBDist X Y (inl x, inr y)) ≤ candidatesBDist X Y (inl default, inr y) :=
@@ -351,7 +341,7 @@ theorem HD_candidatesBDist_le :
       calc
         dist (inl (default : X)) (inr y) = dist default default + 1 + dist default y := rfl
         _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
-          apply add_le_add (add_le_add _ le_rfl) <;>
+          gcongr <;>
             exact dist_le_diam_of_mem bounded_of_compactSpace (mem_univ _) (mem_univ _)
     exact le_trans A B
 #align Gromov_Hausdorff.HD_candidates_b_dist_le GromovHausdorff.HD_candidatesBDist_le