cascade renamings

leanprover-community · Mar 4, 2024 · dcc991f · dcc991f
1 parent 1b69d82
commit dcc991f
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 13 deletions.
diff --git 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
@@ -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
@@ -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 ?_)