awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b : ℤ
this :
  Summable (α := ℂ) fun (i : ℤ) ↦
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (((↑i : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑i : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹
rw :
  ∀
    (this :
      Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0} }) ↦
        HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) *
          (((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹),
    Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0} }) ↦
      1 / ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ))
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))

Tactic:
rw [← Finset.summable_compl_iff (s := {0})] at *

Premises used: Finset.summable_compl_iff, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b : ℤ
this :
  Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0} }) ↦
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) *
      (((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹
apply :
  ∀ (m : { x : ℤ // x ∉ {0} }),
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) *
        (((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹ =
      1 / ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ))
⊢ Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0} }) ↦
    1 / ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ))

Tactic:
apply this.congr (fun m ↦ ?_)

Premises used: Summable.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b : ℤ
this :
  Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0} }) ↦
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) *
      (((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹
m : { x : ℤ // x ∉ {0} }
⊢ (↑m : ℤ) ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b : ℤ
this :
  Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0} }) ↦
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) *
      (((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑(↑x : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹
m : { x : ℤ // x ∉ {0} }
⊢ HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) *
      (((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹ =
    1 / ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ))

Tactic:
grind [one_div_linear_sub_one_div_linear_eq z a b m (by grind)]

Premises used: _private.0.EisensteinSeries.one_div_linear_sub_one_div_linear_eq, Subtype.val
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)))⁻¹

Tactic:
have := summable_linear_right_add_one_mul_linear_right z m m
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
this : Summable (α := ℂ) fun (n : ℤ) ↦ (((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)))⁻¹
rw :
  ∀
    (this :
      Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0, -1} }) ↦
        (((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ)))⁻¹),
    Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0, -1} }) ↦
      1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ) + 1)
⊢ Summable (α := ℂ) fun (b : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)

Tactic:
rw [← Finset.summable_compl_iff (s := {0, -1})] at *

Premises used: Finset.summable_compl_iff, Insert.insert, Singleton.singleton, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
this :
  Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0, -1} }) ↦
    (((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ)))⁻¹
apply :
  ∀ (b : { x : ℤ // x ∉ {0, -1} }),
    (((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ)))⁻¹ =
      1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ) + 1)
⊢ Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0, -1} }) ↦
    1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ) + 1)

Tactic:
apply this.congr (fun b ↦ ?_)

Premises used: Summable.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
this :
  Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0, -1} }) ↦
    (((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ)))⁻¹
b : { x : ℤ // x ∉ {0, -1} }
⊢ m ≠ 0 ∨ (↑b : ℤ) ≠ 0 ∧ (↑b : ℤ) + 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
this :
  Summable (α := ℂ) fun (x : { x : ℤ // x ∉ {0, -1} }) ↦
    (((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑(↑x : ℤ) : ℂ)))⁻¹
b : { x : ℤ // x ∉ {0, -1} }
⊢ (((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ)))⁻¹ =
    1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ) + 1)

Tactic:
simpa [add_assoc, mul_comm] using
    (one_div_linear_sub_one_div_linear_eq z b (b + 1) m (by grind)).symm

Premises used: _private.0.EisensteinSeries.one_div_linear_sub_one_div_linear_eq, add_assoc, HAdd.hAdd, mul_comm, OfNat.ofNat, Eq.symm, Subtype.val
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
simp_rw :
  Eq (α := ℂ)
    (∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ),
      (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * ∑' (n : ℤ), (HPow.hPow (β := ℤ) (-((↑x : ℂ) * (↑z : ℂ)⁻¹) + (↑n : ℂ)) 2)⁻¹)
    (∑' (n : ℤ), ∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) * (↑z : ℂ) + (↑x : ℂ)) 2)⁻¹)
⊢ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ *
      ∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑x : ℂ) * (-(↑z : ℂ))⁻¹ + (↑n : ℂ)) 2)⁻¹ =
    ∑' (n : ℤ), ∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑x : ℂ)) 2)⁻¹

Tactic:
simp_rw [inv_neg, mul_neg, mul_sum, pow_two, ← zpow_two]

Premises used: Finset.mul_sum, pow_two, inv_neg, zpow_two, mul_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
rw :
  Eq (α := ℂ)
    (∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ),
      (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * ∑' (n : ℤ), (HPow.hPow (β := ℤ) (-((↑x : ℂ) * (↑z : ℂ)⁻¹) + (↑n : ℂ)) 2)⁻¹)
    (∑ i ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), ∑' (b : ℤ), (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2)⁻¹)
⊢ Eq (α := ℂ)
    (∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ),
      (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * ∑' (n : ℤ), (HPow.hPow (β := ℤ) (-((↑x : ℂ) * (↑z : ℂ)⁻¹) + (↑n : ℂ)) 2)⁻¹)
    (∑' (n : ℤ), ∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) * (↑z : ℂ) + (↑x : ℂ)) 2)⁻¹)

Tactic:
rw [Summable.tsum_finsetSum (fun i hi ↦ linear_left_summable (ne_zero z) i le_rfl)]

Premises used: le_rfl, EisensteinSeries.linear_left_summable, UpperHalfPlane.ne_zero, Summable.tsum_finsetSum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
apply :
  ∀ (n : ℤ) (hn : Membership.mem (γ := Finset ℤ) (Ico (-(↑N : ℤ)) (↑N : ℤ)) n),
    (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * ∑' (n_1 : ℤ), (HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)⁻¹) + (↑n_1 : ℂ)) 2)⁻¹ =
      ∑' (b : ℤ), (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹
⊢ Eq (α := ℂ)
    (∑ x ∈ Ico (-(↑N : ℤ)) (↑N : ℤ),
      (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * ∑' (n : ℤ), (HPow.hPow (β := ℤ) (-((↑x : ℂ) * (↑z : ℂ)⁻¹) + (↑n : ℂ)) 2)⁻¹)
    (∑ i ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), ∑' (b : ℤ), (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2)⁻¹)

Tactic:
apply sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
n : ℤ
hn : Membership.mem (γ := Finset ℤ) (Ico (-(↑N : ℤ)) (↑N : ℤ)) n
rw :
  Eq (α := ℂ)
    (∑' (d : ℤ), (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * (HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)⁻¹) + (↑(-d) : ℂ)) 2)⁻¹)
    (∑' (b : ℤ), (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹)
⊢ (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * ∑' (n_1 : ℤ), (HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)⁻¹) + (↑n_1 : ℂ)) 2)⁻¹ =
    ∑' (b : ℤ), (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹

Tactic:
rw [← tsum_mul_left, ← tsum_comp_neg]

Premises used: tsum_mul_left, tsum_comp_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
n : ℤ
hn : Membership.mem (γ := Finset ℤ) (Ico (-(↑N : ℤ)) (↑N : ℤ)) n
⊢ ∀ (b : ℤ),
    (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * (HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)⁻¹) + (↑(-b) : ℂ)) 2)⁻¹ =
      (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹

Tactic:
grind [zpow_two, ne_zero z]

Premises used: UpperHalfPlane.ne_zero, zpow_two
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ
n : ℤ
hn : Membership.mem (γ := Finset ℤ) (Ico (-(↑N : ℤ)) (↑N : ℤ)) n
⊢ Eq (α := ℂ)
    (∑' (d : ℤ), (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * (HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)⁻¹) + (↑(-d) : ℂ)) 2)⁻¹)
    (∑' (b : ℤ), (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹)

Tactic:
apply tsum_congr (by grind [zpow_two, ne_zero z])

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
rw :
  Tendsto (β := ℂ)
    (fun (N : ℕ) ↦
      ∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    atTop (𝓝 (∑'[symmetricIco ℤ] (x : ℤ), (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x (S • z)))
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    atTop (𝓝 ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)))

Tactic:
rw [G2_eq_tsum_symmetricIco, ← tsum_mul_left]

Premises used: EisensteinSeries.G2_eq_tsum_symmetricIco, tsum_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ HasSum (α := ℂ) (fun (i : ℤ) ↦ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand i (S • z))
    (∑'[symmetricIco ℤ] (b : ℤ), (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand b (S • z)) (symmetricIco ℤ)

Tactic:
have := ((summable_e2Summand_symmetricIco (S • z)).mul_left (z.1 ^ 2)⁻¹).hasSum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  HasSum (α := ℂ) (fun (i : ℤ) ↦ (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand i (S • z))
    (∑'[symmetricIco ℤ] (b : ℤ), (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand b (S • z)) (symmetricIco ℤ)
simp :
  ∀
    (this :
      Tendsto (β := ℂ)
        (Function.comp (β := ℤ)
          ((fun (s : Finset ℤ) ↦
              ∑ x ∈ s, (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) ∘
            fun (N : ℤ) ↦ Ico (-N) N)
          Nat.cast)
        atTop
        (𝓝
          (∑'[{ filter := Filter.map (fun (N : ℤ) ↦ Ico (-N) N) (Filter.map Nat.cast atTop) }] (x : ℤ),
            (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }))),
    Tendsto (β := ℂ)
      (fun (N : ℕ) ↦
        ∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
      atTop
      (𝓝
        (∑'[{ filter := Filter.map (fun (N : ℤ) ↦ Ico (-N) N) (Filter.map Nat.cast atTop) }] (x : ℤ),
          (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }))
⊢ Tendsto (β := ℂ)
    (fun (N : ℕ) ↦
      ∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    atTop (𝓝 (∑'[symmetricIco ℤ] (x : ℤ), (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x (S • z)))

Tactic:
simp only [HasSum, symmetricIco, tendsto_map'_iff, modular_S_smul, ← Nat.map_cast_int_atTop] at *

Premises used: SummationFilter.symmetricIco, Filter.tendsto_map'_iff, UpperHalfPlane.modular_S_smul, HasSum, Nat.map_cast_int_atTop, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  Tendsto (β := ℂ)
    (Function.comp (β := ℤ)
      ((fun (s : Finset ℤ) ↦
          ∑ x ∈ s, (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) ∘
        fun (N : ℤ) ↦ Ico (-N) N)
      Nat.cast)
    atTop
    (𝓝
      (∑'[{ filter := Filter.map (fun (N : ℤ) ↦ Ico (-N) N) (Filter.map Nat.cast atTop) }] (x : ℤ),
        (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }))
apply :
  ∀ (N : ℕ),
    Eq (α := ℂ)
      (Function.comp (β := ℤ)
        ((fun (s : Finset ℤ) ↦
            ∑ x ∈ s, (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) ∘
          fun (N : ℤ) ↦ Ico (-N) N)
        Nat.cast N)
      (∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
⊢ Tendsto (β := ℂ)
    (fun (N : ℕ) ↦
      ∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    atTop
    (𝓝
      (∑'[{ filter := Filter.map (fun (N : ℤ) ↦ Ico (-N) N) (Filter.map Nat.cast atTop) }] (x : ℤ),
        (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }))

Tactic:
apply this.congr (fun N ↦ ?_)

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  Tendsto (β := ℂ)
    (Function.comp (β := ℤ)
      ((fun (s : Finset ℤ) ↦
          ∑ x ∈ s, (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) ∘
        fun (N : ℤ) ↦ Ico (-N) N)
      Nat.cast)
    atTop
    (𝓝
      (∑'[{ filter := Filter.map (fun (N : ℤ) ↦ Ico (-N) N) (Filter.map Nat.cast atTop) }] (x : ℤ),
        (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }))
N : ℕ
⊢ Eq (α := ℂ)
    (Function.comp (β := ℤ)
      ((fun (s : Finset ℤ) ↦
          ∑ x ∈ s, (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ }) ∘
        fun (N : ℤ) ↦ Ico (-N) N)
      Nat.cast N)
    (∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)

Tactic:
simpa [e2Summand, eisSummand, ← mul_sum] using aux_sum_Ico_S_identity z N

Premises used: Finset.mul_sum, EisensteinSeries.e2Summand, _private.0.EisensteinSeries.aux_sum_Ico_S_identity, EisensteinSeries.eisSummand
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
ha :
  HasSum (fun (b : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
    ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)
⊢ ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2 =
    (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)

Tactic:
apply HasSum.tsum_eq

Premises used: HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
ha :
  Tendsto
    (fun (N : ℕ) ↦
      ∑ n ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
    atTop (𝓝 ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)))
⊢ HasSum (fun (b : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 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.Summable
Goal:
z : ℍ
apply :
  ∀ (x : ℕ),
    Eq (α := ℂ) (∑' (n : ℤ), ∑ m ∈ Ico (-(↑x : ℤ)) (↑x : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
      (∑ n ∈ Ico (-(↑x : ℤ)) (↑x : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑ n ∈ 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.Summable
Goal:
z : ℍ
x : ℕ
rw :
  ∀ (i : ℤ),
    Membership.mem (γ := Finset ℤ) (Ico (-(↑x : ℤ)) (↑x : ℤ)) i →
      Summable (α := ℂ) fun (n : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2
⊢ Eq (α := ℂ) (∑' (n : ℤ), ∑ m ∈ Ico (-(↑x : ℤ)) (↑x : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    (∑ n ∈ Ico (-(↑x : ℤ)) (↑x : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)

Tactic:
rw [Summable.tsum_finsetSum]

Premises used: Summable.tsum_finsetSum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
x : ℕ
i : ℤ
hi : Membership.mem (γ := 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 le_rfl

Premises used: le_rfl, EisensteinSeries.linear_left_summable, UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
x : ℕ
⊢ ∀ (i : ℤ),
    Membership.mem (γ := Finset ℤ) (Ico (-(↑x : ℤ)) (↑x : ℤ)) i →
      Summable (α := ℂ) fun (n : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2

Tactic:
exact fun i hi ↦ by simpa using linear_left_summable (ne_zero z) i le_rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℂ
m : ℤ
b : ℕ
⊢ ∑ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), (1 / ((↑m : ℂ) * z + (↑n : ℂ)) - 1 / ((↑m : ℂ) * z + (↑(n + 1) : ℂ))) =
    1 / ((↑m : ℂ) * z + (↑(-(↑b : ℤ)) : ℂ)) - 1 / ((↑m : ℂ) * z + (↑(↑b : ℤ) : ℂ))

Tactic:
sum_Ico_int_sub b (fun n ↦ 1 / ((m : ℂ) * z + n))

Premises used: Int.cast, HMul.hMul, Finset.sum_Ico_int_sub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℂ
m : ℤ
b : ℕ
h :
  ∀ (x : ℤ),
    Membership.mem (γ := Finset ℤ) (Ico (-(↑b : ℤ)) (↑b : ℤ)) x →
      1 / ((↑m : ℂ) * z + (↑x : ℂ)) - 1 / ((↑m : ℂ) * z + (↑x : ℂ) + 1) =
        1 / ((↑m : ℂ) * z + (↑x : ℂ)) - 1 / ((↑m : ℂ) * z + (↑(x + 1) : ℂ))
h₁ : 1 / ((↑m : ℂ) * z - (↑b : ℂ)) = 1 / ((↑m : ℂ) * z + (↑(-(↑b : ℤ)) : ℂ))
⊢ ∑ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), (1 / ((↑m : ℂ) * z + (↑n : ℂ)) - 1 / ((↑m : ℂ) * z + (↑n : ℂ) + 1)) =
    1 / ((↑m : ℂ) * z - (↑b : ℂ)) - 1 / ((↑m : ℂ) * z + (↑b : ℂ))

Tactic:
convert! sum_Ico_int_sub b (fun n ↦ 1 / ((m : ℂ) * z + n)) using 2

Premises used: Int.cast, HMul.hMul, Finset.sum_Ico_int_sub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℂ
m : ℤ
b : ℕ
x : ℤ
h : Membership.mem (γ := Finset ℤ) (Ico (-(↑b : ℤ)) (↑b : ℤ)) x
⊢ 1 / ((↑m : ℂ) * z + (↑x : ℂ)) - 1 / ((↑m : ℂ) * z + (↑x : ℂ) + 1) =
    1 / ((↑m : ℂ) * z + (↑x : ℂ)) - 1 / ((↑m : ℂ) * z + (↑(x + 1) : ℂ))

Tactic:
simp [add_assoc, sub_eq_add_neg]

Premises used: add_assoc, sub_eq_add_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℂ
m : ℤ
b : ℕ
⊢ 1 / ((↑m : ℂ) * z - (↑b : ℂ)) = 1 / ((↑m : ℂ) * z + (↑(-(↑b : ℤ)) : ℂ))

Tactic:
simp [add_assoc, sub_eq_add_neg]

Premises used: add_assoc, sub_eq_add_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
ha :
  HasSum (α := ℂ) (fun (b : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)) 0
    (symmetricIco ℤ)
⊢ Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))) 0

Tactic:
apply HasSum.tsum_eq

Premises used: HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
ha :
  Tendsto (β := ℂ) (fun (N : ℕ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) - (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ))) atTop
    (𝓝 0)
⊢ HasSum (α := ℂ) (fun (b : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)) 0
    (symmetricIco ℤ)

Tactic:
simp_rw [hasSum_symmetricIco_int_iff, telescope_aux z m]

Premises used: UpperHalfPlane.coe, SummationFilter.hasSum_symmetricIco_int_iff, _private.0.EisensteinSeries.telescope_aux
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
m : ℤ
⊢ Tendsto (β := ℂ) (fun (N : ℕ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) - (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ))) atTop
    (𝓝 0)

Tactic:
simpa using (tendsto_zero_inv_linear_sub z m).sub (tendsto_zero_inv_linear z m)

Premises used: UpperHalfPlane.coe, EisensteinSeries.tendsto_zero_inv_linear_sub, EisensteinSeries.tendsto_zero_inv_linear, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
rw :
  HDiv.hDiv (α := ℂ) 2 (↑(↑d : ℕ) : ℂ) +
      (1 / ((↑0 : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) - 1 / ((↑0 : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) +
          ∑' (n : ℕ+),
            (1 / ((↑(↑(↑n : ℕ) : ℤ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) -
              1 / ((↑(↑(↑n : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))) +
        ∑' (n : ℕ+),
          (1 / ((↑(-(↑(↑n : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) -
            1 / ((↑(-(↑(↑n : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)))) =
    ∑' (m : ℕ+),
      (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
          1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
        1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)))
rw₁ :
  Summable (α := ℂ) fun (m : ℤ) ↦
    1 / ((↑m : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))
⊢ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))) =
    -HDiv.hDiv (α := ℂ) 2 (↑(↑d : ℕ) : ℂ) +
      ∑' (m : ℕ+),
        (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
            1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
          1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)))

Tactic:
rw [eq_neg_add_iff_add_eq (b := 2 / (d : ℂ)), tsum_int_eq_zero_add_tsum_pnat]

Premises used: tsum_int_eq_zero_add_tsum_pnat, eq_neg_add_iff_add_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
simp :
  HDiv.hDiv (α := ℂ) 2 (↑(↑d : ℕ) : ℂ) +
      (HSub.hSub (α := ℂ) (-(↑(↑d : ℕ) : ℂ))⁻¹ (↑(↑d : ℕ) : ℂ)⁻¹ +
          ∑' (n : ℕ+),
            (((↑(↑n : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ))⁻¹ - ((↑(↑n : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))⁻¹) +
        ∑' (n : ℕ+),
          ((-((↑(↑n : ℕ) : ℂ) * (↑z : ℂ)) - (↑(↑d : ℕ) : ℂ))⁻¹ - (-((↑(↑n : ℕ) : ℂ) * (↑z : ℂ)) + (↑(↑d : ℕ) : ℂ))⁻¹)) =
    ∑' (m : ℕ+),
      (((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ))⁻¹ + (-((↑(↑m : ℕ) : ℂ) * (↑z : ℂ)) + -(↑(↑d : ℕ) : ℂ))⁻¹ -
          ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))⁻¹ -
        (-((↑(↑m : ℕ) : ℂ) * (↑z : ℂ)) + (↑(↑d : ℕ) : ℂ))⁻¹)
⊢ HDiv.hDiv (α := ℂ) 2 (↑(↑d : ℕ) : ℂ) +
      (1 / ((↑0 : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) - 1 / ((↑0 : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) +
          ∑' (n : ℕ+),
            (1 / ((↑(↑(↑n : ℕ) : ℤ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) -
              1 / ((↑(↑(↑n : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))) +
        ∑' (n : ℕ+),
          (1 / ((↑(-(↑(↑n : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) -
            1 / ((↑(-(↑(↑n : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)))) =
    ∑' (m : ℕ+),
      (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
          1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
        1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)))

Tactic:
simp only [Int.cast_zero, zero_mul, zero_sub, one_div, zero_add, Int.cast_natCast, Int.cast_neg,
      neg_mul]

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_zero, MulZeroClass.zero_mul, zero_add, one_div, neg_mul, zero_sub