awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ+
h2 :
  (↑π : ℂ) * ((↑π : ℂ) * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)).cot =
    1 / (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ) +
      ∑' (n : ℕ+),
        (1 / ((↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ) - (↑(↑n : ℕ) : ℂ)) +
          1 / ((↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ) + (↑(↑n : ℕ) : ℂ)))
⊢ 2 / (↑z : ℂ) *
      ∑' (m : ℕ+),
        (1 / (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))) =
    -2 * (↑π : ℂ) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
      HDiv.hDiv (α := ℂ) 2 (↑(↑N : ℕ) : ℂ)
have h : ∀
  (h2 :
    (↑π : ℂ) * I -
          2 * (↑π : ℂ) * I *
            (HPow.hPow (β := ℕ)
                (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ))) 0 +
              ∑' (n : ℕ+),
                cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ)) ^
                  (↑n : ℕ)) -
        (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ) =
      (↑π : ℂ) * I -
          2 * (↑π : ℂ) * I *
            (HPow.hPow (β := ℕ)
                (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ))) 0 +
              ∑' (n : ℕ+),
                cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ)) ^
                  (↑n : ℕ)) -
        (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ)),
  2 / (↑z : ℂ) *
        ((↑π : ℂ) * I -
            2 * (↑π : ℂ) * I *
              (HPow.hPow (β := ℕ)
                  (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ))) 0 +
                ∑' (n : ℕ+),
                  cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ)) ^
                    (↑n : ℕ)) -
          (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ)) -
      (-(2 * (↑π : ℂ)) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ)) =
    HDiv.hDiv (α := ℂ) 2 (↑(↑N : ℕ) : ℂ)
Tactic: rw [pi_mul_cot_pi_q_exp, ← sub_eq_iff_eq_add', one_div, inv_div, neg_mul, ← h2,
      ← tsum_zero_pnat_eq_tsum_nat
      (by simpa using norm_exp_two_pi_I_lt_one ⟨-N / z, im_pnat_div_pos N z⟩)] at *
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
⊢ Tendsto
    (fun (x : ℕ+) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+),
          (1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
have H0 : Eq (α := (n : ℕ+) → ℂ)
  (fun (n : ℕ+) ↦
    2 / (↑z : ℂ) *
      ∑' (m : ℕ+),
        (1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
  fun (n : ℕ+) ↦
  -2 * (↑π : ℂ) * I / (↑z : ℂ) -
      2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
        ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
    HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ)
Tactic: have H0 : (fun n : ℕ+ ↦ (2 / z * ∑' (m : ℕ+), (1 / (-(n : ℂ) / z - m) + 1 / (-n / z + m)))) =
      (fun n : ℕ+ ↦ (-2 * π * I / z) - (2 / z * (2 * π * I)) *
      (∑' m : ℕ+, cexp (2 * π * I * (-n / z)) ^ (m : ℕ)) + 2 / n) := by
    ext N
    have h2 := cot_series_rep <| coe_mem_integerComplement ⟨-N / z, im_pnat_div_pos N z⟩
    rw [pi_mul_cot_pi_q_exp, ← sub_eq_iff_eq_add', one_div, inv_div, neg_mul, ← h2,
      ← tsum_zero_pnat_eq_tsum_nat
      (by simpa using norm_exp_two_pi_I_lt_one ⟨-N / z, im_pnat_div_pos N z⟩)] at *
    field [ne_zero z]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
H0 :
  Eq (α := (n : ℕ+) → ℂ)
    (fun (n : ℕ+) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+),
          (1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    fun (n : ℕ+) ↦
    -2 * (↑π : ℂ) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
      HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ)
⊢ Tendsto
    (fun (x : ℕ+) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+),
          (1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
have rw : Tendsto
  (fun (n : ℕ+) ↦
    -2 * (↑π : ℂ) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
      HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ))
  atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
Tactic: rw [H0]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
H0 :
  Eq (α := (n : ℕ+) → ℂ)
    (fun (n : ℕ+) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+),
          (1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    fun (n : ℕ+) ↦
    -2 * (↑π : ℂ) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
      HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ)
⊢ Tendsto
    (fun (n : ℕ+) ↦
      -2 * (↑π : ℂ) * I / (↑z : ℂ) -
          2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
            ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
        HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
have nth_rw : Tendsto
  (fun (n : ℕ+) ↦
    -2 * (↑π : ℂ) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
      HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ))
  atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ) - 2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) * 0 + HMul.hMul (α := ℂ) 2 0))
Tactic: nth_rw 2 [show -2 * π * I / z = (-2 * π * I / z) - (2 / z * (2 * π * I)) * 0 + 2 * 0 by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
H0 :
  Eq (α := (n : ℕ+) → ℂ)
    (fun (n : ℕ+) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+),
          (1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    fun (n : ℕ+) ↦
    -2 * (↑π : ℂ) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
      HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ)
⊢ Tendsto
    (fun (n : ℕ+) ↦
      -2 * (↑π : ℂ) * I / (↑z : ℂ) -
          2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
            ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑n : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ) +
        HDiv.hDiv (α := ℂ) 2 (↑(↑n : ℕ) : ℂ))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ) - 2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) * 0 + HMul.hMul (α := ℂ) 2 0))
have refine : Tendsto (β := ℂ) (fun (n : ℕ+) ↦ (↑(↑n : ℕ) : ℂ)⁻¹) atTop (𝓝 0)
Tactic: refine aux_tendsto_tsum_cexp_pnat z |>.const_mul _ |>.const_sub _ |>.add (.const_mul _ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ+
⊢ Eq (α := ℂ)
    (∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
      ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (∑' (m : ℤ),
      ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
have rw : ∀ (i : ℤ) (hi : Membership.mem (γ := Finset ℤ) (Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ)) i),
  Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ) + 1)
Tactic: rw [Summable.tsum_finsetSum (fun i hi ↦ ?_)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
N : ℕ+
i : ℤ
hi : Membership.mem (γ := Finset ℤ) (Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ)) i
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ) + 1)
have apply : ∀ (b : ℤ),
  1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑(i + 1) : ℂ)) =
    1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ) + 1)
Tactic: apply (summable_left_one_div_linear_sub_one_div_linear z i (i + 1)).congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
⊢ Tendsto
    (fun (N : ℕ+) ↦
      ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
have this : ∀ (N : ℕ+),
  Eq (α := ℂ)
    (∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
      ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    (∑' (m : ℤ),
      ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
Tactic: have (N : ℕ+) :
      ∑ n ∈ Ico (-N : ℤ) N, ∑' m : ℤ, (1 / ((m : ℂ) * z + n) - 1 / (m * z + n + 1))
      = ∑' m : ℤ, ∑ n ∈ Ico (-N : ℤ) N, (1 / ((m : ℂ) * z + n) - 1 / (m * z + n + 1)) := by
    rw [Summable.tsum_finsetSum (fun i hi ↦ ?_)]
    apply (summable_left_one_div_linear_sub_one_div_linear z i (i + 1)).congr
    grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
this :
  ∀ (N : ℕ+),
    Eq (α := ℂ)
      (∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
      (∑' (m : ℤ),
        ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
          (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
⊢ Tendsto
    (fun (N : ℕ+) ↦
      ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
have this₁ : ∀ (N : ℕ+),
  ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
      ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)) =
    -HDiv.hDiv (α := ℂ) 2 (↑(↑N : ℕ) : ℂ) +
      ∑' (m : ℕ+),
        (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑N : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑N : ℕ) : ℂ)) -
            1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)) -
          1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)))
Tactic: simp only [telescope_aux, aux_tsum_identity_1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)) =
      -HDiv.hDiv (α := ℂ) 2 (↑(↑N : ℕ) : ℂ) +
        ∑' (m : ℕ+),
          (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑N : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑N : ℕ) : ℂ)) -
              1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)) -
            1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)))
⊢ Tendsto
    (fun (N : ℕ+) ↦
      ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
have rw : Tendsto
  (fun (x : ℕ+) ↦
    -HDiv.hDiv (α := ℂ) 2 (↑(↑x : ℕ) : ℂ) +
      ∑' (m : ℕ+),
        (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑x : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑x : ℕ) : ℂ)) -
            1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ)) -
          1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ))))
  atTop (𝓝 (0 + -2 * (↑π : ℂ) * I / (↑z : ℂ)))
Tactic: rw [funext this, show -2 * π * I / z = 0 + -2 * π * I / z by ring]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)) =
      -HDiv.hDiv (α := ℂ) 2 (↑(↑N : ℕ) : ℂ) +
        ∑' (m : ℕ+),
          (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑N : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑N : ℕ) : ℂ)) -
              1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)) -
            1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)))
⊢ Tendsto
    (fun (x : ℕ+) ↦
      -HDiv.hDiv (α := ℂ) 2 (↑(↑x : ℕ) : ℂ) +
        ∑' (m : ℕ+),
          (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑x : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑x : ℕ) : ℂ)) -
              1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ)) -
            1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ))))
    atTop (𝓝 (0 + -2 * (↑π : ℂ) * I / (↑z : ℂ)))
have hf : Tendsto (β := ℂ) (fun (x : ℕ+) ↦ -HDiv.hDiv (α := ℂ) 2 (↑(↑x : ℕ) : ℂ)) atTop (𝓝 0)
Tactic: apply Tendsto.add
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ),
        ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)) =
      -HDiv.hDiv (α := ℂ) 2 (↑(↑N : ℕ) : ℂ) +
        ∑' (m : ℕ+),
          (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑N : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑N : ℕ) : ℂ)) -
              1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)) -
            1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑N : ℕ) : ℂ)))
hf : Tendsto (β := ℂ) (fun (x : ℕ+) ↦ -HDiv.hDiv (α := ℂ) 2 (↑(↑x : ℕ) : ℂ)) atTop (𝓝 0)
⊢ Tendsto
    (fun (x : ℕ+) ↦
      -HDiv.hDiv (α := ℂ) 2 (↑(↑x : ℕ) : ℂ) +
        ∑' (m : ℕ+),
          (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑x : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑x : ℕ) : ℂ)) -
              1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ)) -
            1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ))))
    atTop (𝓝 (0 + -2 * (↑π : ℂ) * I / (↑z : ℂ)))
have hg : Tendsto
  (fun (x : ℕ+) ↦
    ∑' (m : ℕ+),
      (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑x : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑x : ℕ) : ℂ)) -
          1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ)) -
        1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ))))
  atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
Tactic: apply Tendsto.add
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ ∑'[symmetricIco ℤ] (n : ℤ),
      ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)) =
    -2 * (↑π : ℂ) * I / (↑z : ℂ)
have ha : HasSum (fun (b : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)))
  (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)
Tactic: apply HasSum.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ Eq (α := ℂ)
    (∑' (m : ℤ),
      ∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    0
have h : ∀ (x : ℤ),
  Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))) 0
Tactic: convert! tsum_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
⊢ δ =ᶠ[cofinite] 0
have h : ∀ (x : Fin 2 → ℤ) (hx : x ≠ ![0, 0]) (hx' : x ≠ ![0, -1]), δ x = 0 x
Tactic: filter_upwards [eventually_cofinite_ne ![0, 0], eventually_cofinite_ne ![0, -1]] with x hx hx'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦ G2Term z m - δ m
have simp_rw : Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦
  (HPow.hPow (β := ℕ) ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ)) 2 * ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + 1))⁻¹
Tactic: simp_rw [G2Term, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ LT.lt (α := ℝ) 2 3
have linarith : LE.le (α := ℝ) 3 2 → -1 + HSub.hSub (α := ℝ) 3 2 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
⊢ Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦
    (HPow.hPow (β := ℕ) ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ)) 2 * ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + 1))⁻¹
have apply : Asymptotics.IsBigO (E := ℂ) (F := ℝ) cofinite
  (fun (m : Fin 2 → ℤ) ↦
    (HPow.hPow (β := ℕ) ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ)) 2 * ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + 1))⁻¹)
  fun (n : Fin 2 → ℤ) ↦ (HPow.hPow (β := ℝ) ‖n‖ 3)⁻¹
Tactic: apply summable_of_isBigO_rpow_norm (a := 3) (by linarith)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
⊢ Summable (G2Term z)
have H : Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦ G2Term z m - δ m
Tactic: have H : Summable fun m ↦ G2Term z m - δ m := by
    simp_rw [G2Term, add_sub_cancel_right]
    apply summable_of_isBigO_rpow_norm (a := 3) (by linarith)
    simpa [pow_three, pow_two, ← mul_assoc] using ((isBigO_linear_add_const_vec z 0 1).mul
      (isBigO_linear_add_const_vec z 0 0)).mul (isBigO_linear_add_const_vec z 0 0)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
b n : ℤ
⊢ ((↑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 pos : ∀ (h : b = 0 ∧ 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)⁻¹
Tactic: by_cases h : b = 0 ∧ n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
b n : ℤ
pos :
  ∀ (h : b = 0 ∧ 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)⁻¹
⊢ ((↑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 : ∀ (h : ¬(b = 0 ∧ 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)⁻¹
Tactic: by_cases h : b = 0 ∧ n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (hypothesis)
Goal:
z : ℍ
b n : ℤ
h : ¬(b = 0 ∧ 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 h₁ : b = 0 → ¬n = 0
Tactic: simp only [not_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬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 pos : ∀ (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)⁻¹
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
pos :
  ∀ (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)⁻¹
⊢ ((↑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 : ∀ (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)⁻¹
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
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 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)⁻¹
Tactic: by_cases hn : n = -1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
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)⁻¹
⊢ ((↑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 : ∀ (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)⁻¹
Tactic: by_cases hn : n = -1
-- 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
⊢ ((↑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 pos : HAdd.hAdd (α := ℂ) 2 (-1) = 1
Tactic: simp [hb, hn, δ_eq_two]