awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
pos :
  ∀ (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)⁻¹
neg :
  ∀ (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)⁻¹
⊢ ((↑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)⁻¹

Tactic:
by_cases hn : n = -1
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : n = -1
pos : HAdd.hAdd (α := ℂ) 2 (-1) = 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)⁻¹

Tactic:
simp [hb, hn, δ_eq_two]

Premises used: _private.0.EisensteinSeries.δ_eq_two
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : n = -1
⊢ HAdd.hAdd (α := ℂ) 2 (-1) = 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
have hn0 : (n : ℂ) ≠ 0 := by aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
norm_cast : ¬n + 1 = 0
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
⊢ ¬n + 1 = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : Ne (α := ℂ) (↑n : ℂ) 0
⊢ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
have hn1 : (n : ℂ) + 1 ≠ 0 := by norm_cast; grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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
neg :
  (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ * (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)⁻¹ +
      ((↑n : ℂ)⁻¹ - (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹) =
    (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)⁻¹
⊢ ((↑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)⁻¹

Tactic:
simp [δ, h, hb, hn]

Premises used: _private.0.EisensteinSeries.δ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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
⊢ (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ * (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)⁻¹ +
      ((↑n : ℂ)⁻¹ - (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹) =
    (HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2)⁻¹

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ ![(↑b : ℝ), HAdd.hAdd (α := ℝ) (↑n : ℝ) 1] ≠ 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1 ≠ 0

Tactic:
simpa [add_assoc] using linear_ne_zero (cd := ![b, n + 1]) z (by aesop)

Premises used: add_assoc, UpperHalfPlane.linear_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ (↑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)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1 ≠ 0
⊢ Ne (α := Fin 2 → ℝ) ![(↑b : ℝ), (↑n : ℝ)] 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1 ≠ 0
⊢ (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) ≠ 0

Tactic:
have h1 : (b : ℂ) * z + n ≠ 0 := linear_ne_zero (cd := ![b, n]) z (by aesop)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1 ≠ 0
h1 : (↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) ≠ 0
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)⁻¹
⊢ ((↑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)⁻¹

Tactic:
simp [δ]

Premises used: _private.0.EisensteinSeries.δ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)⁻¹ +
        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:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
set :
  let t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n];
  G2 z = t
⊢ G2 z = ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]

Tactic:
set t := ∑' m, ∑' n, (G2Term z ![m, n])
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ t = t + 0

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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]
hg :
  Summable (α := ℂ) fun (m : ℤ) ↦
    ∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))
⊢ G2 z = t

Tactic:
rw [G2, show t = t + 0 by ring, ← tsum_tsum_symmetricIco_sub_eq z, ← Summable.tsum_add]

Premises used: EisensteinSeries.G2, EisensteinSeries.tsum_tsum_symmetricIco_sub_eq, Summable.tsum_add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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))))
rw₁ :
  Summable (α := ℂ) fun (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))))

Tactic:
rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]

Premises used: tsum_eq_of_summable_unconditional
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
e_f :
  ∀ (a : ℤ),
    e2Summand a z =
      HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![a, n])
        (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
⊢ 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:
congr with a
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a : ℤ
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))))
⊢ e2Summand a z =
    HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![a, n])
      (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑a : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 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)]

Premises used: tsum_eq_of_summable_unconditional, EisensteinSeries.e2Summand, EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succ, _private.0.EisensteinSeries.G2Term_prod_summable, Summable.prod_factor, Summable.tsum_add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a b : ℤ
⊢ eisSummand 2 ![a, b] z =
    G2Term z ![(a, b).1, (a, b).2] + (1 / ((↑a : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑a : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1))

Tactic:
simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat]

Premises used: zpow_ofNat, _private.0.EisensteinSeries.G2Term, EisensteinSeries.eisSummand, _private.0.EisensteinSeries.aux_identity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a : ℤ
⊢ 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:
exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable (α := ℂ) fun (b : ℤ) ↦
    HAdd.hAdd (α := ℂ) (∑' (n : ℤ), G2Term z ![b, n])
      (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))

Tactic:
simpa only [tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z, add_zero]
        using (G2Term_prod_summable z).prod

Premises used: EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero, Summable.prod, add_zero, _private.0.EisensteinSeries.G2Term_prod_summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ ∑' (n : ℤ), G2Term z ![m, n]

Tactic:
grind [(G2Term_prod_summable z).prod.congr]

Premises used: Summable.prod, Summable.congr, _private.0.EisensteinSeries.G2Term_prod_summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
b : ℤ
⊢ Eq (α := ℂ) 0
    (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))

Tactic:
simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]

Premises used: EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable (α := ℂ) fun (m : ℤ) ↦
    ∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))

Tactic:
exact summable_zero.congr
      fun b ↦ by simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]

Premises used: summable_zero, Summable.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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 ℤ)
rw₁ : Summable (α := ℂ) fun (n : ℤ) ↦ ∑' (m : ℤ), G2Term z ![m, n]
⊢ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z) - -2 * (↑π : ℂ) * I / (↑z : ℂ) = ∑' (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]

Premises used: tsum_eq_of_summable_unconditional, Summable.tsum_sub, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, EisensteinSeries.tsum_symmetricIco_tsum_sub_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
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]
⊢ 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:
apply tsum_congr (fun N ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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
hg : Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)
⊢ 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:
rw [← Summable.tsum_sub]

Premises used: Summable.tsum_sub
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
N : ℤ
apply :
  ∀ (M : ℤ),
    1 / HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
        (1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)) =
      G2Term z ![M, N]
⊢ Eq (α := ℂ)
    (∑' (b : ℤ),
      (1 / HPow.hPow (β := ℕ) ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
        (1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1))))
    (∑' (m : ℤ), G2Term z ![m, N])

Tactic:
apply tsum_congr (fun M ↦ ?_)

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
N M : ℤ
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]
⊢ 1 / HPow.hPow (β := ℕ) ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2 -
      (1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑M : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)) =
    G2Term z ![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]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, Matrix.cons_val_fin_one, _private.0.EisensteinSeries.G2Term, Fin.isValue, one_div, mul_inv_rev
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
N M : ℤ
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]
⊢ (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:
nth_rw 1 [← aux_identity z M N]

Premises used: _private.0.EisensteinSeries.aux_identity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
N M : ℤ
⊢ ((↑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:
ring
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
N : ℤ
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) 2

Tactic:
simpa using linear_left_summable (ne_zero z) N le_rfl

Premises used: le_rfl, EisensteinSeries.linear_left_summable, UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
N : ℤ
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ) + 1)

Tactic:
simpa [add_assoc] using summable_left_one_div_linear_sub_one_div_linear z N (N + 1)

Premises used: EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, add_assoc, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
hf :
  HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)
⊢ Summable (α := ℂ) (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    (symmetricIco ℤ)

Tactic:
apply HasSum.summable (a := (z.1 ^ 2)⁻¹ * G2 (S • z))

Premises used: HasSum.summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
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)))
⊢ HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)

Tactic:
rw [hasSum_symmetricIco_int_iff]

Premises used: SummationFilter.hasSum_symmetricIco_int_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
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)
⊢ 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:
apply (tendsto_double_sum_S_act z).congr (fun x ↦ ?_)

Premises used: EisensteinSeries.tendsto_double_sum_S_act, Filter.Tendsto.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
x : ℕ
rw :
  ∀ (i : ℤ) (hi : Membership.mem (γ := Finset ℤ) (Finset.Ico (-(↑x : ℤ)) (↑x : ℤ)) i),
    Summable (α := ℂ) fun (n : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2
⊢ 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:
rw [Summable.tsum_finsetSum (fun i hi ↦ ?_)]

Premises used: Summable.tsum_finsetSum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
x : ℕ
i : ℤ
hi : Membership.mem (γ := Finset ℤ) (Finset.Ico (-(↑x : ℤ)) (↑x : ℤ)) i
⊢ LE.le (α := ℤ) 2 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
x : ℕ
i : ℤ
hi : Membership.mem (γ := Finset ℤ) (Finset.Ico (-(↑x : ℤ)) (↑x : ℤ)) i
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2

Tactic:
simpa using linear_left_summable (ne_zero z) i (k := 2) (by norm_num)

Premises used: EisensteinSeries.linear_left_summable, UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
hg :
  HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)
⊢ Summable (α := ℂ)
    (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (symmetricIco ℤ)

Tactic:
apply HasSum.summable (a := -2 * π * I / z)

Premises used: HasSum.summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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 : ℂ)))
rw : ℕ
⊢ HasSum (fun (n : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)

Tactic:
rw [hasSum_symmetricIco_int_iff, ← tendsto_comp_val_Ioi_atTop]

Premises used: SummationFilter.hasSum_symmetricIco_int_iff, Filter.tendsto_comp_val_Ioi_atTop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ 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:
tendsto_tsum_one_div_linear_sub_succ_eq z

Premises used: PNat.val, Set.Ioi, Set.Mem, setOf, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, Nat.lt, PNat