[Merged by Bors] - feat: golf using gcongr throughout the library

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -262,10 +262,8 @@ theorem IsEquivalent.smul {α E 𝕜 : Type _} [NormedField 𝕜] [NormedAddComm
   refine' hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ _)
   have key :=
     calc
-      ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖ :=
-        mul_le_mul_of_nonneg_right hφx.le (norm_nonneg <| u x)
-      _ ≤ c / 2 / C * (C * ‖v x‖) :=
-        (mul_le_mul_of_nonneg_left hCuvx (div_pos (div_pos hc zero_lt_two) hC).le)
+      ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖ := by gcongr
+      _ ≤ c / 2 / C * (C * ‖v x‖) := by gcongr
       _ = c / 2 * ‖v x‖ := by
         field_simp [hC.ne.symm]
         ring
@@ -274,8 +272,8 @@ theorem IsEquivalent.smul {α E 𝕜 : Type _} [NormedField 𝕜] [NormedAddComm
       simp [sub_smul, sub_add]
     _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := (norm_add_le _ _)
     _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
-    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := (add_le_add_right key _)
-    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := (add_le_add_left huvx _)
+    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
+    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
     _ = c * ‖v x‖ := by ring
 #align asymptotics.is_equivalent.smul Asymptotics.IsEquivalent.smul
 

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -196,7 +196,7 @@ theorem IsBigOWith.weaken (h : IsBigOWith c l f g') (hc : c ≤ c') : IsBigOWith
     mem_of_superset h.bound fun x hx =>
       calc
         ‖f x‖ ≤ c * ‖g' x‖ := hx
-        _ ≤ _ := mul_le_mul_of_nonneg_right hc (norm_nonneg _)
+        _ ≤ _ := by gcongr
 #align asymptotics.is_O_with.weaken Asymptotics.IsBigOWith.weaken
 
 theorem IsBigOWith.exists_pos (h : IsBigOWith c l f g') :
@@ -462,7 +462,7 @@ theorem IsBigOWith.trans (hfg : IsBigOWith c l f g) (hgk : IsBigOWith c' l g k)
   filter_upwards [hfg, hgk]with x hx hx'
   calc
     ‖f x‖ ≤ c * ‖g x‖ := hx
-    _ ≤ c * (c' * ‖k x‖) := (mul_le_mul_of_nonneg_left hx' hc)
+    _ ≤ c * (c' * ‖k x‖) := by gcongr
     _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm
 #align asymptotics.is_O_with.trans Asymptotics.IsBigOWith.trans
 
@@ -1631,8 +1631,7 @@ theorem IsBigOWith.of_pow {n : ℕ} {f : α → 𝕜} {g : α → R} (h : IsBigO
         calc
           ‖f x‖ ^ n = ‖f x ^ n‖ := (norm_pow _ _).symm
           _ ≤ c' ^ n * ‖g x ^ n‖ := hx
-          _ ≤ c' ^ n * ‖g x‖ ^ n :=
-            (mul_le_mul_of_nonneg_left (norm_pow_le' _ hn.bot_lt) (pow_nonneg hc' _))
+          _ ≤ c' ^ n * ‖g x‖ ^ n := by gcongr; exact norm_pow_le' _ hn.bot_lt
           _ = (c' * ‖g x‖) ^ n := (mul_pow _ _ _).symm
 #align asymptotics.is_O_with.of_pow Asymptotics.IsBigOWith.of_pow
 
@@ -1934,7 +1933,7 @@ theorem isBigOWith_of_eq_mul (φ : α → 𝕜) (hφ : ∀ᶠ x in l, ‖φ x‖
   simp only [IsBigOWith_def]
   refine' h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => _)
   simp only [norm_mul, Pi.mul_apply]
-  exact mul_le_mul_of_nonneg_right hx (norm_nonneg _)
+  gcongr
 #align asymptotics.is_O_with_of_eq_mul Asymptotics.isBigOWith_of_eq_mul
 
 theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -127,15 +127,13 @@ theorem Asymptotics.IsLittleO.sum_range {α : Type _} [NormedAddCommGroup α] {f
     _ ≤ ‖∑ i in range N, f i‖ + ∑ i in Ico N n, ε / 2 * g i :=
       (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
     _ ≤ ‖∑ i in range N, f i‖ + ∑ i in range n, ε / 2 * g i := by
-      refine' add_le_add le_rfl _
+      gcongr
       apply sum_le_sum_of_subset_of_nonneg
       · rw [range_eq_Ico]
         exact Ico_subset_Ico (zero_le _) le_rfl
       · intro i _ _
         exact mul_nonneg (half_pos εpos).le (hg i)
-    _ ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i := by
-      rw [← mul_sum]
-      exact add_le_add hn (mul_le_mul_of_nonneg_left le_rfl (half_pos εpos).le)
+    _ ≤ ε / 2 * ‖∑ i in range n, g i‖ + ε / 2 * ∑ i in range n, g i := by rw [← mul_sum]; gcongr
     _ = ε * ‖∑ i in range n, g i‖ := by
       simp only [B]
       ring

Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

@@ -185,7 +185,7 @@ theorem SuperpolynomialDecay.trans_eventually_abs_le (hf : SuperpolynomialDecay
       (eventually_of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => _)
   calc
     |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
-    _ ≤ |k x ^ z| * |f x| := (mul_le_mul le_rfl hx (abs_nonneg _) (abs_nonneg _))
+    _ ≤ |k x ^ z| * |f x| := by gcongr; exact hx
     _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm
 #align asymptotics.superpolynomial_decay.trans_eventually_abs_le Asymptotics.SuperpolynomialDecay.trans_eventually_abs_le
 

Mathlib/Analysis/BoxIntegral/Box/Basic.lean

@@ -9,6 +9,7 @@ Authors: Yury Kudryashov
 ! if you have ported upstream changes.
 -/
 import Mathlib.Data.Set.Intervals.Monotone
+import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.TFAE
 import Mathlib.Topology.Algebra.Order.MonotoneConvergence
 import Mathlib.Topology.MetricSpace.Basic
@@ -535,8 +536,7 @@ theorem diam_Icc_le_of_distortion_le (I : Box ι) (i : ι) {c : ℝ≥0} (h : I.
     calc
       dist x y ≤ dist I.lower I.upper := Real.dist_le_of_mem_pi_Icc hx hy
       _ ≤ I.distortion * (I.upper i - I.lower i) := (I.dist_le_distortion_mul i)
-      _ ≤ c * (I.upper i - I.lower i) :=
-        mul_le_mul_of_nonneg_right h (sub_nonneg.2 (I.lower_le_upper i))
+      _ ≤ c * (I.upper i - I.lower i) := by gcongr; exact sub_nonneg.2 (I.lower_le_upper i)
 #align box_integral.box.diam_Icc_le_of_distortion_le BoxIntegral.Box.diam_Icc_le_of_distortion_le
 
 end Distortion

Mathlib/Analysis/Convex/Star.lean

@@ -394,10 +394,8 @@ theorem starConvex_iff_div : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s →
     ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s :=
   ⟨fun h y hy a b ha hb hab => by
     apply h hy
-    · have ha' := mul_le_mul_of_nonneg_left ha (inv_pos.2 hab).le
-      rwa [MulZeroClass.mul_zero, ← div_eq_inv_mul] at ha'
-    · have hb' := mul_le_mul_of_nonneg_left hb (inv_pos.2 hab).le
-      rwa [MulZeroClass.mul_zero, ← div_eq_inv_mul] at hb'
+    · positivity
+    · positivity
     · rw [← add_div]
       exact div_self hab.ne',
   fun h y hy a b ha hb hab => by
@@ -409,7 +407,7 @@ theorem starConvex_iff_div : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s →
 theorem StarConvex.mem_smul (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
     x ∈ t • s := by
   rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
-  exact hs.smul_mem hx (inv_nonneg.2 <| zero_le_one.trans ht) (inv_le_one ht)
+  exact hs.smul_mem hx (by positivity) (inv_le_one ht)
 #align star_convex.mem_smul StarConvex.mem_smul
 
 end AddCommGroup

Mathlib/Analysis/Hofer.lean

@@ -82,7 +82,7 @@ theorem hofer {X : Type _} [MetricSpace X] [CompleteSpace X] (x : X) (ε : ℝ)
           congr with i
           field_simp
         _ = (∑ i in r, ((1 : ℝ) / 2) ^ i) * ε := Finset.sum_mul.symm
-        _ ≤ 2 * ε := mul_le_mul_of_nonneg_right (sum_geometric_two_le _) (le_of_lt ε_pos)
+        _ ≤ 2 * ε := by gcongr; apply sum_geometric_two_le
     have B : 2 ^ (n + 1) * ϕ x ≤ ϕ (u (n + 1)) := by
       refine' @geom_le (ϕ ∘ u) _ zero_le_two (n + 1) fun m hm => _
       exact (IH _ <| Nat.lt_add_one_iff.1 hm).2.le

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -633,9 +633,7 @@ instance (priority := 100) NormedDivisionRing.to_hasContinuousInv₀ : HasContin
           mul_assoc _ e, inv_mul_cancel r0, mul_inv_cancel e0, one_mul, mul_one]
       -- porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
       _ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp [mul_comm]
-      _ ≤ ‖r - e‖ / ‖r‖ / ε :=
-        div_le_div_of_le_left (div_nonneg (norm_nonneg _) (norm_nonneg _)) ε0 he.le
-
+      _ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
   refine' squeeze_zero' (eventually_of_forall fun _ => norm_nonneg _) this _
   refine' (((continuous_const.sub continuous_id).norm.div_const _).div_const _).tendsto' _ _ _
   simp

Mathlib/Analysis/Normed/Field/InfiniteSum.lean

@@ -85,8 +85,7 @@ theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → R}
   calc
     ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl in antidiagonal n, ‖f kl.1 * g kl.2‖ :=
       norm_sum_le _ _
-    _ ≤ ∑ kl in antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := sum_le_sum fun i _ => norm_mul_le _ _
-
+    _ ≤ ∑ kl in antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le
 #align summable_norm_sum_mul_antidiagonal_of_summable_norm summable_norm_sum_mul_antidiagonal_of_summable_norm
 
 /-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
@@ -118,4 +117,3 @@ theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm [CompleteSpace R] {f g
 #align tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm
 
 end Nat
-

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -812,7 +812,7 @@ attribute [to_additive] LipschitzOnWith.norm_div_le
 @[to_additive]
 theorem LipschitzOnWith.norm_div_le_of_le {f : E → F} {C : ℝ≥0} (h : LipschitzOnWith C f s)
     (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r :=
-  (h.norm_div_le ha hb).trans <| mul_le_mul_of_nonneg_left hr C.2
+  (h.norm_div_le ha hb).trans <| by gcongr
 #align lipschitz_on_with.norm_div_le_of_le LipschitzOnWith.norm_div_le_of_le
 #align lipschitz_on_with.norm_sub_le_of_le LipschitzOnWith.norm_sub_le_of_le
 
@@ -831,7 +831,7 @@ attribute [to_additive] LipschitzWith.norm_div_le
 @[to_additive]
 theorem LipschitzWith.norm_div_le_of_le {f : E → F} {C : ℝ≥0} (h : LipschitzWith C f)
     (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ C * r :=
-  (h.norm_div_le _ _).trans <| mul_le_mul_of_nonneg_left hr C.2
+  (h.norm_div_le _ _).trans <| by gcongr
 #align lipschitz_with.norm_div_le_of_le LipschitzWith.norm_div_le_of_le
 #align lipschitz_with.norm_sub_le_of_le LipschitzWith.norm_sub_le_of_le
 
@@ -1158,8 +1158,7 @@ theorem Filter.Tendsto.op_one_isBoundedUnder_le' {f : α → E} {g : α → F} {
   · exact (mul_nonpos_of_nonpos_of_nonneg (mul_nonpos_of_nonpos_of_nonneg hA <| norm_nonneg' _) <|
       norm_nonneg' _).trans_lt ε₀
   calc
-    A * ‖f i‖ * ‖g i‖ ≤ A * δ * C :=
-      mul_le_mul (mul_le_mul_of_nonneg_left hf.le hA) hg (norm_nonneg' _) (mul_nonneg hA δ₀.le)
+    A * ‖f i‖ * ‖g i‖ ≤ A * δ * C := by gcongr; exact hg
     _ = A * C * δ := (mul_right_comm _ _ _)
     _ < ε := hδ
 #align filter.tendsto.op_one_is_bounded_under_le' Filter.Tendsto.op_one_isBoundedUnder_le'

Mathlib/Analysis/Normed/Group/ControlledClosure.lean

@@ -68,7 +68,7 @@ theorem controlled_closure_of_complete {f : NormedAddGroupHom G H} {K : AddSubgr
     rintro n (hn : n ≥ 1)
     calc
       ‖u n‖ ≤ C * ‖v n‖ := hnorm_u n
-      _ ≤ C * b n := (mul_le_mul_of_nonneg_left (hv _ <| Nat.succ_le_iff.mp hn).le hC.le)
+      _ ≤ C * b n := by gcongr; exact (hv _ <| Nat.succ_le_iff.mp hn).le
       _ = (1 / 2) ^ n * (ε * ‖h‖ / 2) := by simp [mul_div_cancel' _ hC.ne.symm]
       _ = ε * ‖h‖ / 2 * (1 / 2) ^ n := mul_comm _ _
   -- We now show that the limit `g` of `s` is the desired preimage.
@@ -91,26 +91,23 @@ theorem controlled_closure_of_complete {f : NormedAddGroupHom G H} {K : AddSubgr
       have :=
         calc
           ‖v 0‖ ≤ ‖h‖ + ‖v 0 - h‖ := norm_le_insert' _ _
-          _ ≤ ‖h‖ + b 0 := by apply add_le_add_left hv₀.le
+          _ ≤ ‖h‖ + b 0 := by gcongr
       calc
         ‖u 0‖ ≤ C * ‖v 0‖ := hnorm_u 0
-        _ ≤ C * (‖h‖ + b 0) := (mul_le_mul_of_nonneg_left this hC.le)
+        _ ≤ C * (‖h‖ + b 0) := by gcongr
         _ = C * b 0 + C * ‖h‖ := by rw [add_comm, mul_add]
     have : (∑ k in range (n + 1), C * b k) ≤ ε * ‖h‖ :=
       calc
         (∑ k in range (n + 1), C * b k) = (∑ k in range (n + 1), (1 / 2 : ℝ) ^ k) * (ε * ‖h‖ / 2) :=
           by simp only [mul_div_cancel' _ hC.ne.symm, ← sum_mul]
-        _ ≤ 2 * (ε * ‖h‖ / 2) :=
-          (mul_le_mul_of_nonneg_right (sum_geometric_two_le _) (by nlinarith [hε, norm_nonneg h]))
+        _ ≤ 2 * (ε * ‖h‖ / 2) := by gcongr; apply sum_geometric_two_le
         _ = ε * ‖h‖ := mul_div_cancel' _ two_ne_zero
     calc
       ‖s n‖ ≤ ∑ k in range (n + 1), ‖u k‖ := norm_sum_le _ _
       _ = (∑ k in range n, ‖u (k + 1)‖) + ‖u 0‖ := (sum_range_succ' _ _)
-      _ ≤ (∑ k in range n, C * ‖v (k + 1)‖) + ‖u 0‖ :=
-        (add_le_add_right (sum_le_sum fun _ _ => hnorm_u _) _)
-      _ ≤ (∑ k in range n, C * b (k + 1)) + (C * b 0 + C * ‖h‖) :=
-        (add_le_add (sum_le_sum fun k _ => mul_le_mul_of_nonneg_left (hv _ k.succ_pos).le hC.le)
-          hnorm₀)
+      _ ≤ (∑ k in range n, C * ‖v (k + 1)‖) + ‖u 0‖ := by gcongr; apply hnorm_u
+      _ ≤ (∑ k in range n, C * b (k + 1)) + (C * b 0 + C * ‖h‖) := by
+        gcongr with k; exact (hv _ k.succ_pos).le
       _ = (∑ k in range (n + 1), C * b k) + C * ‖h‖ := by rw [← add_assoc, sum_range_succ']
       _ ≤ (C + ε) * ‖h‖ := by
         rw [add_comm, add_mul]

Mathlib/Analysis/Normed/Group/Hom.lean

@@ -73,7 +73,7 @@ theorem exists_pos_bound_of_bound {V W : Type _} [SeminormedAddCommGroup V]
   ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), fun x =>
     calc
       ‖f x‖ ≤ M * ‖x‖ := h x
-      _ ≤ max M 1 * ‖x‖ := mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _)
+      _ ≤ max M 1 * ‖x‖ := by gcongr; apply le_max_left
       ⟩
 #align exists_pos_bound_of_bound exists_pos_bound_of_bound
 
@@ -189,7 +189,7 @@ theorem SurjectiveOnWith.mono {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup
   use g, rfl
   by_cases Hg : ‖f g‖ = 0
   · simpa [Hg] using hg
-  · exact hg.trans ((mul_le_mul_right <| (Ne.symm Hg).le_iff_lt.mp (norm_nonneg _)).mpr H)
+  · exact hg.trans (by gcongr)
 #align normed_add_group_hom.surjective_on_with.mono NormedAddGroupHom.SurjectiveOnWith.mono
 
 theorem SurjectiveOnWith.exists_pos {f : NormedAddGroupHom V₁ V₂} {K : AddSubgroup V₂} {C : ℝ}
@@ -251,11 +251,11 @@ theorem le_opNorm (x : V₁) : ‖f x‖ ≤ ‖f‖ * ‖x‖ := by
 #align normed_add_group_hom.le_op_norm NormedAddGroupHom.le_opNorm
 
 theorem le_opNorm_of_le {c : ℝ} {x} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖f‖ * c :=
-  le_trans (f.le_opNorm x) (mul_le_mul_of_nonneg_left h f.opNorm_nonneg)
+  le_trans (f.le_opNorm x) (by gcongr; exact f.opNorm_nonneg)
 #align normed_add_group_hom.le_op_norm_of_le NormedAddGroupHom.le_opNorm_of_le
 
 theorem le_of_opNorm_le {c : ℝ} (h : ‖f‖ ≤ c) (x : V₁) : ‖f x‖ ≤ c * ‖x‖ :=
-  (f.le_opNorm x).trans (mul_le_mul_of_nonneg_right h (norm_nonneg x))
+  (f.le_opNorm x).trans (by gcongr)
 #align normed_add_group_hom.le_of_op_norm_le NormedAddGroupHom.le_of_opNorm_le
 
 /-- continuous linear maps are Lipschitz continuous. -/
@@ -315,7 +315,7 @@ given to the constructor or zero if this bound is negative. -/
 theorem mkNormedAddGroupHom_norm_le' (f : V₁ →+ V₂) {C : ℝ} (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
     ‖f.mkNormedAddGroupHom C h‖ ≤ max C 0 :=
   opNorm_le_bound _ (le_max_right _ _) fun x =>
-    (h x).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg x)
+    (h x).trans <| by gcongr; apply le_max_left
 #align normed_add_group_hom.mk_normed_add_group_hom_norm_le' NormedAddGroupHom.mkNormedAddGroupHom_norm_le'
 
 alias mkNormedAddGroupHom_norm_le ← _root_.AddMonoidHom.mkNormedAddGroupHom_norm_le
@@ -333,7 +333,7 @@ instance add : Add (NormedAddGroupHom V₁ V₂) :=
     (f.toAddMonoidHom + g.toAddMonoidHom).mkNormedAddGroupHom (‖f‖ + ‖g‖) fun v =>
       calc
         ‖f v + g v‖ ≤ ‖f v‖ + ‖g v‖ := norm_add_le _ _
-        _ ≤ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ := (add_le_add (le_opNorm f v) (le_opNorm g v))
+        _ ≤ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ := by gcongr <;> apply le_opNorm
         _ = (‖f‖ + ‖g‖) * ‖v‖ := by rw [add_mul]
         ⟩
 
@@ -512,7 +512,7 @@ instance smul : SMul R (NormedAddGroupHom V₁ V₂) where
           rw [map_zero, smul_zero, dist_zero_right, dist_zero_right] at this
           rw [mul_assoc]
           refine' this.trans _
-          refine' mul_le_mul_of_nonneg_left _ dist_nonneg
+          gcongr
           exact hb x⟩ }
 
 @[simp]
@@ -547,7 +547,7 @@ instance nsmul : SMul ℕ (NormedAddGroupHom V₁ V₂) where
         let ⟨b, hb⟩ := f.bound'
         ⟨n • b, fun v => by
           rw [Pi.smul_apply, nsmul_eq_mul, mul_assoc]
-          exact (norm_nsmul_le _ _).trans (mul_le_mul_of_nonneg_left (hb _) (Nat.cast_nonneg _))⟩ }
+          exact (norm_nsmul_le _ _).trans (by gcongr; apply hb)⟩ }
 #align normed_add_group_hom.has_nat_scalar NormedAddGroupHom.nsmul
 
 @[simp]
@@ -568,7 +568,7 @@ instance zsmul : SMul ℤ (NormedAddGroupHom V₁ V₂) where
         let ⟨b, hb⟩ := f.bound'
         ⟨‖z‖ • b, fun v => by
           rw [Pi.smul_apply, smul_eq_mul, mul_assoc]
-          exact (norm_zsmul_le _ _).trans (mul_le_mul_of_nonneg_left (hb _) <| norm_nonneg _)⟩ }
+          exact (norm_zsmul_le _ _).trans (by gcongr; apply hb)⟩ }
 #align normed_add_group_hom.has_int_scalar NormedAddGroupHom.zsmul
 
 @[simp]
@@ -650,7 +650,7 @@ protected def comp (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V₁
   (g.toAddMonoidHom.comp f.toAddMonoidHom).mkNormedAddGroupHom (‖g‖ * ‖f‖) fun v =>
     calc
       ‖g (f v)‖ ≤ ‖g‖ * ‖f v‖ := le_opNorm _ _
-      _ ≤ ‖g‖ * (‖f‖ * ‖v‖) := (mul_le_mul_of_nonneg_left (le_opNorm _ _) (opNorm_nonneg _))
+      _ ≤ ‖g‖ * (‖f‖ * ‖v‖) := by gcongr; apply le_opNorm
       _ = ‖g‖ * ‖f‖ * ‖v‖ := by rw [mul_assoc]
 #align normed_add_group_hom.comp NormedAddGroupHom.comp
 
@@ -661,7 +661,7 @@ theorem norm_comp_le (g : NormedAddGroupHom V₂ V₃) (f : NormedAddGroupHom V
 
 theorem norm_comp_le_of_le {g : NormedAddGroupHom V₂ V₃} {C₁ C₂ : ℝ} (hg : ‖g‖ ≤ C₂)
     (hf : ‖f‖ ≤ C₁) : ‖g.comp f‖ ≤ C₂ * C₁ :=
-  le_trans (norm_comp_le g f) <| mul_le_mul hg hf (norm_nonneg _) (le_trans (norm_nonneg _) hg)
+  le_trans (norm_comp_le g f) <| by gcongr; exact le_trans (norm_nonneg _) hg
 #align normed_add_group_hom.norm_comp_le_of_le NormedAddGroupHom.norm_comp_le_of_le
 
 theorem norm_comp_le_of_le' {g : NormedAddGroupHom V₂ V₃} (C₁ C₂ C₃ : ℝ) (h : C₃ = C₂ * C₁)

Mathlib/Analysis/Normed/Group/HomCompletion.lean

@@ -187,12 +187,12 @@ theorem NormedAddGroupHom.ker_completion {f : NormedAddGroupHom G H} {C : ℝ}
   refine ⟨_, ⟨⟨g - g', mem_ker⟩, rfl⟩, ?_⟩
   have : ‖f g‖ ≤ ‖f‖ * δ
   calc ‖f g‖ ≤ ‖f‖ * ‖hatg - g‖ := by simpa [hatg_in] using f.completion.le_opNorm (hatg - g)
-    _ ≤ ‖f‖ * δ := mul_le_mul_of_nonneg_left hg.le (norm_nonneg f)
+    _ ≤ ‖f‖ * δ := by gcongr
   calc ‖hatg - ↑(g - g')‖ = ‖hatg - g + g'‖ := by rw [Completion.coe_sub, sub_add]
     _ ≤ ‖hatg - g‖ + ‖(g' : Completion G)‖ := norm_add_le _ _
     _ = ‖hatg - g‖ + ‖g'‖ := by rw [Completion.norm_coe]
     _ < δ + C' * ‖f g‖ := add_lt_add_of_lt_of_le hg hfg
-    _ ≤ δ + C' * (‖f‖ * δ) := add_le_add_left (mul_le_mul_of_nonneg_left this C'_pos.le) _
+    _ ≤ δ + C' * (‖f‖ * δ) := by gcongr
     _ < ε := by simpa only [add_mul, one_mul, mul_assoc] using hδ
 #align normed_add_group_hom.ker_completion NormedAddGroupHom.ker_completion