awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
⊢ ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹ + δ ![b, n] +
      (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ))⁻¹ - ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹) =
    (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
have hn0 : Ne (α := ℂ) (↑n : ℂ) 0
Tactic: have hn0 : (n : ℂ) ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
have norm_cast : ¬n + 1 = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
⊢ ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹ + δ ![b, n] +
      (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ))⁻¹ - ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹) =
    (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
have hn1 : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: have hn1 : (n : ℂ) + 1 ≠ 0 := by norm_cast; grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
hn1 : HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹ + δ ![b, n] +
      (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ))⁻¹ - ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹) =
    (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
have neg : (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ * (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)⁻¹ +
    ((↑n : ℂ)⁻¹ - (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹) =
  (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)⁻¹
Tactic: simp [δ, h, hb, hn]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹ + δ ![b, n] +
      (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ))⁻¹ - ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹) =
    (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
have h0 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1 ≠ 0
Tactic: have h0 : (b : ℂ) * z + n + 1 ≠ 0 := by
        simpa [add_assoc] using linear_ne_zero (cd := ![b, n + 1]) z (by aesop)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1 ≠ 0
⊢ ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹ + δ ![b, n] +
      (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ))⁻¹ - ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹) =
    (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
have h1 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) ≠ 0
Tactic: have h1 : (b : ℂ) * z + n ≠ 0 := linear_ne_zero (cd := ![b, n]) z (by aesop)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1 ≠ 0
h1 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) ≠ 0
⊢ ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹ + δ ![b, n] +
      (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ))⁻¹ - ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹) =
    (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
have neg : (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹ +
      if b = 0 ∧ n = 0 then 1 else if b = 0 ∧ n = -1 then 2 else 0) +
    (((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ))⁻¹ - ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)⁻¹) =
  (HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
Tactic: simp [δ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ G2 z = t
have rw : Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
  (∑' (b : ℤ),
    HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
      (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
Tactic: rw [G2, show t = t + 0 by ring, ← tsum_tsum_symmetricIco_sub_eq z, ← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
rw :
  Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
    (∑' (b : ℤ),
      HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
        (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
⊢ G2 z = t
have hf : Summable (α := ℂ) fun (m : ℤ) ↦ ∑' (n : ℤ), G2Term z ![m, n]
Tactic: rw [G2, show t = t + 0 by ring, ← tsum_tsum_symmetricIco_sub_eq z, ← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
rw :
  Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
    (∑' (b : ℤ),
      HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
        (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
hf : Summable (α := ℂ) fun (m : ℤ) ↦ ∑' (n : ℤ), G2Term z ![m, n]
⊢ G2 z = t
have hg : Summable (α := ℂ) fun (m : ℤ) ↦
  ∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))
Tactic: rw [G2, show t = t + 0 by ring, ← tsum_tsum_symmetricIco_sub_eq z, ← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
    (∑' (b : ℤ),
      HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
        (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
have rw : Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
  (∑'[symmetricIcc ℤ] (b : ℤ),
    HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
      (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
Tactic: rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
rw :
  Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
    (∑'[symmetricIcc ℤ] (b : ℤ),
      HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
        (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
⊢ Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
    (∑' (b : ℤ),
      HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
        (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
have rw₁ : Summable (α := ℂ) fun (b : ℤ) ↦
  HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
    (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
Tactic: rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Eq (α := ℂ) (∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z)
    (∑'[symmetricIcc ℤ] (b : ℤ),
      HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
        (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))))
have e_f : ∀ (a : ℤ),
  e2Summand a z =
    HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![a, n])
      (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
Tactic: congr with a
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a : ℤ
⊢ e2Summand a z =
    HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![a, n])
      (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
have e_f : Eq (α := ℂ) (∑' (n : ℤ), eisSummand 2 ![a, n] z)
  (∑' (b : ℤ),
    (G2Term z ![(a, b).1, (a, b).2] +
      (1 / ((↑a : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑a : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1))))
Tactic: rw [e2Summand, tsum_eq_of_summable_unconditional
        (summable_right_one_div_linear_sub_one_div_linear_succ z a), ← Summable.tsum_add
        ((G2Term_prod_summable z).prod_factor _)
        (summable_right_one_div_linear_sub_one_div_linear_succ z a)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ) = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
have rw : Eq (α := ℂ)
  (∑'[symmetricIco ℤ] (b : ℤ),
    HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
      (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1))))
  (∑'[symmetricIco ℤ] (b : ℤ), ∑' (m : ℤ), G2Term z ![m, b])
Tactic: rw [← tsum_symmetricIco_tsum_sub_eq z, ← tsum_symmetricIco_tsum_eq_S_act z,
    ← tsum_eq_of_summable_unconditional (L := symmetricIco ℤ), ← Summable.tsum_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
rw :
  Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (b : ℤ),
      HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
        (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1))))
    (∑'[symmetricIco ℤ] (b : ℤ), ∑' (m : ℤ), G2Term z ![m, b])
⊢ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ) = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
have hf : Summable (α := ℂ) (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2) (symmetricIco ℤ)
Tactic: rw [← tsum_symmetricIco_tsum_sub_eq z, ← tsum_symmetricIco_tsum_eq_S_act z,
    ← tsum_eq_of_summable_unconditional (L := symmetricIco ℤ), ← Summable.tsum_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
rw :
  Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (b : ℤ),
      HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
        (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1))))
    (∑'[symmetricIco ℤ] (b : ℤ), ∑' (m : ℤ), G2Term z ![m, b])
hf :
  Summable (α := ℂ) (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    (symmetricIco ℤ)
⊢ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ) = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
have hg : Summable (α := ℂ)
  (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
  (symmetricIco ℤ)
Tactic: rw [← tsum_symmetricIco_tsum_sub_eq z, ← tsum_symmetricIco_tsum_eq_S_act z,
    ← tsum_eq_of_summable_unconditional (L := symmetricIco ℤ), ← Summable.tsum_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
rw :
  Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (b : ℤ),
      HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
        (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1))))
    (∑'[symmetricIco ℤ] (b : ℤ), ∑' (m : ℤ), G2Term z ![m, b])
hf :
  Summable (α := ℂ) (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    (symmetricIco ℤ)
hg :
  Summable (α := ℂ)
    (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (symmetricIco ℤ)
⊢ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ) = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]
have rw₁ : Summable (α := ℂ) fun (n : ℤ) ↦ ∑' (m : ℤ), G2Term z ![m, n]
Tactic: rw [← tsum_symmetricIco_tsum_sub_eq z, ← tsum_symmetricIco_tsum_eq_S_act z,
    ← tsum_eq_of_summable_unconditional (L := symmetricIco ℤ), ← Summable.tsum_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (b : ℤ),
      HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
        (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1))))
    (∑'[symmetricIco ℤ] (b : ℤ), ∑' (m : ℤ), G2Term z ![m, b])
have apply : ∀ (N : ℤ),
  HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)
      (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))) =
    ∑' (m : ℤ), G2Term z ![m, N]
Tactic: apply tsum_congr (fun N ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
N : ℤ
⊢ HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)
      (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))) =
    ∑' (m : ℤ), G2Term z ![m, N]
have rw : Eq (α := ℂ)
  (∑' (b : ℤ),
    (1 / HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
      (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))))
  (∑' (m : ℤ), G2Term z ![m, N])
Tactic: rw [← Summable.tsum_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
N : ℤ
rw :
  Eq (α := ℂ)
    (∑' (b : ℤ),
      (1 / HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
        (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))))
    (∑' (m : ℤ), G2Term z ![m, N])
⊢ HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)
      (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))) =
    ∑' (m : ℤ), G2Term z ![m, N]
have hf : Summable (α := ℂ) fun (m : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2
Tactic: rw [← Summable.tsum_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
N : ℤ
rw :
  Eq (α := ℂ)
    (∑' (b : ℤ),
      (1 / HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
        (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))))
    (∑' (m : ℤ), G2Term z ![m, N])
hf : Summable (α := ℂ) fun (m : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2
⊢ HSub.hSub (α := ℂ) (∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)
      (∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))) =
    ∑' (m : ℤ), G2Term z ![m, N]
have hg : Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)
Tactic: rw [← Summable.tsum_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
N : ℤ
⊢ Eq (α := ℂ)
    (∑' (b : ℤ),
      (1 / HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
        (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))))
    (∑' (m : ℤ), G2Term z ![m, N])
have apply : ∀ (M : ℤ),
  1 / HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
      (1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)) =
    G2Term z ![M, N]
Tactic: apply tsum_congr (fun M ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
N M : ℤ
⊢ 1 / HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
      (1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)) =
    G2Term z ![M, N]
have simp : (HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)⁻¹ -
    (((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ))⁻¹ - ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹) =
  ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)⁻¹ + δ ![M, N]
Tactic: simp only [one_div, G2Term, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
        Matrix.cons_val_fin_one, mul_inv_rev]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
N M : ℤ
⊢ (HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)⁻¹ -
      (((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ))⁻¹ - ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹) =
    ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)⁻¹ + δ ![M, N]
have nth_rw : ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)⁻¹ + δ ![M, N] +
      (((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ))⁻¹ - ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹) -
    (((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ))⁻¹ - ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹) =
  ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)⁻¹ * (HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2)⁻¹ + δ ![M, N]
Tactic: nth_rw 1 [← aux_identity z M N]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Summable (α := ℂ) (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    (symmetricIco ℤ)
have hf : HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
  ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)
Tactic: apply HasSum.summable (a := (z.1 ^ 2)⁻¹ * G2 (S • z))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)
have hf : Tendsto
  (fun (N : ℕ) ↦
    ∑ n ∈ Finset.Ico (-(↑N : ℤ)) (↑N : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
  atTop (𝓝 ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)))
Tactic: rw [hasSum_symmetricIco_int_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑ n ∈ Finset.Ico (-(↑N : ℤ)) (↑N : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    atTop (𝓝 ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)))
have apply : ∀ (x : ℕ),
  Eq (α := ℂ)
    (∑' (n : ℤ), ∑ m ∈ Finset.Ico (-(↑x : ℤ)) (↑x : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    (∑ n ∈ Finset.Ico (-(↑x : ℤ)) (↑x : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
Tactic: apply (tendsto_double_sum_S_act z).congr (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
x : ℕ
⊢ Eq (α := ℂ)
    (∑' (n : ℤ), ∑ m ∈ Finset.Ico (-(↑x : ℤ)) (↑x : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    (∑ n ∈ Finset.Ico (-(↑x : ℤ)) (↑x : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
have rw : ∀ (i : ℤ) (hi : Membership.mem (γ := Finset ℤ) (Finset.Ico (-(↑x : ℤ)) (↑x : ℤ)) i),
  Summable (α := ℂ) fun (n : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2
Tactic: rw [Summable.tsum_finsetSum (fun i hi ↦ ?_)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Summable (α := ℂ)
    (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (symmetricIco ℤ)
have hg : HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
  (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)
Tactic: apply HasSum.summable (a := -2 * π * I / z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)
have hg : Tendsto
  (fun (x : (↑(Ioi 0) : Type)) ↦
    ∑ n ∈ Finset.Ico (-(↑(↑x : ℕ) : ℤ)) (↑(↑x : ℕ) : ℤ),
      ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
  atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
Tactic: rw [hasSum_symmetricIco_int_iff, ← tendsto_comp_val_Ioi_atTop]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
hg :
  Tendsto
    (fun (x : (↑(Ioi 0) : Type)) ↦
      ∑ n ∈ Finset.Ico (-(↑(↑x : ℕ) : ℤ)) (↑(↑x : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
⊢ HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)
have rw : ℕ
Tactic: rw [hasSum_symmetricIco_int_iff, ← tendsto_comp_val_Ioi_atTop]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ ∑' (m : ℤ), G2Term z ![m, n]
have this : Summable (G2Term z)
Tactic: have := G2Term_summable z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
this : Summable (G2Term z)
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ ∑' (m : ℤ), G2Term z ![m, n]
have this₁ : Summable (β := ℤ × ℤ) (G2Term z ∘ (⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
Tactic: rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Eq (α := ℂ) (∑' (m : Fin 2 → ℤ), G2Term z m) (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])
have rw : Eq (α := ℂ) (∑' (c : ℤ × ℤ), G2Term z (((finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ) c))
  (∑' (m : ℤ) (n : ℤ), G2Term z ![m, n])
Tactic: rw [← (finTwoArrowEquiv _).symm.tsum_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Eq (α := ℂ) (∑' (m : Fin 2 → ℤ), G2Term z m) (∑' (n : ℤ) (m : ℤ), G2Term z ![m, n])
have h : Summable (α := ℂ) (β := ℤ × ℤ) (Function.uncurry fun (m n : ℤ) ↦ G2Term z ![m, n])
Tactic: rw [Summable.tsum_comm', tsum_G2Term_eq_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
h : Summable (α := ℂ) (β := ℤ × ℤ) (Function.uncurry fun (m n : ℤ) ↦ G2Term z ![m, n])
⊢ Eq (α := ℂ) (∑' (m : Fin 2 → ℤ), G2Term z m) (∑' (n : ℤ) (m : ℤ), G2Term z ![m, n])
have h₁ : ∀ (b : ℤ), Summable (α := ℂ) fun (n : ℤ) ↦ G2Term z ![b, n]
Tactic: rw [Summable.tsum_comm', tsum_G2Term_eq_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
h : Summable (α := ℂ) (β := ℤ × ℤ) (Function.uncurry fun (m n : ℤ) ↦ G2Term z ![m, n])
h₁ : ∀ (b : ℤ), Summable (α := ℂ) fun (n : ℤ) ↦ G2Term z ![b, n]
⊢ Eq (α := ℂ) (∑' (m : Fin 2 → ℤ), G2Term z m) (∑' (n : ℤ) (m : ℤ), G2Term z ![m, n])
have h₂ : ∀ (c : ℤ), Summable (α := ℂ) fun (b : ℤ) ↦ G2Term z ![b, c]
Tactic: rw [Summable.tsum_comm', tsum_G2Term_eq_tsum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
⊢ ∀ (c : ℤ), Summable (α := ℂ) fun (b : ℤ) ↦ G2Term z ![b, c]
have H : Summable (G2Term z)
Tactic: have H := G2Term_summable z