A few more gcongr golfs, probably unrelated

Author: grunweg

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -117,9 +117,10 @@ theorem card_le_mul_sum {x k : ℕ} : #(U x k) ≤ x * ∑ p ∈ P x k, 1 / (p :
   have h : #(P.biUnion N) ≤ ∑ p ∈ P, #(N p) := card_biUnion_le
   calc
     (#(P.biUnion N) : ℝ) ≤ ∑ p ∈ P, (#(N p) : ℝ) := by assumption_mod_cast
-    _ ≤ ∑ p ∈ P, x * (1 / (p : ℝ)) := sum_le_sum fun p _ => ?_
+    _ ≤ ∑ p ∈ P, x * (1 / (p : ℝ)) := by
+      gcongr with p _
+      simp only [N, mul_one_div, Nat.card_multiples, Nat.cast_div_le]
     _ = x * ∑ p ∈ P, 1 / (p : ℝ) := by rw [mul_sum]
-  simp only [N, mul_one_div, Nat.card_multiples, Nat.cast_div_le]
 
 /--
 The number of `e < x` for which `e + 1` is a squarefree product of primes smaller than or equal to

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

@@ -1273,8 +1273,8 @@ lemma div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a /
 @[mono, gcongr, bound]
 lemma div_le_div₀ (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hdb : d ≤ b) : a / b ≤ c / d := by
   rw [div_eq_mul_inv, div_eq_mul_inv]
-  exact mul_le_mul hac ((inv_le_inv₀ (hd.trans_le hdb) hd).2 hdb)
-    (inv_nonneg.2 <| hd.le.trans hdb) hc
+  gcongr
+  exacts [inv_nonneg.2 <| hd.le.trans hdb, hc, hd]
 
 @[gcongr]
 lemma div_lt_div₀ (hac : a < c) (hdb : d ≤ b) (hc : 0 ≤ c) (hd : 0 < d) : a / b < c / d := by

Mathlib/Algebra/Order/Ring/Abs.lean

@@ -173,8 +173,8 @@ private theorem abs_geomSum_le [IsOrderedRing α] : |geomSum a b n| ≤ (n + 1)
   rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]
   refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)
   rw [pow_succ, ← mul_assoc, mul_comm |a|]
-  exact mul_le_mul ih le_sup_left (abs_nonneg _) (mul_nonneg
-    (@Nat.cast_succ α .. ▸ Nat.cast_nonneg _) <| pow_nonneg ((abs_nonneg _).trans le_sup_left) _)
+  gcongr
+  exacts [abs_nonneg _, (abs_nonneg _).trans ih, le_sup_left]
 
 omit [LinearOrder α] in
 private theorem pow_sub_pow_eq_sub_mul_geomSum :

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -307,8 +307,7 @@ theorem norm_iteratedFDerivWithin_prod_le [DecidableEq ι] [NormOneClass A'] {u
       (by simp) (by simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp_assoc]; simp)]
     rw [← Finset.univ_sigma_univ, Finset.sum_sigma, Finset.sum_range]
     simp +instances only [comp_apply, Finset.symInsertEquiv_symm_apply_coe]
-    refine Finset.sum_le_sum ?_
-    intro m _
+    gcongr with m _
     specialize IH hf.2 (n := n - m) (le_trans (by exact_mod_cast n.sub_le m) hn)
     grw [IH]
     rw [Finset.mul_sum, ← Finset.sum_coe_sort]

Mathlib/Analysis/SpecialFunctions/Pochhammer.lean

@@ -59,14 +59,11 @@ lemma monotoneOn_deriv_descPochhammer_eval (n : ℕ) :
     intro a ha b hb hab
     rw [Set.mem_Ioi, Nat.cast_add_one, add_sub_cancel_right] at ha hb
     simp_rw [deriv_descPochhammer_eval_eq_sum_prod_range_erase]
-    apply Finset.sum_le_sum; intro i hi
-    apply Finset.prod_le_prod
-    · intro j hj
-      rw [Finset.mem_erase, Finset.mem_range] at hj
-      apply sub_nonneg_of_le
-      exact ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)
-    · intro j hj
-      rwa [← sub_le_sub_iff_right (j : ℝ)] at hab
+    gcongr with i hi
+    intro j hj
+    rw [Finset.mem_erase, Finset.mem_range] at hj
+    apply sub_nonneg_of_le
+    exact ha.le.trans' (mod_cast Nat.le_pred_of_lt hj.2)
 
 /-- `descPochhammer ℝ n` is convex on `[n-1, ∞)`. -/
 theorem convexOn_descPochhammer_eval (n : ℕ) :

Mathlib/Analysis/SumIntegralComparisons.lean

@@ -93,7 +93,7 @@ theorem AntitoneOn.integral_le_sum (hf : AntitoneOn f (Icc x₀ (x₀ + a))) :
       convert (intervalIntegral.sum_integral_adjacent_intervals hint).symm
       simp only [Nat.cast_zero, add_zero]
     _ ≤ ∑ i ∈ Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + i) := by
-      apply Finset.sum_le_sum fun i hi => ?_
+      gcongr with i hi
       have ia : i < a := Finset.mem_range.1 hi
       refine intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => ?_
       apply hf _ _ hx.1

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -108,7 +108,8 @@ private theorem card_nonuniformWitness_sdiff_biUnion_star (hV : V ∈ P.parts) (
     B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty, m
   · suffices ∀ B ∈ (atomise U <| P.nonuniformWitnesses G ε U).parts,
         #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m by
-      exact sum_le_sum fun B hB => this B <| filter_subset _ _ hB
+      gcongr with B hB
+      exact this B <| filter_subset _ _ hB
     intro B hB
     unfold chunk
     split_ifs with h₁

Mathlib/Data/Finsupp/Order.lean

@@ -88,7 +88,8 @@ lemma sum_le_sum_index [DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → 
   classical
   rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
     sum_of_support_subset _ Finset.subset_union_right _ hh₀]
-  exact Finset.sum_le_sum fun i hi ↦ hh _ hi <| hf _
+  gcongr with i hi
+  exact hh _ hi <| hf _
 
 end Preorder
 

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -127,7 +127,7 @@ theorem card_orderOf_eq_totient_aux₂ {d : ℕ} (hd : d ∣ Fintype.card α) :
         exact mem_erase_of_ne_of_mem hm₂ hm₁
       simp [this, h0]
     _ ≤ ∑ m ∈ c.divisors.erase d, φ m := by
-      refine sum_le_sum fun m hm => ?_
+      gcongr with m hm
       have hmc : m ∣ c := by
         simp only [mem_erase, mem_divisors] at hm
         tauto

Mathlib/NumberTheory/Chebyshev.lean

@@ -223,7 +223,7 @@ theorem abs_psi_sub_theta_le_sqrt_mul_log {x : ℝ} (hx : 1 ≤ x) :
   apply le_trans <| abs_sum_le_sum_abs ..
   simp_rw [abs_of_nonneg <| theta_nonneg _]
   trans ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * x.sqrt
-  · apply sum_le_sum fun i hi ↦ ?_
+  · gcongr with i hi
     apply le_trans (theta_le_log4_mul_x (rpow_nonneg (by linarith) _))
     rw [sqrt_eq_rpow]
     gcongr; simp_all