[Merged by Bors] - chore(*): use gcongr/grw

Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

@@ -127,7 +127,7 @@ variable {R : Type u} {α : Type*}
 theorem add_one_le_two_mul [LE R] [NonAssocSemiring R] [AddLeftMono R] {a : R}
     (a1 : 1 ≤ a) : a + 1 ≤ 2 * a :=
   calc
-    a + 1 ≤ a + a := add_le_add_left a1 a
+    a + 1 ≤ a + a := by gcongr
     _ = 2 * a := (two_mul _).symm
 
 section OrderedSemiring
@@ -137,8 +137,8 @@ variable [Semiring R] [Preorder R] {a b c d : R}
 theorem add_le_mul_two_add [ZeroLEOneClass R] [MulPosMono R] [AddLeftMono R]
     (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
   calc
-    a + (2 + b) ≤ a + (a + a * b) :=
-      add_le_add_left (add_le_add a2 <| le_mul_of_one_le_left b0 <| one_le_two.trans a2) a
+    a + (2 + b) ≤ a + (a + a * b) := by
+      gcongr; exact le_mul_of_one_le_left b0 <| one_le_two.trans a2
     _ ≤ a * (2 + b) := by rw [mul_add, mul_two, add_assoc]
 
 theorem mul_le_mul_of_nonpos_left [ExistsAddOfLE R] [PosMulMono R]
@@ -148,7 +148,7 @@ theorem mul_le_mul_of_nonpos_left [ExistsAddOfLE R] [PosMulMono R]
   refine le_of_add_le_add_right (a := d * b + d * a) ?_
   calc
     _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
-    _ ≤ d * a := mul_le_mul_of_nonneg_left h <| hcd.trans_le <| add_le_of_nonpos_left hc
+    _ ≤ d * a := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
     _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]
 
 theorem mul_le_mul_of_nonpos_right [ExistsAddOfLE R] [MulPosMono R]
@@ -158,7 +158,7 @@ theorem mul_le_mul_of_nonpos_right [ExistsAddOfLE R] [MulPosMono R]
   refine le_of_add_le_add_right (a := b * d + a * d) ?_
   calc
     _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
-    _ ≤ a * d := mul_le_mul_of_nonneg_right h <| hcd.trans_le <| add_le_of_nonpos_left hc
+    _ ≤ a * d := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
     _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]
 
 theorem mul_nonneg_of_nonpos_of_nonpos [ExistsAddOfLE R] [MulPosMono R]
@@ -169,7 +169,7 @@ theorem mul_nonneg_of_nonpos_of_nonpos [ExistsAddOfLE R] [MulPosMono R]
 theorem mul_le_mul_of_nonneg_of_nonpos [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R]
     [AddRightMono R] [AddRightReflectLE R]
     (hca : c ≤ a) (hbd : b ≤ d) (hc : 0 ≤ c) (hb : b ≤ 0) : a * b ≤ c * d :=
-  (mul_le_mul_of_nonpos_right hca hb).trans <| mul_le_mul_of_nonneg_left hbd hc
+  (mul_le_mul_of_nonpos_right hca hb).trans <| by gcongr; assumption
 
 theorem mul_le_mul_of_nonneg_of_nonpos' [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
     [AddRightMono R] [AddRightReflectLE R]
@@ -375,7 +375,8 @@ lemma mul_add_mul_le_mul_add_mul [ExistsAddOfLE R] [MulPosMono R]
     (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d := by
   obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd
   rw [mul_add, add_right_comm, mul_add, ← add_assoc]
-  exact add_le_add_left (mul_le_mul_of_nonneg_right hab hd) _
+  gcongr
+  assumption
 
 /-- Binary **rearrangement inequality**. -/
 lemma mul_add_mul_le_mul_add_mul' [ExistsAddOfLE R] [MulPosMono R]
@@ -727,8 +728,9 @@ variable [CommSemiring R] [LinearOrder R] {a d : R}
 
 lemma max_mul_mul_le_max_mul_max [PosMulMono R] [MulPosMono R] (b c : R) (ha : 0 ≤ a) (hd : 0 ≤ d) :
     max (a * b) (d * c) ≤ max a c * max d b :=
-  have ba : b * a ≤ max d b * max c a :=
-    mul_le_mul (le_max_right d b) (le_max_right c a) ha (le_trans hd (le_max_left d b))
+  have ba : b * a ≤ max d b * max c a := by
+    gcongr
+    exacts [ha, hd.trans <| le_max_left d b, le_max_right d b, le_max_right c a]
   have cd : c * d ≤ max a c * max b d :=
     mul_le_mul (le_max_right a c) (le_max_right b d) hd (le_trans ha (le_max_left a c))
   max_le (by simpa [mul_comm, max_comm] using ba) (by simpa [mul_comm, max_comm] using cd)

Mathlib/Analysis/Distribution/FourierSchwartz.lean

@@ -57,7 +57,7 @@ noncomputable def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) := by
         (∫ (x : V), (1 + ‖x‖) ^ (- (integrablePower (volume : Measure V) : ℝ))) * 2 *
         ((Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)).sup
           (schwartzSeminormFamily 𝕜 V E)) f := by
-      apply Finset.sum_le_sum (fun p hp ↦ ?_)
+      gcongr with p hp
       simp only [Finset.mem_product, Finset.mem_range] at hp
       apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 _ _ _).trans
       simp only [mul_assoc]

Mathlib/Analysis/Normed/Field/Ultra.lean

@@ -119,15 +119,15 @@ lemma isUltrametricDist_of_forall_norm_natCast_le_one
   rw [← Finset.card_range (m + 1), ← Finset.sum_const, Finset.card_range]
   rcases max_cases 1 (‖x‖ ^ m) with (⟨hm, hx⟩|⟨hm, hx⟩) <;> rw [hm] <;>
   -- which we show by comparing the terms in the sum one by one
-  refine Finset.sum_le_sum fun i hi ↦ ?_
+  gcongr with i hi
   · rcases eq_or_ne m 0 with rfl | hm
     · simp only [pow_zero, le_refl,
         show i = 0 by simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi]
     · rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx
       exact pow_le_one₀ (norm_nonneg _) hx
-  · refine pow_le_pow_right₀ ?_ (by simpa only [Finset.mem_range, Nat.lt_succ] using hi)
-    contrapose! hx
+  · contrapose! hx
     exact pow_le_one₀ (norm_nonneg _) hx.le
+  · simpa [Nat.lt_succ_iff] using hi
 
 end sufficient
 

Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

@@ -122,7 +122,7 @@ theorem smul (c : 𝕜) (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 
   (c • hlf.mk' f).isLinear.with_bound (‖c‖ * M) fun x =>
     calc
       ‖c • f x‖ = ‖c‖ * ‖f x‖ := norm_smul c (f x)
-      _ ≤ ‖c‖ * (M * ‖x‖) := mul_le_mul_of_nonneg_left (hM _) (norm_nonneg _)
+      _ ≤ ‖c‖ * (M * ‖x‖) := by grw [hM]
       _ = ‖c‖ * M * ‖x‖ := (mul_assoc _ _ _).symm
 
 theorem neg (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 fun e => -f e := by

Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

@@ -159,7 +159,7 @@ theorem exists_index_pow_le (hna : IsNonarchimedean p) (x y : R) (n : ℕ) :
     ∃ (m : ℕ), m < n + 1 ∧ p ((x + y) ^ (n : ℕ)) ^ (1 / (n : ℝ)) ≤
       (p (x ^ m) * p (y ^ (n - m : ℕ))) ^ (1 / (n : ℝ)) := by
   obtain ⟨m, hm_lt, hm⟩ := IsNonarchimedean.add_pow_le hna n x y
-  exact ⟨m, hm_lt, Real.rpow_le_rpow (apply_nonneg p _) hm (one_div_nonneg.mpr n.cast_nonneg')⟩
+  exact ⟨m, hm_lt, by gcongr⟩
 
 end CommRing
 
@@ -180,10 +180,7 @@ theorem map_pow_le_pow {F α : Type*} [Ring α] [FunLike F α ℝ] [RingSeminorm
 theorem map_pow_le_pow' {F α : Type*} [Ring α] [FunLike F α ℝ] [RingSeminormClass F α ℝ] {f : F}
     (hf1 : f 1 ≤ 1) (a : α) : ∀ n : ℕ, f (a ^ n) ≤ f a ^ n
   | 0 => by simp only [pow_zero, hf1]
-  | n + 1 => by
-    simp only [pow_succ _ n]
-    exact le_trans (map_mul_le_mul f _ a)
-      (mul_le_mul_of_nonneg_right (map_pow_le_pow' hf1 _ n) (apply_nonneg f a))
+  | n + 1 => map_pow_le_pow _ _ n.succ_ne_zero
 
 /-- The norm of a `NonUnitalSeminormedRing` as a `RingSeminorm`. -/
 def normRingSeminorm (R : Type*) [NonUnitalSeminormedRing R] : RingSeminorm R :=

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -223,7 +223,7 @@ theorem IsBigOWith.rpow (h : IsBigOWith c l f g) (hc : 0 ≤ c) (hr : 0 ≤ r) (
   filter_upwards [hg, h.bound] with x hgx hx
   calc
     |f x ^ r| ≤ |f x| ^ r := abs_rpow_le_abs_rpow _ _
-    _ ≤ (c * |g x|) ^ r := rpow_le_rpow (abs_nonneg _) hx hr
+    _ ≤ (c * |g x|) ^ r := by gcongr; assumption
     _ = c ^ r * |g x ^ r| := by rw [mul_rpow hc (abs_nonneg _), abs_rpow_of_nonneg hgx]
 
 theorem IsBigO.rpow (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) (h : f =O[l] g) :

Mathlib/LinearAlgebra/Matrix/DotProduct.lean

@@ -56,12 +56,12 @@ lemma dotProduct_nonneg_of_nonneg {v w : n → R} (hv : 0 ≤ v) (hw : 0 ≤ w)
   Finset.sum_nonneg (fun i _ => mul_nonneg (hv i) (hw i))
 
 lemma dotProduct_le_dotProduct_of_nonneg_right {u v w : n → R} (huv : u ≤ v) (hw : 0 ≤ w) :
-    u ⬝ᵥ w ≤ v ⬝ᵥ w :=
-  Finset.sum_le_sum fun i _ => mul_le_mul_of_nonneg_right (huv i) (hw i)
+    u ⬝ᵥ w ≤ v ⬝ᵥ w := by
+  unfold dotProduct; gcongr <;> apply_rules
 
 lemma dotProduct_le_dotProduct_of_nonneg_left {u v w : n → R} (huv : u ≤ v) (hw : 0 ≤ w) :
-    w ⬝ᵥ u ≤ w ⬝ᵥ v :=
-  Finset.sum_le_sum (fun i _ => mul_le_mul_of_nonneg_left (huv i) (hw i))
+    w ⬝ᵥ u ≤ w ⬝ᵥ v := by
+  unfold dotProduct; gcongr <;> apply_rules
 
 end OrderedSemiring
 

Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

@@ -185,7 +185,6 @@ theorem eLpNorm_le_eLpNorm_top_mul_eLpNorm (p : ℝ≥0∞) (f : α → E) {g :
   simp only [← ENNReal.mul_rpow_of_nonneg (hz := hp.le)]
   apply lintegral_mono_ae
   filter_upwards [h, enorm_ae_le_eLpNormEssSup f μ] with x hb hf
-  refine ENNReal.rpow_le_rpow ?_ hp.le
   gcongr
   exact hf
 
@@ -210,10 +209,11 @@ theorem eLpNorm'_le_eLpNorm'_mul_eLpNorm' {p q r : ℝ} (hf : AEStronglyMeasurab
     eLpNorm' (fun x => b (f x) (g x)) r μ
       ≤ eLpNorm' (fun x ↦ (c : ℝ) • ‖f x‖ * ‖g x‖) r μ := by
       simp only [eLpNorm']
-      refine (ENNReal.rpow_le_rpow_iff <| one_div_pos.mpr hro_lt).mpr <|
-        lintegral_mono_ae <| h.mono fun a ha ↦ (ENNReal.rpow_le_rpow_iff hro_lt).mpr <| ?_
-      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe, ← NNReal.coe_le_coe]
-      simpa [Real.nnnorm_of_nonneg (by positivity)] using ha
+      gcongr ?_ ^ _
+      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
+      gcongr
+      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]
+      simpa using ha
     _ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by
       simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
       rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]

Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean

@@ -53,7 +53,7 @@ theorem exists_eLpNorm_indicator_le (hp : p ≠ ∞) (c : E) {ε : ℝ≥0∞} (
     simpa only [← ENNReal.coe_rpow_of_nonneg _ hp₀', enorm, ← ENNReal.coe_mul] using hδε' hηδ
   refine ⟨η, hη_pos, fun s hs => ?_⟩
   refine (eLpNorm_indicator_const_le _ _).trans (le_trans ?_ hη_le)
-  exact mul_le_mul_left' (ENNReal.rpow_le_rpow hs hp₀') _
+  gcongr
 
 section Topology
 variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X]

Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

@@ -426,12 +426,13 @@ variable {G' G'' : Type*}
 
 theorem setToSimpleFunc_mono_left {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] G'')
     (hTT' : ∀ s x, T s x ≤ T' s x) (f : α →ₛ F) : setToSimpleFunc T f ≤ setToSimpleFunc T' f := by
-  simp_rw [setToSimpleFunc]; exact sum_le_sum fun i _ => hTT' _ i
+  simp_rw [setToSimpleFunc]; gcongr; apply hTT'
 
 theorem setToSimpleFunc_mono_left' (T T' : Set α → E →L[ℝ] G'')
     (hTT' : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, T s x ≤ T' s x) (f : α →ₛ E)
     (hf : Integrable f μ) : setToSimpleFunc T f ≤ setToSimpleFunc T' f := by
-  refine sum_le_sum fun i _ => ?_
+  unfold setToSimpleFunc
+  gcongr with i _
   by_cases h0 : i = 0
   · simp [h0]
   · exact hTT' _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hf h0) i
@@ -477,7 +478,7 @@ theorem norm_setToSimpleFunc_le_sum_opNorm {m : MeasurableSpace α} (T : Set α
   calc
     ‖∑ x ∈ f.range, T (f ⁻¹' {x}) x‖ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' {x}) x‖ := norm_sum_le _ _
     _ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' {x})‖ * ‖x‖ := by
-      refine Finset.sum_le_sum fun b _ => ?_; simp_rw [ContinuousLinearMap.le_opNorm]
+      gcongr with b; apply ContinuousLinearMap.le_opNorm
 
 theorem norm_setToSimpleFunc_le_sum_mul_norm (T : Set α → F →L[ℝ] F') {C : ℝ}
     (hT_norm : ∀ s, MeasurableSet s → ‖T s‖ ≤ C * μ.real s) (f : α →ₛ F) :

Mathlib/MeasureTheory/Measure/AddContent.lean

@@ -191,8 +191,7 @@ lemma addContent_sUnion_le_sum {m : AddContent C} (hC : IsSetSemiring C)
     simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
     exact (Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2
   rw [h3, addContent_sUnion h1 h2, sum_disjiUnion]
-  · apply sum_le_sum
-    intro x hx
+  · gcongr with x hx
     refine sum_addContent_le_of_subset hC (hC.disjointOfUnion_subset h_ss hx)
       (hC.pairwiseDisjoint_disjointOfUnion_of_mem h_ss hx) (h_ss hx)
       (fun _ s ↦ hC.subset_of_mem_disjointOfUnion h_ss hx s)

Mathlib/ModelTheory/Skolem.lean

@@ -48,7 +48,7 @@ theorem card_functions_sum_skolem₁ :
   simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']
   conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]
   rw [add_comm, add_eq_max, max_eq_left]
-  · refine sum_le_sum _ _ fun n => ?_
+  · gcongr with n
     rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{v}]
     refine ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => ?_⟩⟩
     rcases h with ⟨rfl, ⟨rfl⟩⟩

Mathlib/Probability/StrongLaw.lean

@@ -444,7 +444,7 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) :
     calc
       ∑ i ∈ range N, ℙ {ω | (u i * ε : ℝ) ≤ |S (u i) ω - 𝔼[S (u i)]|} ≤
           ∑ i ∈ range N, ENNReal.ofReal (Var[S (u i)] / (u i * ε) ^ 2) := by
-        refine sum_le_sum fun i _ => ?_
+        gcongr with i _
         apply meas_ge_le_variance_div_sq
         · exact memLp_finset_sum' _ fun j _ => (hident j).aestronglyMeasurable_fst.memLp_truncation
         · apply mul_pos (Nat.cast_pos.2 _) εpos
@@ -459,9 +459,8 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) :
         apply ENNReal.ofReal_le_ofReal
         simp_rw [div_eq_inv_mul, ← inv_pow, mul_inv, mul_comm _ (ε⁻¹), mul_pow, mul_assoc,
           ← mul_sum]
-        refine mul_le_mul_of_nonneg_left ?_ (sq_nonneg _)
-        conv_lhs => enter [2, i]; rw [inv_pow]
-        exact I2 N
+        gcongr
+        simpa only [inv_pow] using I2 N
   have I4 : (∑' i, ℙ {ω | (u i * ε : ℝ) ≤ |S (u i) ω - 𝔼[S (u i)]|}) < ∞ :=
     (le_of_tendsto_of_tendsto' (ENNReal.tendsto_nat_tsum _) tendsto_const_nhds I3).trans_lt
       ENNReal.ofReal_lt_top

Mathlib/SetTheory/Cardinal/Order.lean

@@ -475,6 +475,7 @@ theorem sum_add_distrib' {ι} (f g : ι → Cardinal) :
     (Cardinal.sum fun i => f i + g i) = sum f + sum g :=
   sum_add_distrib f g
 
+@[gcongr]
 theorem sum_le_sum {ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=
   ⟨(Embedding.refl _).sigmaMap fun i =>
       Classical.choice <| by have := H i; rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this⟩