awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
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)
have rw : ∀ (i : ℤ),
  Membership.mem (γ := Finset ℤ) (Ico (-(↑x : ℤ)) (↑x : ℤ)) i →
    Summable (α := ℂ) fun (n : ℤ) ↦ 1 / HPow.hPow (β := ℕ) ((↑n : ℂ) * (↑z : ℂ) + (↑i : ℂ)) 2
Tactic: rw [Summable.tsum_finsetSum]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
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 : ℂ))
have 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) : ℂ))
Tactic: convert! sum_Ico_int_sub b (fun n ↦ 1 / ((m : ℂ) * z + n)) using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
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) : ℂ))
⊢ ∑ n ∈ Ico (-(↑b : ℤ)) (↑b : ℤ), (1 / ((↑m : ℂ) * z + (↑n : ℂ)) - 1 / ((↑m : ℂ) * z + (↑n : ℂ) + 1)) =
    1 / ((↑m : ℂ) * z - (↑b : ℂ)) - 1 / ((↑m : ℂ) * z + (↑b : ℂ))
have h₁ : 1 / ((↑m : ℂ) * z - (↑b : ℂ)) = 1 / ((↑m : ℂ) * z + (↑(-(↑b : ℤ)) : ℂ))
Tactic: convert! sum_Ico_int_sub b (fun n ↦ 1 / ((m : ℂ) * z + n)) using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
m : ℤ
⊢ Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))) 0
have ha : HasSum (α := ℂ) (fun (b : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)) 0
  (symmetricIco ℤ)
Tactic: apply HasSum.tsum_eq
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
m : ℤ
⊢ HasSum (α := ℂ) (fun (b : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)) 0
    (symmetricIco ℤ)
have ha : Tendsto (β := ℂ) (fun (N : ℕ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) - (↑N : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑N : ℂ))) atTop (𝓝 0)
Tactic: simp_rw [hasSum_symmetricIco_int_iff, telescope_aux z m]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
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 : ℕ) : ℂ)))
have 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 : ℕ) : ℂ)))
Tactic: rw [eq_neg_add_iff_add_eq (b := 2 / (d : ℂ)), tsum_int_eq_zero_add_tsum_pnat]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
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 : ℕ) : ℂ)))
⊢ ∑' (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 : ℕ) : ℂ)))
have rw₁ : Summable (α := ℂ) fun (m : ℤ) ↦
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
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 : ℕ) : ℂ)))
have 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 : ℕ) : ℂ))⁻¹)
Tactic: simp only [Int.cast_zero, zero_mul, zero_sub, one_div, zero_add, Int.cast_natCast, Int.cast_neg,
      neg_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
⊢ 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 : ℕ) : ℂ))⁻¹)
have ring_nf : HAdd.hAdd (α := ℂ)
    (∑' (n : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹))
    (∑' (n : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹)) =
  ∑' (m : ℕ+),
    ((-(↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
        ((↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
      ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
⊢ HAdd.hAdd (α := ℂ)
      (∑' (n : ℕ+),
        ((-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹))
      (∑' (n : ℕ+),
        ((-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹)) =
    ∑' (m : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
          ((↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
        ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹)
have rw : Eq (α := ℂ)
  (∑' (b : ℕ+),
    ((-(↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ +
      ((-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹)))
  (∑' (m : ℕ+),
    ((-(↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
        ((↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
      ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹))
Tactic: rw [← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
rw :
  Eq (α := ℂ)
    (∑' (b : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ +
        ((-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹)))
    (∑' (m : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
          ((↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
        ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹))
⊢ HAdd.hAdd (α := ℂ)
      (∑' (n : ℕ+),
        ((-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹))
      (∑' (n : ℕ+),
        ((-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹)) =
    ∑' (m : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
          ((↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
        ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹)
have hf : Summable (α := ℂ) fun (n : ℕ+) ↦
  (-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹
Tactic: rw [← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
rw :
  Eq (α := ℂ)
    (∑' (b : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ +
        ((-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹)))
    (∑' (m : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
          ((↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
        ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹))
hf :
  Summable (α := ℂ) fun (n : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹
⊢ HAdd.hAdd (α := ℂ)
      (∑' (n : ℕ+),
        ((-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹))
      (∑' (n : ℕ+),
        ((-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹)) =
    ∑' (m : ℕ+),
      ((-(↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
          ((↑(↑d : ℕ) : ℂ) + (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹ -
        ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑m : ℕ) : ℂ))⁻¹)
have hg : Summable (α := ℂ) fun (n : ℕ+) ↦
  (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹
Tactic: rw [← Summable.tsum_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
⊢ Summable (α := ℂ) fun (n : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹
have hf : ∀ (b : ℕ+),
  1 / ((↑(↑(↑b : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(-(↑(↑d : ℕ) : ℤ)) : ℂ)) -
      1 / ((↑(↑(↑b : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(↑(↑d : ℕ) : ℤ) : ℂ)) =
    (-(↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹
Tactic: apply (summable_pnat_iff_summable_nat.mpr ((summable_int_iff_summable_nat_and_neg.mp
        (summable_left_one_div_linear_sub_one_div_linear z (-d) d)).1)).congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
⊢ Summable (α := ℂ) fun (n : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹
have hg : ∀ (b : ℕ+),
  1 / ((↑(-(↑(↑b : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(-(↑(↑d : ℕ) : ℤ)) : ℂ)) -
      1 / ((↑(-(↑(↑b : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(↑(↑d : ℕ) : ℤ) : ℂ)) =
    (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹
Tactic: apply (summable_pnat_iff_summable_nat.mpr ((summable_int_iff_summable_nat_and_neg.mp
        (summable_left_one_div_linear_sub_one_div_linear z (-d) d)).2)).congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
⊢ ∑' (m : ℕ+),
      (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
          1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
        1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))) =
    2 / (↑z : ℂ) *
      ∑' (m : ℕ+),
        (1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ)))
have rw : Eq (α := ℂ)
  (∑' (m : ℕ+),
    (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
        1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
      1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))))
  (∑' (i : ℕ+),
    2 / (↑z : ℂ) *
      (1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑i : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑i : ℕ) : ℂ))))
Tactic: rw [← Summable.tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
rw :
  Eq (α := ℂ)
    (∑' (m : ℕ+),
      (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
          1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
        1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))))
    (∑' (i : ℕ+),
      2 / (↑z : ℂ) *
        (1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑i : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑i : ℕ) : ℂ))))
⊢ ∑' (m : ℕ+),
      (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
          1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
        1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))) =
    2 / (↑z : ℂ) *
      ∑' (m : ℕ+),
        (1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ)))
have hf : Summable (α := ℂ) fun (m : ℕ+) ↦
  1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))
Tactic: rw [← Summable.tsum_mul_left]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
d : ℕ+
⊢ Summable (α := ℂ) fun (m : ℕ+) ↦
    1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))
have this : Summable (α := ℂ) fun (n : ℕ) ↦ cotTerm (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ)) n
Tactic: have := summable_cotTerm (by simpa using z.int_div_mem_integerComplement (n := -d) (by aesop))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
d : ℕ+
this : Summable (α := ℂ) fun (n : ℕ) ↦ cotTerm (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ)) n
⊢ Summable (α := ℂ) fun (m : ℕ+) ↦
    1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))
have hf : ∀
  (this :
    Summable (α := ℂ) fun (n : ℕ) ↦
      (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ +
        (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹),
  Summable (α := ℂ) fun (m : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))⁻¹
Tactic: simp only [cotTerm, one_div] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
d : ℕ+
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ +
      (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹
⊢ Summable (α := ℂ) fun (m : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))⁻¹
have this₁ : Summable (α := ℂ) fun (n : ℕ) ↦
  (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(n + 1) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(n + 1) : ℂ))⁻¹
Tactic: simp only [← Nat.cast_add_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
d : ℕ+
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(n + 1) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(n + 1) : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (m : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))⁻¹
have this₁ : Summable (α := ℂ) fun (n : ℕ) ↦ (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑n : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑n : ℂ))⁻¹
Tactic: rw [summable_nat_add_iff (f := fun n ↦ (-d / (z : ℂ) - n)⁻¹ + (-d / (z : ℂ) + n)⁻¹)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
⊢ Tendsto (β := ℂ) (fun (N : ℕ+) ↦ ∑' (n : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑n : ℕ))
    atTop (𝓝 0)
have this : Tendsto (β := ℂ)
  (fun (m : ℕ+) ↦
    ∑' (n : ℕ+),
      cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑1 : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ)) ^ ((↑n : ℕ) * (↑m : ℕ)))
  atTop (𝓝 0)
Tactic: have := tendsto_zero_geometric_tsum_pnat (norm_exp_two_pi_I_lt_one ⟨_, im_pnat_div_pos 1 z⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
this :
  Tendsto (β := ℂ)
    (fun (m : ℕ+) ↦
      ∑' (n : ℕ+),
        cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑1 : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ ((↑n : ℕ) * (↑m : ℕ)))
    atTop (𝓝 0)
⊢ Tendsto (β := ℂ) (fun (N : ℕ+) ↦ ∑' (n : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑n : ℕ))
    atTop (𝓝 0)
have simp : ∀
  (this :
    Tendsto (β := ℂ)
      (fun (m : ℕ+) ↦
        ∑' (n : ℕ+),
          cexp (HMul.hMul (α := ℂ) (↑(↑n : ℕ) : ℂ) (↑(↑m : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * (-(↑1 : ℂ) / (↑z : ℂ)))))
      atTop (𝓝 0)),
  Tendsto (β := ℂ)
    (fun (N : ℕ+) ↦ ∑' (n : ℕ+), cexp ((↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))))) atTop
    (𝓝 0)
Tactic: simp only [← exp_nsmul, nsmul_eq_mul, Nat.cast_mul] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ Tendsto
    (fun (n : ℕ) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+), (1 / (-(↑n : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑n : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
have rw : Tendsto
  (fun (x : ℕ+) ↦
    2 / (↑z : ℂ) *
      ∑' (m : ℕ+),
        (1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
  atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
Tactic: rw [← PNat.tendsto_comp_val_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (goal)
Goal:
z : ℍ
⊢ 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 : ℕ) : ℂ)
have h : ∀ (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 : ℕ) : ℂ)
Tactic: ext N
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable (hypothesis)
Goal:
z : ℍ
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 h2 : (↑π : ℂ) * ((↑π : ℂ) * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ)).cot =
  1 / (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ) +
    ∑' (n : ℕ+),
      (1 / ((↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ) - (↑(↑n : ℕ) : ℂ)) +
        1 / ((↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := sorry : ℍ } : ℂ) + (↑(↑n : ℕ) : ℂ)))
Tactic: have h2 := cot_series_rep <| coe_mem_integerComplement ⟨-N / z, im_pnat_div_pos N z⟩