awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
b : ℕ+
⊢ 2 *
      (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
        (cexp ((↑b : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑b : ℕ) : ℂ))) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
            (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ)))))
have e_a : HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑(↑b : ℕ) : ℂ) *
      cexp (I * (↑π : ℂ) * (↑z : ℂ) * (↑a : ℂ) * (↑(↑b : ℕ) : ℂ) * 2 + I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * 2) *
    8 =
  -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑(↑b : ℕ) : ℂ) * cexp (I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * 2) *
        cexp (I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * (↑a : ℂ) * 2) *
      8)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
⊢ -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
have this : Eq (α := ℂ)
  (∑' (d : ℕ+) (c : ℕ+),
    HPow.hPow (α := ℂ) (β := ℕ) (↑(↑c : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑d : ℕ) * (↑c : ℕ)))
  (∑' (e : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑e : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑e : ℕ))
Tactic: have := tsum_prod_pow_eq_tsum_sigma 1 (norm_exp_two_pi_I_lt_one z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
this :
  Eq (α := ℂ)
    (∑' (d : ℕ+) (c : ℕ+),
      HPow.hPow (α := ℂ) (β := ℕ) (↑(↑c : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑e : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑e : ℕ))
⊢ -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
have this₁ : Eq (α := ℂ)
  (∑' (n : ℕ) (c : ℕ+),
    HPow.hPow (α := ℂ) (β := ℕ) (↑(↑c : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((n + 1) * (↑c : ℕ)))
  (∑' (e : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑e : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑e : ℕ))
Tactic: rw [tsum_pnat_eq_tsum_succ (f := fun d ↦ ∑' c : ℕ+, c ^ 1 * 𝕢 z ^ (d * c : ℕ))] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
    atTop
    (𝓝
      (-8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)))
have this : -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
    ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
  ∑' (m : ℕ),
    -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
Tactic: have : -8 * π ^ 2 * ∑' n : ℕ+, σ 1 n * 𝕢 z ^ (n : ℕ) =
      ∑' m : ℕ, (-8 * π ^ 2 * ∑' n : ℕ+, n * 𝕢 z ^ ((m + 1) * n)) := by
    have := tsum_prod_pow_eq_tsum_sigma 1 (norm_exp_two_pi_I_lt_one z)
    rw [tsum_pnat_eq_tsum_succ (f := fun d ↦ ∑' c : ℕ+, c ^ 1 * 𝕢 z ^ (d * c : ℕ))] at this
    simp [← tsum_mul_left, ← this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
    atTop
    (𝓝
      (-8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)))
have rw : Tendsto (β := ℂ)
  (fun (N : ℕ) ↦
    ∑ m ∈ range N,
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
  atTop
  (𝓝
    (∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
⊢ Tendsto (β := ℂ)
    (fun (N : ℕ) ↦
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
    atTop
    (𝓝
      (∑' (m : ℕ),
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))))
have refine : Summable (α := ℂ) fun (m : ℕ) ↦ ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
Tactic: refine (Summable.mul_left _ ?_).hasSum.comp tendsto_finset_range
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
⊢ Summable (α := ℂ) fun (m : ℕ) ↦
    ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
have rw : Summable (α := ℂ) fun (x : ℕ+) ↦
  ∑' (c : ℕ+), (↑(↑c : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑x : ℕ) * (↑c : ℕ))
Tactic: rw [← summable_pnat_iff_summable_succ (f := fun b ↦ ∑' c : ℕ+, c * 𝕢 z ^ (b * c : ℕ))]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
⊢ Summable (α := ℂ) fun (x : ℕ+) ↦
    ∑' (c : ℕ+), (↑(↑c : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑x : ℕ) * (↑c : ℕ))
have apply : ∀ (b : ℕ+),
  Eq (α := ℂ)
    (∑' (c : ℕ+),
      HPow.hPow (α := ℂ) (β := ℕ) (↑(↑(b, c).2 : ℕ) : ℂ) 1 *
        cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑(b, c).1 : ℕ) * (↑(b, c).2 : ℕ)))
    (∑' (c : ℕ+), (↑(↑c : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑b : ℕ) * (↑c : ℕ)))
Tactic: apply (summable_prod_mul_pow 1 (norm_exp_two_pi_I_lt_one z)).prod.congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ E2 z =
    1 -
      HMul.hMul (α := ℂ) 24
        (∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
have simp : 6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
    (2 * (HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6) -
      8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)) =
  1 -
    HMul.hMul (α := ℂ) 24
      (∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
Tactic: simp [E2, G2_eq_tsum_cexp, riemannZeta_two]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ HasSum (fun (x : ℤ) ↦ e2Summand x z)
    (2 * riemannZeta 2 -
      8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
    (symmetricIco ℤ)
have apply : Tendsto (β := ℂ) (fun (N : ℕ) ↦ -e2Summand (↑N : ℤ) z) atTop (𝓝 0)
Tactic: apply (hasSum_e2Summand_symmetricIcc z).hasSum_symmetricIco_of_hasSum_symmetricIcc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ G2 z = ∑'[symmetricIco ℤ] (m : ℤ), e2Summand m z
have rw : Tendsto (β := ℂ) (fun (N : ℕ) ↦ -e2Summand (↑N : ℤ) z) atTop (𝓝 0)
Tactic: rw [G2, tsum_symmetricIcc_eq_tsum_symmetricIco (summable_e2Summand_symmetricIcc z)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))
have rw : 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) - ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ))) *
    (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))) =
  HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))
Tactic: rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
rw :
  1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) - ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ))) *
      (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))
⊢ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))
have ha : (↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ) ≠ 0
Tactic: rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
rw :
  1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) - ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ))) *
      (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))
ha : (↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ) ≠ 0
⊢ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))
have hb : (↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) ≠ 0
Tactic: rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
a b : ℤ
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))
have this : Summable (α := ℂ) fun (i : ℤ) ↦
  HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (((↑i : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑i : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹
Tactic: have := Summable.mul_left (b - a : ℂ) (summable_linear_left_mul_linear_left (ne_zero z) a b)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
a b : ℤ
this :
  Summable (α := ℂ) fun (i : ℤ) ↦
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (((↑i : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑i : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))
have 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 : ℂ))
Tactic: rw [← Finset.summable_compl_iff (s := {0})] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
a b : ℤ
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 : ℂ))
have apply : ∀ (m : { x : ℤ // x ∉ {0} }),
  HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) *
      (((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹ =
    1 / ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑(↑m : ℤ) : ℂ) * (↑z : ℂ) + (↑b : ℂ))
Tactic: apply this.congr (fun m ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
m : ℤ
⊢ Summable (α := ℂ) fun (b : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)
have this : Summable (α := ℂ) fun (n : ℤ) ↦ (((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)))⁻¹
Tactic: have := summable_linear_right_add_one_mul_linear_right z m m
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
m : ℤ
this : Summable (α := ℂ) fun (n : ℤ) ↦ (((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)))⁻¹
⊢ Summable (α := ℂ) fun (b : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)
have 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)
Tactic: rw [← Finset.summable_compl_iff (s := {0, -1})] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
m : ℤ
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)
have apply : ∀ (b : { x : ℤ // x ∉ {0, -1} }),
  (((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ) + 1) * ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ)))⁻¹ =
    1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑b : ℤ) : ℂ) + 1)
Tactic: apply this.congr (fun b ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
⊢ (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)⁻¹
have 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)⁻¹)
Tactic: simp_rw [inv_neg, mul_neg, mul_sum, pow_two, ← zpow_two]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
⊢ 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)⁻¹)
have 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)⁻¹)
Tactic: rw [Summable.tsum_finsetSum (fun i hi ↦ linear_left_summable (ne_zero z) i le_rfl)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
⊢ 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)⁻¹)
have 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)⁻¹
Tactic: apply sum_congr rfl fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ
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)⁻¹
have rw : Eq (α := ℂ)
  (∑' (d : ℤ), (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * (HPow.hPow (β := ℤ) (-((↑n : ℂ) * (↑z : ℂ)⁻¹) + (↑(-d) : ℂ)) 2)⁻¹)
  (∑' (b : ℤ), (HPow.hPow (β := ℤ) ((↑b : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)⁻¹)
Tactic: rw [← tsum_mul_left, ← tsum_comp_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    atTop (𝓝 ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)))
have 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)))
Tactic: rw [G2_eq_tsum_symmetricIco, ← tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
⊢ 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)))
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
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 ℤ)
⊢ 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)))
have simp : ∀
  (this :
    Tendsto (β := ℂ)
      (Function.comp (β := ℤ)
        ((fun (s : Finset ℤ) ↦
            ∑ x ∈ s, (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ }) ∘
          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 := sorry : ℍ }))),
  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 := sorry : ℍ }))
Tactic: simp only [HasSum, symmetricIco, tendsto_map'_iff, modular_S_smul, ← Nat.map_cast_int_atTop] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
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 := ⋯ : ℍ }))
⊢ 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 := ⋯ : ℍ }))
have apply : ∀ (N : ℕ),
  Eq (α := ℂ)
    (Function.comp (β := ℤ)
      ((fun (s : Finset ℤ) ↦
          ∑ x ∈ s, (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * e2Summand x { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry : ℍ }) ∘
        fun (N : ℤ) ↦ Ico (-N) N)
      Nat.cast N)
    (∑' (n : ℤ), ∑ m ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
Tactic: apply this.congr (fun N ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2 =
    (HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)
have ha : HasSum (fun (b : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
  ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)
Tactic: apply HasSum.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ HasSum (fun (b : ℤ) ↦ ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) 2)
    ((HPow.hPow (β := ℕ) (↑z : ℂ) 2)⁻¹ * G2 (S • z)) (symmetricIco ℤ)
have ha : Tendsto
  (fun (N : ℕ) ↦ ∑ n ∈ 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.Summable (goal)
Goal:
z : ℍ
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑ n ∈ 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 ∈ Ico (-(↑x : ℤ)) (↑x : ℤ), 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑m : ℂ)) 2)
    (∑ n ∈ Ico (-(↑x : ℤ)) (↑x : ℤ), ∑' (m : ℤ), 1 / HPow.hPow (β := ℕ) ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) 2)
Tactic: apply (tendsto_double_sum_S_act z).congr (fun x ↦ ?_)