diff --git a/Mathlib/Analysis/Asymptotics/Lemmas.lean b/Mathlib/Analysis/Asymptotics/Lemmas.lean
index 22eb669d477578..49694fe10a9cc1 100644
--- a/Mathlib/Analysis/Asymptotics/Lemmas.lean
+++ b/Mathlib/Analysis/Asymptotics/Lemmas.lean
@@ -672,6 +672,12 @@ lemma Asymptotics.IsBigO.comp_summable_norm {ι E F : Type*}
   summable_of_isBigO hg <| hf.norm_norm.comp_tendsto <|
     tendsto_zero_iff_norm_tendsto_zero.2 hg.tendsto_cofinite_zero
 
+lemma Summable.mul_tendsto_const {F ι : Type*} [NormedRing F] [NormMulClass F] [NormOneClass F]
+    [CompleteSpace F] {f g : ι → F} (hf : Summable fun n ↦ ‖f n‖) {c : F}
+    (hg : Tendsto g cofinite (𝓝 c)) : Summable fun n ↦ f n * g n := by
+  apply summable_of_isBigO hf
+  simpa using (isBigO_const_mul_self 1 f _).mul (hg.isBigO_one F)
+
 namespace PartialHomeomorph
 
 variable {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β]
diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean
index 59453b7b5157dc..680b42245578ce 100644
--- a/Mathlib/Analysis/Complex/Exponential.lean
+++ b/Mathlib/Analysis/Complex/Exponential.lean
@@ -455,7 +455,7 @@ lemma norm_exp_sub_sum_le_exp_norm_sub_sum (x : ℂ) (n : ℕ) :
     rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
     refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
     congr with i
-    simp [Complex.norm_pow]
+    simp [Complex.norm_pow, Complex.norm_natCast]
   _ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
     gcongr
     exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _
diff --git a/Mathlib/Analysis/Complex/Norm.lean b/Mathlib/Analysis/Complex/Norm.lean
index f647b46b7159fa..f7827a3885342c 100644
--- a/Mathlib/Analysis/Complex/Norm.lean
+++ b/Mathlib/Analysis/Complex/Norm.lean
@@ -104,7 +104,7 @@ protected theorem norm_of_nonneg {r : ℝ} (h : 0 ≤ r) : ‖(r : ℂ)‖ = r :
 @[simp, norm_cast]
 lemma nnnorm_real (r : ℝ) : ‖(r : ℂ)‖₊ = ‖r‖₊ := by ext; exact norm_real _
 
-@[simp 1100, norm_cast]
+@[norm_cast]
 lemma norm_natCast (n : ℕ) : ‖(n : ℂ)‖ = n := Complex.norm_of_nonneg n.cast_nonneg
 
 @[simp 1100]
@@ -114,7 +114,7 @@ lemma norm_ofNat (n : ℕ) [n.AtLeastTwo] :
 protected lemma norm_two : ‖(2 : ℂ)‖ = 2 := norm_ofNat 2
 
 @[simp 1100, norm_cast]
-lemma nnnorm_natCast (n : ℕ) : ‖(n : ℂ)‖₊ = n := Subtype.ext <| by simp
+lemma nnnorm_natCast (n : ℕ) : ‖(n : ℂ)‖₊ = n := Subtype.ext <| by simp [norm_natCast]
 
 @[simp 1100]
 lemma nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :
diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
index 6873c34837776c..bf7ec6e318464d 100644
--- a/Mathlib/Analysis/Normed/Group/Basic.lean
+++ b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -1081,7 +1081,7 @@ theorem norm_of_nonpos (hr : r ≤ 0) : ‖r‖ = -r :=
 theorem le_norm_self (r : ℝ) : r ≤ ‖r‖ :=
   le_abs_self r
 
-@[simp 1100] lemma norm_natCast (n : ℕ) : ‖(n : ℝ)‖ = n := abs_of_nonneg n.cast_nonneg
+lemma norm_natCast (n : ℕ) : ‖(n : ℝ)‖ = n := abs_of_nonneg n.cast_nonneg
 @[simp 1100] lemma nnnorm_natCast (n : ℕ) : ‖(n : ℝ)‖₊ = n := NNReal.eq <| norm_natCast _
 @[simp 1100] lemma enorm_natCast (n : ℕ) : ‖(n : ℝ)‖ₑ = n := by simp [enorm]
 
diff --git a/Mathlib/Analysis/Normed/Group/Int.lean b/Mathlib/Analysis/Normed/Group/Int.lean
index da0a26bda53f36..3bf3b3861fe7a4 100644
--- a/Mathlib/Analysis/Normed/Group/Int.lean
+++ b/Mathlib/Analysis/Normed/Group/Int.lean
@@ -25,7 +25,6 @@ theorem norm_cast_real (m : ℤ) : ‖(m : ℝ)‖ = ‖m‖ :=
 theorem norm_eq_abs (n : ℤ) : ‖n‖ = |(n : ℝ)| :=
   rfl
 
-@[simp]
 theorem norm_natCast (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [Int.norm_eq_abs]
 
 theorem _root_.NNReal.natCast_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ :=
@@ -48,7 +47,7 @@ variable [SeminormedCommGroup α]
 
 @[to_additive norm_zsmul_le]
 theorem norm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖ ≤ ‖n‖ * ‖a‖ := by
-  rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa using norm_pow_le_mul_norm
+  rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩ <;> simpa [Int.norm_natCast] using norm_pow_le_mul_norm
 
 @[to_additive nnnorm_zsmul_le]
 theorem nnnorm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊ := by
diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean
index cfd52d15481dba..3907b5158a8217 100644
--- a/Mathlib/Analysis/Normed/Module/Basic.lean
+++ b/Mathlib/Analysis/Normed/Module/Basic.lean
@@ -71,6 +71,11 @@ theorem norm_natCast_eq_mul_norm_one (α) [SeminormedRing α] [NormSMulClass ℤ
     ‖(n : α)‖ = n * ‖(1 : α)‖ := by
   simpa using norm_intCast_eq_abs_mul_norm_one α n
 
+@[simp]
+lemma norm_natCast {α : Type*} [SeminormedRing α] [NormOneClass α] [NormSMulClass ℤ α]
+    (a : ℕ) : ‖(a : α)‖ = a := by
+  simpa using norm_natCast_eq_mul_norm_one α a
+
 theorem eventually_nhds_norm_smul_sub_lt (c : 𝕜) (x : E) {ε : ℝ} (h : 0 < ε) :
     ∀ᶠ y in 𝓝 x, ‖c • (y - x)‖ < ε :=
   have : Tendsto (fun y ↦ ‖c • (y - x)‖) (𝓝 x) (𝓝 0) :=
diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
index 3c41224b49536b..77f545d06b41da 100644
--- a/Mathlib/Analysis/RCLike/Basic.lean
+++ b/Mathlib/Analysis/RCLike/Basic.lean
@@ -611,7 +611,7 @@ theorem ratCast_im (q : ℚ) : im (q : K) = 0 := by rw [← ofReal_ratCast, ofRe
 theorem norm_of_nonneg {r : ℝ} (h : 0 ≤ r) : ‖(r : K)‖ = r :=
   (norm_ofReal _).trans (abs_of_nonneg h)
 
-@[simp, rclike_simps, norm_cast]
+@[simp 1100, rclike_simps, norm_cast]
 theorem norm_natCast (n : ℕ) : ‖(n : K)‖ = n := by
   rw [← ofReal_natCast]
   exact norm_of_nonneg (Nat.cast_nonneg n)
diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
index 8d50c857ea757a..701de35d06c0f6 100644
--- a/Mathlib/NumberTheory/ArithmeticFunction.lean
+++ b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -831,6 +831,9 @@ theorem sigma_one_apply_prime_pow {p i : ℕ} (hp : p.Prime) :
     σ 1 (p ^ i) = ∑ k ∈ .range (i + 1), p ^ k := by
   simp [sigma_apply_prime_pow hp]
 
+theorem sigma_eq_sum_div (k n : ℕ) : sigma k n = ∑ d ∈ Nat.divisors n, (n / d) ^ k := by
+  rw [sigma_apply, ← Nat.sum_div_divisors]
+
 theorem sigma_zero_apply (n : ℕ) : σ 0 n = #n.divisors := by simp [sigma_apply]
 
 theorem sigma_zero_apply_prime_pow {p i : ℕ} (hp : p.Prime) : σ 0 (p ^ i) = i + 1 := by
diff --git a/Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean b/Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean
index e9967258a2bd52..8ec89e74cb42b1 100644
--- a/Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean
+++ b/Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean
@@ -3,8 +3,8 @@ Copyright (c) 2025 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 -/
-import Mathlib.NumberTheory.Divisors
-import Mathlib.Data.PNat.Defs
+import Mathlib.Analysis.SpecificLimits.Normed
+import Mathlib.NumberTheory.ArithmeticFunction
 
 /-!
 # Lemmas on infinite sums over the antidiagonal of the divisors function
@@ -12,8 +12,15 @@ import Mathlib.Data.PNat.Defs
 This file contains lemmas about the antidiagonal of the divisors function. It defines the map from
 `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b` to `(a, b)`.
 
+We then prove some identities about the infinite sums over this antidiagonal, such as
+`∑' n : ℕ+, n ^ k * r ^ n / (1 - r ^ n) = ∑' n : ℕ+, σ k n * r ^ n`
+which are used for Eisenstein series and their q-expansions. This is also a special case of
+Lambert series.
+
 -/
 
+open Filter Complex ArithmeticFunction Nat Topology
+
 /-- The map from `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b`
 to `(a, b)`. -/
 def divisorsAntidiagonalFactors (n : ℕ+) : Nat.divisorsAntidiagonal n → ℕ+ × ℕ+ := fun x ↦
@@ -48,3 +55,68 @@ lemma sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ+ × ℕ+) :
 
 lemma sigmaAntidiagonalEquivProd_symm_apply_snd (x : ℕ+ × ℕ+) :
     (sigmaAntidiagonalEquivProd.symm x).2 = (x.1.1, x.2.1) := rfl
+
+section tsum
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜]
+
+omit [NormSMulClass ℤ 𝕜] in
+lemma summable_norm_pow_mul_geometric_div_one_sub (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    Summable fun n : ℕ ↦ n ^ k * r ^ n / (1 - r ^ n) := by
+  simp only [div_eq_mul_one_div ( _ * _ ^ _)]
+  apply Summable.mul_tendsto_const (c := 1 / (1 - 0))
+    (by simpa using summable_norm_pow_mul_geometric_of_norm_lt_one k hr)
+  simpa only [Nat.cofinite_eq_atTop] using
+   tendsto_const_nhds.div ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).const_sub 1) (by simp)
+
+private lemma summable_divisorsAntidiagonal_aux (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    Summable fun c : (n : ℕ+) × {x // x ∈ (n : ℕ).divisorsAntidiagonal} ↦
+    (c.2.1.2) ^ k * (r ^ (c.2.1.1 * c.2.1.2)) := by
+  apply Summable.of_norm
+  rw [summable_sigma_of_nonneg (fun a ↦ by positivity)]
+  constructor
+  · exact fun n ↦ (hasSum_fintype _).summable
+  · simp only [norm_mul, norm_pow, tsum_fintype, Finset.univ_eq_attach]
+    apply Summable.of_nonneg_of_le (f := fun c : ℕ+ ↦ ‖(c : 𝕜) ^ (k + 1) * r ^ (c : ℕ)‖)
+      (fun b ↦ Finset.sum_nonneg (fun _ _ ↦ mul_nonneg (by simp) (by simp))) (fun b ↦ ?_)
+      (by apply (summable_norm_pow_mul_geometric_of_norm_lt_one (k + 1) hr).subtype)
+    transitivity ∑ _ ∈ (b : ℕ).divisors, ‖(b : 𝕜)‖ ^ k * ‖r ^ (b : ℕ)‖
+    · rw [(b : ℕ).divisorsAntidiagonal.sum_attach (fun x ↦ ‖(x.2 : 𝕜)‖ ^ _ * _ ^ (x.1 * x.2)),
+          sum_divisorsAntidiagonal ((fun x y ↦ ‖(y : 𝕜)‖ ^ k * _ ^ (x * y)))]
+      gcongr with i hi
+      · simpa using le_of_dvd b.2 (div_dvd_of_dvd (dvd_of_mem_divisors hi))
+      · rw [norm_pow, mul_comm,  Nat.div_mul_cancel (dvd_of_mem_divisors hi)]
+    · simp only [norm_pow, Finset.sum_const, nsmul_eq_mul, ← mul_assoc, add_comm k 1, pow_add,
+        pow_one, norm_mul]
+      gcongr
+      simpa using Nat.card_divisors_le_self b
+
+theorem summable_prod_mul_pow (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    Summable fun c : (ℕ+ × ℕ+) ↦ c.2 ^ k * (r ^ (c.1 * c.2 : ℕ)) := by
+  simpa [sigmaAntidiagonalEquivProd.summable_iff.symm] using summable_divisorsAntidiagonal_aux k hr
+
+theorem tsum_prod_pow_eq_tsum_sigma (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    ∑' d : ℕ+, ∑' c : ℕ+, c ^ k * r ^ (d * c : ℕ) = ∑' e : ℕ+, σ k e * r ^ (e : ℕ) := by
+  suffices ∑' c : ℕ+ × ℕ+, c.2 ^ k * r ^ (c.1 * c.2 : ℕ) =
+    ∑' e : ℕ+, σ k e * r ^ (e : ℕ) by rwa [← (summable_prod_mul_pow k hr).tsum_prod]
+  simp only [← sigmaAntidiagonalEquivProd.tsum_eq, sigmaAntidiagonalEquivProd,
+    divisorsAntidiagonalFactors, PNat.mk_coe, Equiv.coe_fn_mk, sigma_eq_sum_div, cast_sum,
+    cast_pow, Summable.tsum_sigma (summable_divisorsAntidiagonal_aux k hr)]
+  refine tsum_congr fun n ↦ ?_
+  simpa [tsum_fintype, Finset.sum_mul,
+    (n : ℕ).divisorsAntidiagonal.sum_attach fun x : ℕ × ℕ ↦ x.2 ^ k * r ^ (x.1 * x.2),
+    sum_divisorsAntidiagonal fun x y ↦ y ^ k * r ^ (x * y)]
+      using Finset.sum_congr rfl fun i hi ↦ by rw [Nat.mul_div_cancel' (dvd_of_mem_divisors hi)]
+
+lemma tsum_pow_div_one_sub_eq_tsum_sigma {r : 𝕜} (hr : ‖r‖ < 1) (k : ℕ) :
+    ∑' n : ℕ+, n ^ k * r ^ (n : ℕ) / (1 - r ^ (n : ℕ)) = ∑' n : ℕ+, σ k n * r ^ (n : ℕ) := by
+  have (m : ℕ) [NeZero m] := tsum_geometric_of_norm_lt_one (ξ := r ^ m)
+    (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
+  simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
+    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (fun m ↦ n ^ k * (r ^ n) ^ m)]
+  have h00 := tsum_prod_pow_eq_tsum_sigma k hr
+  rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00
+  rw [← h00]
+  exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm b.val c.val, pow_mul]
+
+end tsum
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
index 39a1e84ffefc18..2c2e0519770b09 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@@ -386,6 +386,11 @@ theorem tprod_congr {f g : β → α}
     (hfg : ∀ b, f b = g b) : ∏' b, f b = ∏' b, g b :=
   congr_arg tprod (funext hfg)
 
+@[to_additive]
+theorem tprod_congr₂ {f g : γ → β → α}
+    (hfg : ∀ b c, f b c = g b c) : ∏' c, ∏' b, f b c = ∏' c, ∏' b, g b c :=
+  tprod_congr fun c ↦ tprod_congr fun b ↦ hfg b c
+
 @[to_additive]
 theorem tprod_fintype [Fintype β] (f : β → α) : ∏' b, f b = ∏ b, f b := by
   apply tprod_eq_prod; simp