chore: more uses of calc and gcongr (#19173)

Motivated by the deprecation in #19081

Author: YaelDillies

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

@@ -1033,6 +1033,9 @@ theorem pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n, a ^ n ≤ b ^
   | n + 1 => by simpa only [pow_succ']
       using mul_le_mul hab (pow_le_pow_left₀ ha hab _) (pow_nonneg ha _) (ha.trans hab)
 
+lemma pow_left_monotoneOn : MonotoneOn (fun a : M₀ ↦ a ^ n) {x | 0 ≤ x} :=
+  fun _a ha _b _ hab ↦ pow_le_pow_left₀ ha hab _
+
 end
 
 variable [Preorder α] {f g : α → M₀}

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -412,8 +412,8 @@ lemma norm_iteratedFDeriv_fourierPowSMulRight
     gcongr with i hi
     · rw [← Nat.cast_pow, Nat.cast_le]
       calc n.descFactorial i ≤ n ^ i := Nat.descFactorial_le_pow _ _
-      _ ≤ (n + 1) ^ i := pow_le_pow_left (by omega) (by omega) i
-      _ ≤ (n + 1) ^ k := pow_right_mono₀ (by omega) (Finset.mem_range_succ_iff.mp hi)
+      _ ≤ (n + 1) ^ i := by gcongr; omega
+      _ ≤ (n + 1) ^ k := by gcongr; exacts [le_add_self, Finset.mem_range_succ_iff.mp hi]
     · exact hv _ (by omega) _ (by omega)
   _ = (2 * n + 2) ^ k * (‖L‖^n * C) := by
     simp only [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose, mul_one, ← mul_assoc,

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -1212,7 +1212,7 @@ instance (priority := 100) InnerProductSpace.toUniformConvexSpace : UniformConve
     refine le_sqrt_of_sq_le ?_
     rw [sq, eq_sub_iff_add_eq.2 (parallelogram_law_with_norm ℝ x y), ← sq ‖x - y‖, hx, hy]
     ring_nf
-    exact sub_le_sub_left (pow_le_pow_left hε.le hxy _) 4⟩
+    gcongr⟩
 
 section Complex_Seminormed
 

Mathlib/Analysis/Normed/Field/Ultra.lean

@@ -89,8 +89,7 @@ lemma isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm
   -- `‖x + 1‖ ^ m ≤ (m + 1) • max 1 ‖x‖ ^ m`, so we're done
   -- we can distribute powers into the right term of `max`
   have hp : max 1 ‖x‖ ^ m = max 1 (‖x‖ ^ m) := by
-    have : MonotoneOn (fun a : ℝ ↦ a ^ m) (Set.Ici _) := fun a h b _ h' ↦ pow_le_pow_left h h' _
-    rw [this.map_max (by simp [zero_le_one]) (norm_nonneg x), one_pow]
+    rw [pow_left_monotoneOn.map_max (by simp [zero_le_one]) (norm_nonneg x), one_pow]
   rw [hp] at hm
   refine le_of_pow_le_pow_left₀ (fun h ↦ ?_) (zero_lt_one.trans ha').le ((h _ _).trans hm.le)
   simp only [h, zero_add, pow_zero, max_self, one_smul, lt_self_iff_false] at hm

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -264,7 +264,7 @@ theorem tendsto_exp_div_pow_atTop (n : ℕ) : Tendsto (fun x => exp x / x ^ n) a
   have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
   rw [Set.mem_Ici, le_div_iff₀ (pow_pos hx₀ _), ← le_div_iff₀' hC₀]
   calc
-    x ^ n ≤ ⌈x⌉₊ ^ n := mod_cast pow_le_pow_left hx₀.le (Nat.le_ceil _) _
+    x ^ n ≤ ⌈x⌉₊ ^ n := by gcongr; exact Nat.le_ceil _
     _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
     _ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le
     _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

@@ -72,15 +72,14 @@ variable {E}
 theorem finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : (n : ℝ) < r) :
     (∫⁻ x : ℝ in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n)) < ∞ := by
   have hr : 0 < r := lt_of_le_of_lt n.cast_nonneg hnr
-  have h_int : ∀ x : ℝ, x ∈ Ioc (0 : ℝ) 1 →
-      ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * n))) := fun x hx ↦ by
-    apply ENNReal.ofReal_le_ofReal
-    rw [← neg_mul, rpow_mul hx.1.le, rpow_natCast]
-    refine pow_le_pow_left ?_ (by simp only [sub_le_self_iff, zero_le_one]) n
-    rw [le_sub_iff_add_le', add_zero]
-    refine Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 ?_
-    rw [Right.neg_nonpos_iff, inv_nonneg]
-    exact hr.le
+  have h_int x (hx : x ∈ Ioc (0 : ℝ) 1) := by
+    calc
+      ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ .ofReal ((x ^ (-r⁻¹) - 0) ^ n) := by
+        gcongr
+        · rw [sub_nonneg]
+          exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 (by simpa using hr.le)
+        · norm_num
+      _ = .ofReal (x ^ (-(r⁻¹ * n))) := by simp [rpow_mul hx.1.le, ← neg_mul]
   refine lt_of_le_of_lt (setLIntegral_mono' measurableSet_Ioc h_int) ?_
   refine IntegrableOn.setLIntegral_lt_top ?_
   rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -69,7 +69,7 @@ private theorem eps_pos {ε : ℝ} {n : ℕ} (h : 100 ≤ (4 : ℝ) ^ n * ε ^ 5
     (pos_of_mul_pos_right ((show 0 < (100 : ℝ) by norm_num).trans_le h) (by positivity))
 
 private theorem m_pos [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α) : 0 < m :=
-  Nat.div_pos ((Nat.mul_le_mul_left _ <| Nat.pow_le_pow_left (by norm_num) _).trans hPα) <|
+  Nat.div_pos (hPα.trans' <| by unfold stepBound; gcongr; norm_num) <|
     stepBound_pos (P.parts_nonempty <| univ_nonempty.ne_empty).card_pos
 
 /-- Local extension for the `positivity` tactic: A few facts that are needed many times for the

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -226,20 +226,19 @@ private theorem one_sub_le_m_div_m_add_one_sq [Nonempty α]
   sz_positivity
 
 private theorem m_add_one_div_m_le_one_add [Nonempty α]
-    (hPα : #P.parts * 16 ^ #P.parts ≤ card α) (hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5)
-    (hε₁ : ε ≤ 1) : ((m + 1 : ℝ) / m) ^ 2 ≤ ↑1 + ε ^ 5 / 49 := by
-  rw [same_add_div]
-  swap; · sz_positivity
-  have : ↑1 + ↑1 / (m : ℝ) ≤ ↑1 + ε ^ 5 / 100 := by
-    rw [add_le_add_iff_left, ← one_div_div (100 : ℝ)]
-    exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)
-  refine (pow_le_pow_left ?_ this 2).trans ?_
-  · positivity
-  rw [add_sq, one_pow, add_assoc, add_le_add_iff_left, mul_one, ← le_sub_iff_add_le',
-    div_eq_mul_one_div _ (49 : ℝ), mul_div_left_comm (2 : ℝ), ← mul_sub_left_distrib, div_pow,
-    div_le_iff₀ (show (0 : ℝ) < ↑100 ^ 2 by norm_num), mul_assoc, sq]
-  refine mul_le_mul_of_nonneg_left ?_ (by sz_positivity)
-  exact (pow_le_one₀ (by sz_positivity) hε₁).trans (by norm_num)
+    (hPα : #P.parts * 16 ^ #P.parts ≤ card α) (hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5) (hε₁ : ε ≤ 1) :
+    ((m + 1 : ℝ) / m) ^ 2 ≤ ↑1 + ε ^ 5 / 49 := by
+  have : 0 ≤ ε := by sz_positivity
+  rw [same_add_div (by sz_positivity)]
+  calc
+    _ ≤ (1 + ε ^ 5 / 100) ^ 2 := by
+      gcongr (1 + ?_) ^ 2
+      rw [← one_div_div (100 : ℝ)]
+      exact one_div_le_one_div_of_le (by sz_positivity) (hundred_div_ε_pow_five_le_m hPα hPε)
+    _ = 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000) := by ring
+    _ ≤ 1 + ε ^ 5 * (50⁻¹ + 1 ^ 5 / 10000) := by gcongr
+    _ ≤ 1 + ε ^ 5 * 49⁻¹ := by gcongr; norm_num
+    _ = 1 + ε ^ 5 / 49 := by rw [div_eq_mul_inv]
 
 private theorem density_sub_eps_le_sum_density_div_card [Nonempty α]
     (hPα : #P.parts * 16 ^ #P.parts ≤ card α) (hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5)
@@ -346,21 +345,20 @@ private theorem edgeDensity_chunk_aux [Nonempty α]
     · exact mod_cast G.edgeDensity_le_one _ _
     · exact div_le_div_of_nonneg_left (by sz_positivity) (by norm_num) (by norm_num)
   rw [← sub_nonneg] at hGε
-  have : ↑(G.edgeDensity U V) - ε ^ 5 / ↑50 ≤
-      (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts,
-        (G.edgeDensity ab.1 ab.2 : ℝ)) / ↑16 ^ #P.parts := by
-    have rflU := Set.Subset.refl (chunk hP G ε hU).parts.toSet
-    have rflV := Set.Subset.refl (chunk hP G ε hV).parts.toSet
-    refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
-    · rw [biUnion_parts, biUnion_parts]
-    · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
-      norm_cast
-  refine le_trans ?_ (pow_le_pow_left hGε this 2)
-  rw [sub_sq, sub_add, sub_le_sub_iff_left]
-  refine (sub_le_self _ <| sq_nonneg <| ε ^ 5 / 50).trans ?_
-  rw [mul_right_comm, mul_div_left_comm, div_eq_mul_inv (ε ^ 5),
-    show (2 : ℝ) / 50 = 25⁻¹ by norm_num]
-  exact mul_le_of_le_one_right (by sz_positivity) (mod_cast G.edgeDensity_le_one _ _)
+  have : 0 ≤ ε := by sz_positivity
+  calc
+    _ = G.edgeDensity U V ^ 2 - 1 * ε ^ 5 / 25 + 0 ^ 10 / 2500 := by ring
+    _ ≤ G.edgeDensity U V ^ 2 - G.edgeDensity U V * ε ^ 5 / 25 + ε ^ 10 / 2500 := by
+      gcongr; exact mod_cast G.edgeDensity_le_one ..
+    _ = (G.edgeDensity U V - ε ^ 5 / 50) ^ 2 := by ring
+    _ ≤ _ := by
+      gcongr
+      have rflU := Set.Subset.refl (chunk hP G ε hU).parts.toSet
+      have rflV := Set.Subset.refl (chunk hP G ε hV).parts.toSet
+      refine (le_trans ?_ <| density_sub_eps_le_sum_density_div_card hPα hPε rflU rflV).trans ?_
+      · rw [biUnion_parts, biUnion_parts]
+      · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← cast_mul, ← mul_pow, cast_pow]
+        norm_cast
 
 private theorem abs_density_star_sub_density_le_eps (hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5)
     (hε₁ : ε ≤ 1) {hU : U ∈ P.parts} {hV : V ∈ P.parts} (hUV' : U ≠ V) (hUV : ¬G.IsUniform ε U V) :

Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean

@@ -100,8 +100,9 @@ theorem szemeredi_regularity (hε : 0 < ε) (hl : l ≤ card α) :
     obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := h (⌊4 / ε ^ 5⌋₊ + 1)
     refine ⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans ?_,
       hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) ?_⟩
-    · rw [iterate_succ_apply']
-      exact mul_le_mul_left' (pow_le_pow_left (by norm_num) (by norm_num) _) _
+    · rw [iterate_succ_apply', stepBound, bound]
+      gcongr
+      norm_num
     calc
       (1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by
         rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']; norm_num

Mathlib/Data/Complex/Exponential.lean

@@ -1441,13 +1441,12 @@ theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t
   rcases eq_or_ne n 0 with (rfl | hn)
   · simp
     rwa [Nat.cast_zero] at ht'
-  convert pow_le_pow_left ?_ (one_sub_le_exp_neg (t / n)) n using 2
-  · rw [← Real.exp_nat_mul]
-    congr 1
-    field_simp
-    ring_nf
-  · rwa [sub_nonneg, div_le_one]
-    positivity
+  calc
+    (1 - t / n) ^ n ≤ rexp (-(t / n)) ^ n := by
+      gcongr
+      · exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg
+      · exact one_sub_le_exp_neg _
+    _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity
 
 end Real