chore(*): use gcongr (#24720)

Also add a few missing `gcongr` lemmas.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: Parcly-Taxel

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating
 import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.Data.Nat.Fib.Basic
 import Mathlib.Tactic.Monotonicity
+import Mathlib.Tactic.GCongr
 
 /-!
 # Approximations for Continued Fraction Computations (`GenContFract.of`)
@@ -230,16 +231,14 @@ theorem fib_le_of_contsAux_b :
         -- use the IH to get the inequalities for `pconts` and `ppconts`
         have ppred_nth_fib_le_ppconts_B : (fib n : K) ≤ ppconts.b :=
           IH n (lt_trans (Nat.lt.base n) <| Nat.lt.base <| n + 1) (Or.inr not_terminatedAt_ppred_n)
-        suffices (fib (n + 1) : K) ≤ gp.b * pconts.b by
-          solve_by_elim [_root_.add_le_add ppred_nth_fib_le_ppconts_B]
+        suffices (fib (n + 1) : K) ≤ gp.b * pconts.b by gcongr
         -- finally use the fact that `1 ≤ gp.b` to solve the goal
         suffices 1 * (fib (n + 1) : K) ≤ gp.b * pconts.b by rwa [one_mul] at this
         have one_le_gp_b : (1 : K) ≤ gp.b :=
           of_one_le_get?_partDen (partDen_eq_s_b s_ppred_nth_eq)
-        have : (0 : K) ≤ fib (n + 1) := mod_cast (fib (n + 1)).zero_le
-        have : (0 : K) ≤ gp.b := le_trans zero_le_one one_le_gp_b
-        mono
-        · norm_num
+        gcongr
+        apply IH
+        · simp
         · tauto)
 
 /-- Shows that the `n`th denominator is greater than or equal to the `n + 1`th fibonacci number,
@@ -465,13 +464,12 @@ theorem abs_sub_convs_le (not_terminatedAt_n : ¬(of v).TerminatedAt n) :
       nextConts_b_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _
     solve_by_elim [mul_pos]
   · -- we can cancel multiplication by `conts.b` and addition with `pred_conts.b`
-    suffices gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b from
-      (mul_le_mul_left zero_lt_conts_b).2 <| (add_le_add_iff_left pred_conts.b).2 this
+    suffices gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b by
+      simp only [den, den']; gcongr
     suffices (ifp_succ_n.b : K) * conts.b ≤ ifp_n.fr⁻¹ * conts.b by rwa [← ifp_succ_n_b_eq_gp_b]
     have : (ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹ :=
       IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv stream_nth_eq succ_nth_stream_eq
-    have : 0 ≤ conts.b := le_of_lt zero_lt_conts_b
-    gcongr; exact this
+    gcongr
 
 /-- Shows that `|v - Aₙ / Bₙ| ≤ 1 / (bₙ * Bₙ * Bₙ)`. This bound is worse than the one shown in
 `GenContFract.abs_sub_convs_le`, but sometimes it is easier to apply and
@@ -492,7 +490,8 @@ theorem abs_sub_convergents_le' {b : K}
     · have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_partDen nth_partDen_eq)
       apply_rules [mul_pos]
     · conv_rhs => rw [mul_comm]
-      exact mul_le_mul_of_nonneg_right (le_of_succ_get?_den nth_partDen_eq) hB.le
+      gcongr
+      exact le_of_succ_get?_den nth_partDen_eq
 
 end ErrorTerm
 

Mathlib/Algebra/Polynomial/FieldDivision.lean

@@ -21,6 +21,7 @@ This file starts looking like the ring theory of $R[X]$
 noncomputable section
 
 open Polynomial
+open scoped Nat
 
 namespace Polynomial
 
@@ -84,7 +85,7 @@ theorem lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors
   by_contra! h'
   replace hroot := hroot _ h'
   simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot
-  obtain ⟨q, hq⟩ := Nat.cast_dvd_cast (α := R) <| Nat.factorial_dvd_factorial h'
+  obtain ⟨q, hq⟩ : ((rootMultiplicity t p)! : R) ∣ n ! := by gcongr
   rw [hq, mul_mem_nonZeroDivisors] at hnzd
   rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot
   exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot

Mathlib/Analysis/Asymptotics/ExpGrowth.lean

@@ -75,9 +75,8 @@ lemma expGrowthSup_monotone : Monotone expGrowthSup :=
 lemma expGrowthInf_le_expGrowthSup : expGrowthInf u ≤ expGrowthSup u := liminf_le_limsup
 
 lemma expGrowthInf_le_expGrowthSup_of_frequently_le (h : ∃ᶠ n in atTop, u n ≤ v n) :
-    expGrowthInf u ≤ expGrowthSup v := by
-  refine (liminf_le_limsup_of_frequently_le) (h.mono fun n u_v ↦ ?_)
-  exact div_le_div_right_of_nonneg n.cast_nonneg' (log_monotone u_v)
+    expGrowthInf u ≤ expGrowthSup v :=
+  liminf_le_limsup_of_frequently_le <| h.mono fun n u_v ↦ by gcongr
 
 lemma expGrowthInf_le_iff :
     expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ n : ℕ in atTop, u n ≤ exp (b * n) := by
@@ -130,22 +129,19 @@ lemma frequently_exp_le (h : a < expGrowthSup u) :
 lemma _root_.Frequently.expGrowthInf_le (h : ∃ᶠ n : ℕ in atTop, u n ≤ exp (a * n)) :
     expGrowthInf u ≤ a := by
   apply expGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
-  exact exp_monotone (mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg')
+  gcongr
 
 lemma _root_.Eventually.le_expGrowthInf (h : ∀ᶠ n : ℕ in atTop, exp (a * n) ≤ u n) :
-    a ≤ expGrowthInf u := by
-  apply le_expGrowthInf_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' ?_
-  exact exp_monotone (mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg')
+    a ≤ expGrowthInf u :=
+  le_expGrowthInf_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr
 
 lemma _root_.Eventually.expGrowthSup_le (h : ∀ᶠ n : ℕ in atTop, u n ≤ exp (a * n)) :
-    expGrowthSup u ≤ a:= by
-  apply expGrowthSup_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
-  exact exp_monotone (mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg')
+    expGrowthSup u ≤ a :=
+  expGrowthSup_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans <| by gcongr
 
 lemma _root_.Frequently.le_expGrowthSup (h : ∃ᶠ n : ℕ in atTop, exp (a * n) ≤ u n) :
-    a ≤ expGrowthSup u := by
-  apply le_expGrowthSup_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' ?_
-  exact exp_monotone (mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg')
+    a ≤ expGrowthSup u :=
+  le_expGrowthSup_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr
 
 /-! ### Special cases -/
 

Mathlib/Analysis/Asymptotics/LinearGrowth.lean

@@ -135,31 +135,27 @@ lemma frequently_mul_le (h : a < linearGrowthSup u) :
   le_linearGrowthSup_iff.1 (le_refl (linearGrowthSup u)) a h
 
 lemma _root_.Frequently.linearGrowthInf_le (h : ∃ᶠ n : ℕ in atTop, u n ≤ a * n) :
-    linearGrowthInf u ≤ a := by
-  apply linearGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
-  exact mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg'
+    linearGrowthInf u ≤ a :=
+  linearGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans <| by gcongr
 
 lemma _root_.Eventually.le_linearGrowthInf (h : ∀ᶠ n : ℕ in atTop, a * n ≤ u n) :
-    a ≤ linearGrowthInf u := by
-  apply le_linearGrowthInf_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' ?_
-  exact mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg'
+    a ≤ linearGrowthInf u :=
+  le_linearGrowthInf_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr
 
 lemma _root_.Eventually.linearGrowthSup_le (h : ∀ᶠ n : ℕ in atTop, u n ≤ a * n) :
-    linearGrowthSup u ≤ a:= by
-  apply linearGrowthSup_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans ?_
-  exact mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg'
+    linearGrowthSup u ≤ a:=
+  linearGrowthSup_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans <| by gcongr
 
 lemma _root_.Frequently.le_linearGrowthSup (h : ∃ᶠ n : ℕ in atTop, a * n ≤ u n) :
-    a ≤ linearGrowthSup u := by
-  apply le_linearGrowthSup_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' ?_
-  exact mul_le_mul_of_nonneg_right c_u.le n.cast_nonneg'
+    a ≤ linearGrowthSup u :=
+  le_linearGrowthSup_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr
 
 /-! ### Special cases -/
 
 lemma linearGrowthSup_bot : linearGrowthSup (⊥ : ℕ → EReal) = (⊥ : EReal) := by
   nth_rw 2 [← limsup_const (f := atTop (α := ℕ)) ⊥]
-  refine limsup_congr (eventually_atTop.2 ?_)
-  exact ⟨1, fun n n_pos ↦ bot_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩
+  refine limsup_congr <| (eventually_gt_atTop 0).mono fun n n_pos ↦ ?_
+  exact bot_div_of_pos_ne_top (by positivity) (natCast_ne_top n)
 
 lemma linearGrowthInf_bot : linearGrowthInf (⊥ : ℕ → EReal) = (⊥ : EReal) := by
   apply le_bot_iff.1
@@ -400,7 +396,7 @@ lemma le_linearGrowthInf_comp (hu : 0 ≤ᶠ[atTop] u) (hv : Tendsto v atTop atT
     with n b_uvn a_vn n_0
   replace a_vn := ((lt_div_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn).le
   rw [comp_apply, mul_comm a b, mul_assoc b a]
-  exact b_uvn.trans' (mul_le_mul_of_nonneg_left a_vn b_0.le)
+  exact b_uvn.trans' <| by gcongr
 
 lemma linearGrowthSup_comp_le (hu : ∃ᶠ n in atTop, 0 ≤ u n)
     (hv₀ : (linearGrowthSup fun n ↦ v n : EReal) ≠ 0)
@@ -418,7 +414,7 @@ lemma linearGrowthSup_comp_le (hu : ∃ᶠ n in atTop, 0 ≤ u n)
     with n uvn_b vn_a n_0
   replace vn_a := ((div_lt_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 vn_a).le
   rw [comp_apply, mul_comm a b, mul_assoc b a]
-  exact uvn_b.trans (mul_le_mul_of_nonneg_left vn_a b_0)
+  exact uvn_b.trans <| by gcongr
 
 /-! ### Monotone sequences -/
 
@@ -490,12 +486,12 @@ lemma _root_.Monotone.linearGrowthInf_comp_le (h : Monotone u)
   refine ⟨k, ?_, fun vk_ak' ↦ ?_⟩
   · rw [mul_comm a, ← le_div_iff_mul_le a_0 a_top, EReal.div_eq_inv_mul] at aM_M'
     apply Nat.cast_le.1 <| aM_M'.trans <| an_k.trans' _
-    exact mul_le_mul_of_nonneg_left (Nat.cast_le.2 n_M') (inv_nonneg_of_nonneg a_0.le)
+    gcongr
   · rw [comp_apply, mul_comm a b, mul_assoc b a]
     rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0' (ne_top_of_lt a_a'), mul_comm] at k_an'
     rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0 a_top] at an_k
     have vk_n := Nat.cast_le.1 (vk_ak'.trans k_an')
-    exact (h vk_n).trans <| un_bn.trans (mul_le_mul_of_nonneg_left an_k b_0.le)
+    exact (h vk_n).trans <| un_bn.trans <| by gcongr
 
 lemma _root_.Monotone.le_linearGrowthSup_comp (h : Monotone u)
     (hv : (linearGrowthInf fun n ↦ v n : EReal) ≠ 0) :
@@ -531,12 +527,12 @@ lemma _root_.Monotone.le_linearGrowthSup_comp (h : Monotone u)
   refine ⟨k, ?_, fun ak_vk' ↦ ?_⟩
   · rw [mul_comm a', ← le_div_iff_mul_le a_0' a_top', EReal.div_eq_inv_mul] at aM_M'
     apply Nat.cast_le.1 <| aM_M'.trans <| an_k'.trans' _
-    exact mul_le_mul_of_nonneg_left (Nat.cast_le.2 n_M') (inv_nonneg_of_nonneg a_0'.le)
+    gcongr
   · rw [comp_apply, mul_comm a b, mul_assoc b a]
     rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0' a_top'] at an_k'
     rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0 (ne_top_of_lt a_a'), mul_comm] at k_an
     have n_vk := Nat.cast_le.1 (an_k'.trans ak_vk')
-    exact (mul_le_mul_of_nonneg_left k_an b_0.le).trans <| bn_un.trans (h n_vk)
+    exact le_trans (by gcongr) <| bn_un.trans (h n_vk)
 
 lemma _root_.Monotone.linearGrowthInf_comp {a : EReal} (h : Monotone u)
     (hv : Tendsto (fun n ↦ (v n : EReal) / n) atTop (𝓝 a)) (ha : a ≠ 0) (ha' : a ≠ ⊤) :

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -347,7 +347,8 @@ theorem norm_integral_le_of_norm_le {g : ℝⁿ → ℝ} (hle : ∀ x ∈ Box.Ic
     refine norm_sum_le_of_le _ fun J _ => ?_
     simp only [BoxAdditiveMap.toSMul_apply, norm_smul, smul_eq_mul, Real.norm_eq_abs,
       μ.toBoxAdditive_apply, abs_of_nonneg measureReal_nonneg]
-    exact mul_le_mul_of_nonneg_left (hle _ <| π.tag_mem_Icc _) ENNReal.toReal_nonneg
+    gcongr
+    exact hle _ <| π.tag_mem_Icc _
   · rw [integral, dif_neg hfi, norm_zero]
     exact integral_nonneg (fun x hx => (norm_nonneg _).trans (hle x hx)) μ
 
@@ -681,7 +682,7 @@ theorem integrable_of_bounded_and_ae_continuousWithinAt [CompleteSpace E] {I : B
       intro J hJ
       rw [mem_sdiff, B.mem_filter, not_and] at hJ
       rw [norm_smul, μ.toBoxAdditive_apply, Real.norm_of_nonneg measureReal_nonneg]
-      refine mul_le_mul_of_nonneg_left ?_ toReal_nonneg
+      gcongr _ * ?_
       obtain ⟨x, xJ, xnU⟩ : ∃ x ∈ J, x ∉ U := Set.not_subset.1 (hJ.2 hJ.1)
       have hx : x ∈ Box.Icc I \ U := ⟨Box.coe_subset_Icc ((le_of_mem' _ J hJ.1) xJ), xnU⟩
       have ineq : edist (f (t₁ J)) (f (t₂ J)) ≤ EMetric.diam (f '' (ball x r ∩ (Box.Icc I))) := by

Mathlib/Analysis/Convex/Integral.lean

@@ -285,9 +285,9 @@ theorem StrictConvexOn.ae_eq_const_or_map_average_lt [IsFiniteMeasure μ] (hg :
     g ((a • ⨍ x in t, f x ∂μ) + b • ⨍ x in tᶜ, f x ∂μ) <
         a * g (⨍ x in t, f x ∂μ) + b * g (⨍ x in tᶜ, f x ∂μ) :=
       hg.2 (this h₀).1 (this h₀').1 hne ha hb hab
-    _ ≤ (a * ⨍ x in t, g (f x) ∂μ) + b * ⨍ x in tᶜ, g (f x) ∂μ :=
-      add_le_add (mul_le_mul_of_nonneg_left (this h₀).2 ha.le)
-        (mul_le_mul_of_nonneg_left (this h₀').2 hb.le)
+    _ ≤ (a * ⨍ x in t, g (f x) ∂μ) + b * ⨍ x in tᶜ, g (f x) ∂μ := by
+      gcongr
+      exacts [(this h₀).2, (this h₀').2]
 
 /-- **Jensen's inequality**, strict version: if an integrable function `f : α → E` takes values in a
 convex closed set `s`, and `g : E → ℝ` is continuous and strictly concave on `s`, then

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -170,7 +170,7 @@ theorem decay_add_le_aux (k n : ℕ) (f g : 𝓢(E, F)) (x : E) :
     ‖x‖ ^ k * ‖iteratedFDeriv ℝ n ((f : E → F) + (g : E → F)) x‖ ≤
       ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n g x‖ := by
   rw [← mul_add]
-  refine mul_le_mul_of_nonneg_left ?_ (by positivity)
+  gcongr _ * ?_
   rw [iteratedFDeriv_add_apply (f.smooth _).contDiffAt (g.smooth _).contDiffAt]
   exact norm_add_le _ _
 
@@ -219,15 +219,13 @@ instance instSMul : SMul 𝕜 𝓢(E, F) :=
   ⟨fun c f =>
     { toFun := c • (f : E → F)
       smooth' := (f.smooth _).const_smul c
-      decay' := fun k n => by
-        refine ⟨f.seminormAux k n * (‖c‖ + 1), fun x => ?_⟩
-        have hc : 0 ≤ ‖c‖ := by positivity
-        refine le_trans ?_ ((mul_le_mul_of_nonneg_right (f.le_seminormAux k n x) hc).trans ?_)
-        · apply Eq.le
+      decay' k n := .intro (f.seminormAux k n * ‖c‖) fun x ↦ calc
+        ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ * ‖c‖ := by
           rw [mul_comm _ ‖c‖, ← mul_assoc]
           exact decay_smul_aux k n f c x
-        · apply mul_le_mul_of_nonneg_left _ (f.seminormAux_nonneg k n)
-          linarith }⟩
+        _ ≤ SchwartzMap.seminormAux k n f * ‖c‖ := by
+          gcongr
+          apply f.le_seminormAux }⟩
 
 @[simp]
 theorem smul_apply {f : 𝓢(E, F)} {c : 𝕜} {x : E} : (c • f) x = c • f x :=
@@ -241,9 +239,8 @@ instance instSMulCommClass [SMulCommClass 𝕜 𝕜' F] : SMulCommClass 𝕜 
 
 theorem seminormAux_smul_le (k n : ℕ) (c : 𝕜) (f : 𝓢(E, F)) :
     (c • f).seminormAux k n ≤ ‖c‖ * f.seminormAux k n := by
-  refine
-    (c • f).seminormAux_le_bound k n (mul_nonneg (norm_nonneg _) (seminormAux_nonneg _ _ _))
-      fun x => (decay_smul_aux k n f c x).le.trans ?_
+  refine (c • f).seminormAux_le_bound k n (mul_nonneg (norm_nonneg _) (seminormAux_nonneg _ _ _))
+      fun x => (decay_smul_aux k n f c x).trans_le ?_
   rw [mul_assoc]
   exact mul_le_mul_of_nonneg_left (f.le_seminormAux k n x) (norm_nonneg _)
 
@@ -686,7 +683,7 @@ theorem _root_.MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top (p
         simp only [ENNReal.coe_toReal]
         refine Eq.subst (motive := (∫⁻ x, · x ∂μ < ⊤)) (funext fun x ↦ ?_) this
         rw [← neg_mul, Real.rpow_mul (h_one_add x).le]
-        exact Real.enorm_rpow_of_nonneg (Real.rpow_nonneg (h_one_add x).le _) NNReal.zero_le_coe
+        exact Real.enorm_rpow_of_nonneg (by positivity) NNReal.zero_le_coe
       refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)
       rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]
       gcongr

Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

@@ -239,18 +239,16 @@ induced by `PiTensorProduct.lift`, for every normed space `F`.
 -/
 @[simps]
 noncomputable def liftEquiv : ContinuousMultilinearMap 𝕜 E F ≃ₗ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F where
-  toFun f := LinearMap.mkContinuous (lift f.toMultilinearMap) ‖f‖
-    (fun x ↦ norm_eval_le_injectiveSeminorm f x)
+  toFun f := LinearMap.mkContinuous (lift f.toMultilinearMap) ‖f‖ fun x ↦
+    norm_eval_le_injectiveSeminorm f x
   map_add' f g := by ext _; simp only [ContinuousMultilinearMap.toMultilinearMap_add, map_add,
     LinearMap.mkContinuous_apply, LinearMap.add_apply, ContinuousLinearMap.add_apply]
   map_smul' a f := by ext _; simp only [ContinuousMultilinearMap.toMultilinearMap_smul, map_smul,
     LinearMap.mkContinuous_apply, LinearMap.smul_apply, RingHom.id_apply,
     ContinuousLinearMap.coe_smul', Pi.smul_apply]
-  invFun l := MultilinearMap.mkContinuous (lift.symm l.toLinearMap) ‖l‖ (fun x ↦ by
+  invFun l := MultilinearMap.mkContinuous (lift.symm l.toLinearMap) ‖l‖ fun x ↦ by
     simp only [lift_symm, LinearMap.compMultilinearMap_apply, ContinuousLinearMap.coe_coe]
-    refine le_trans (ContinuousLinearMap.le_opNorm _ _) (mul_le_mul_of_nonneg_left ?_
-      (norm_nonneg l))
-    exact injectiveSeminorm_tprod_le x)
+    exact ContinuousLinearMap.le_opNorm_of_le _ (injectiveSeminorm_tprod_le x)
   left_inv f := by ext x; simp only [LinearMap.mkContinuous_coe, LinearEquiv.symm_apply_apply,
       MultilinearMap.coe_mkContinuous, ContinuousMultilinearMap.coe_coe]
   right_inv l := by

Mathlib/Analysis/ODE/PicardLindelof.lean

@@ -199,7 +199,7 @@ protected theorem mem_closedBall (t : Icc v.tMin v.tMax) : f t ∈ closedBall v.
   calc
     dist (f t) v.x₀ = dist (f t) (f.toFun v.t₀) := by rw [f.map_t₀']
     _ ≤ v.C * dist t v.t₀ := f.lipschitz.dist_le_mul _ _
-    _ ≤ v.C * v.tDist := mul_le_mul_of_nonneg_left (v.dist_t₀_le _) v.C.2
+    _ ≤ v.C * v.tDist := by gcongr; apply v.dist_t₀_le
     _ ≤ v.R := v.isPicardLindelof.C_mul_le_R
 
 /-- Given a curve $γ \colon [t_{\min}, t_{\max}] → E$, `PicardLindelof.vComp` is the function