From dcc991f6eb47d3c0e5b2d2b30e39a0341569304e Mon Sep 17 00:00:00 2001
From: David Loeffler <d.loeffler.01@cantab.net>
Date: Mon, 4 Mar 2024 15:08:13 +0100
Subject: [PATCH] cascade renamings

---
 Mathlib/Analysis/PSeries.lean                      | 14 +++-----------
 .../ModularForms/JacobiTheta/OneVariable.lean      |  2 +-
 .../ModularForms/JacobiTheta/TwoVariable.lean      |  2 +-
 3 files changed, 5 insertions(+), 13 deletions(-)

diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean
index 3ab25054aa4744..4ba6e2862d1b78 100644
--- a/Mathlib/Analysis/PSeries.lean
+++ b/Mathlib/Analysis/PSeries.lean
@@ -225,8 +225,8 @@ theorem Real.summable_one_div_nat_pow {p : ℕ} :
 theorem Real.summable_one_div_int_pow {p : ℕ} :
     (Summable fun n : ℤ => 1 / (n : ℝ) ^ p) ↔ 1 < p := by
   refine'
-    ⟨fun h => Real.summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective), fun h =>
-      summable_int_of_summable_nat (Real.summable_one_div_nat_pow.mpr h)
+    ⟨fun h ↦ Real.summable_one_div_nat_pow.mp (h.comp_injective Nat.cast_injective),
+     fun h ↦ (Real.summable_one_div_nat_pow.mpr h).of_natCast_neg_natCast
         (((Real.summable_one_div_nat_pow.mpr h).mul_left <| 1 / (-1 : ℝ) ^ p).congr fun n => _)⟩
   conv_rhs =>
     rw [Int.cast_neg, neg_eq_neg_one_mul, mul_pow, ← div_div]
@@ -235,15 +235,7 @@ theorem Real.summable_one_div_int_pow {p : ℕ} :
 
 theorem Real.summable_abs_int_rpow {b : ℝ} (hb : 1 < b) :
     Summable fun n : ℤ => |(n : ℝ)| ^ (-b) := by
-  -- Porting note: was
-  -- refine'
-  --   summable_int_of_summable_nat (_ : Summable fun n : ℕ => |(n : ℝ)| ^ _)
-  --     (_ : Summable fun n : ℕ => |((-n : ℤ) : ℝ)| ^ _)
-  -- on_goal 2 => simp_rw [Int.cast_neg, Int.cast_ofNat, abs_neg]
-  -- all_goals
-  --   simp_rw [fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
-  --   rwa [Real.summable_nat_rpow, neg_lt_neg_iff]
-  apply summable_int_of_summable_nat
+  apply Summable.of_natCast_neg_natCast
   on_goal 2 => simp_rw [Int.cast_neg, abs_neg]
   all_goals
     simp_rw [Int.cast_ofNat, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
index 7a688453e604d9..b560af3dd8cb7b 100644
--- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
+++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
@@ -77,7 +77,7 @@ theorem exists_summable_bound_exp_mul_sq {R : ℝ} (hR : 0 < R) :
       ‖cexp (π * I * (n : ℂ) ^ 2 * τ)‖ ≤ bd n := by
   let y := rexp (-π * R)
   have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hR)
-  refine' ⟨fun n => y ^ n.natAbs, summable_int_of_summable_nat _ _, fun hτ n => _⟩; pick_goal 3
+  refine' ⟨fun n => y ^ n.natAbs, Summable.of_natCast_neg_natCast _ _, fun hτ n => _⟩; pick_goal 3
   · refine' (norm_exp_mul_sq_le (hR.trans_le hτ) n).trans _
     dsimp [y]
     gcongr rexp ?_ ^ _
diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
index bf7672edf07113..de8ca8dea1ce40 100644
--- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
+++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
@@ -48,7 +48,7 @@ lemma jacobiTheta₂_term_bound {S T : ℝ} (hT : 0 < T) {z τ : ℂ}
 lemma summable_jacobiTheta₂_term_bound (S : ℝ) {T : ℝ} (hT : 0 < T) :
     Summable (fun n : ℤ ↦ Real.exp (-π * (T * n ^ 2 - 2 * S * |n|))) := by
   suffices Summable (fun n : ℕ ↦ Real.exp (-π * (T * n ^ 2 - 2 * S * n))) by
-    apply summable_int_of_summable_nat <;>
+    apply Summable.of_natCast_neg_natCast <;>
     simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_ofNat, Nat.abs_cast]
   apply summable_of_isBigO_nat summable_exp_neg_nat
   refine Real.isBigO_exp_comp_exp_comp.mpr (Tendsto.isBoundedUnder_le_atBot ?_)