awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
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 : ℕ) : ℂ))⁻¹)
⊢ 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:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℂ))⁻¹
hg :
  Summable (α := ℂ) fun (n : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹
⊢ 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:
rw [← Summable.tsum_add]

Premises used: Summable.tsum_add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ 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:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
hf :
  ∀ (b : ℕ+),
    1 / ((↑(↑(↑b : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(-(↑(↑d : ℕ) : ℤ)) : ℂ)) -
        1 / ((↑(↑(↑b : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(↑(↑d : ℕ) : ℤ) : ℂ)) =
      (-(↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (n : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑n : ℕ) : ℂ) * (↑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

Premises used: PNat.val, Iff.mpr, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, summable_int_iff_summable_nat_and_neg, Nat.cast, And.left, Iff.mp, Summable.congr, Neg.neg, summable_pnat_iff_summable_nat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ ∀ (b : ℕ+),
    1 / ((↑(↑(↑b : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(-(↑(↑d : ℕ) : ℤ)) : ℂ)) -
        1 / ((↑(↑(↑b : ℕ) : ℤ) : ℂ) * (↑z : ℂ) + (↑(↑(↑d : ℕ) : ℤ) : ℂ)) =
      (-(↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) + (↑(↑b : ℕ) : ℂ) * (↑z : ℂ))⁻¹

Tactic:
grind [Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
hg :
  ∀ (b : ℕ+),
    1 / ((↑(-(↑(↑b : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(-(↑(↑d : ℕ) : ℤ)) : ℂ)) -
        1 / ((↑(-(↑(↑b : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(↑(↑d : ℕ) : ℤ) : ℂ)) =
      (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (n : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑n : ℕ) : ℂ))⁻¹

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

Premises used: PNat.val, Iff.mpr, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, summable_int_iff_summable_nat_and_neg, Nat.cast, And.right, Iff.mp, Summable.congr, Neg.neg, summable_pnat_iff_summable_nat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ ∀ (b : ℕ+),
    1 / ((↑(-(↑(↑b : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(-(↑(↑d : ℕ) : ℤ)) : ℂ)) -
        1 / ((↑(-(↑(↑b : ℕ) : ℤ)) : ℂ) * (↑z : ℂ) + (↑(↑(↑d : ℕ) : ℤ) : ℂ)) =
      (-(↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹ - ((↑(↑d : ℕ) : ℂ) - (↑z : ℂ) * (↑(↑b : ℕ) : ℂ))⁻¹

Tactic:
grind [Int.cast_neg, Int.cast_natCast, neg_mul, one_div]

Premises used: Int.cast_neg, Int.cast_natCast, one_div, neg_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ Summable (α := ℂ) fun (m : ℤ) ↦
    1 / ((↑m : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ))

Tactic:
simpa using summable_left_one_div_linear_sub_one_div_linear z (-d) d

Premises used: PNat.val, EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, Nat.cast, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ) : ℂ))))
hf :
  Summable (α := ℂ) fun (m : ℕ+) ↦
    1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))
⊢ ∑' (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 : ℕ) : ℂ)))

Tactic:
rw [← Summable.tsum_mul_left]

Premises used: Summable.tsum_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ ∀ (b : ℕ+),
    1 / ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑d : ℕ) : ℂ)) + 1 / (-(↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑d : ℕ) : ℂ)) -
          1 / ((↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) -
        1 / (-(↑(↑b : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑d : ℕ) : ℂ)) =
      2 / (↑z : ℂ) *
        (1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑b : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑b : ℕ) : ℂ)))

Tactic:
grind [sub_eq_add_neg, ← div_neg, ne_zero z]

Premises used: sub_eq_add_neg, UpperHalfPlane.ne_zero, div_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ 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:
apply tsum_congr (by grind [sub_eq_add_neg, ← div_neg, ne_zero z])

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ Ne (α := ℤ) (-(↑(↑d : ℕ) : ℤ)) 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ -(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) ∈ integerComplement

Tactic:
simpa using z.int_div_mem_integerComplement (n := -d) (by aesop)

Premises used: UpperHalfPlane.int_div_mem_integerComplement
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ cotTerm (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ)) n

Tactic:
have := summable_cotTerm (by simpa using z.int_div_mem_integerComplement (n := -d) (by aesop))
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
this : Summable (α := ℂ) fun (n : ℕ) ↦ cotTerm (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ)) n
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 : ℕ) : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (m : ℕ+) ↦
    1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))

Tactic:
simp only [cotTerm, one_div] at *

Premises used: one_div, cotTerm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ +
      (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹
⊢ Summable (α := ℂ) fun (n : ℕ) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(n + 1) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(n + 1) : ℂ))⁻¹

Tactic:
simp only [← Nat.cast_add_one] at this

Premises used: Nat.cast_add_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(n + 1) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(n + 1) : ℂ))⁻¹
⊢ 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

Premises used: summable_nat_add_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
d : ℕ+
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑n : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑n : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (m : ℕ+) ↦
    (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ))⁻¹ + (-(↑(↑d : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))⁻¹

Tactic:
apply this.subtype

Premises used: Summable.subtype
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ Tendsto (β := ℂ)
    (fun (m : ℕ+) ↦
      ∑' (n : ℕ+),
        cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑1 : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ ((↑n : ℕ) * (↑m : ℕ)))
    atTop (𝓝 0)

Tactic:
have := tendsto_zero_geometric_tsum_pnat (norm_exp_two_pi_I_lt_one ⟨_, im_pnat_div_pos 1 z⟩)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  Tendsto (β := ℂ)
    (fun (m : ℕ+) ↦
      ∑' (n : ℕ+),
        cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑1 : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ ((↑n : ℕ) * (↑m : ℕ)))
    atTop (𝓝 0)
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)
⊢ Tendsto (β := ℂ) (fun (N : ℕ+) ↦ ∑' (n : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑n : ℕ))
    atTop (𝓝 0)

Tactic:
simp only [← exp_nsmul, nsmul_eq_mul, Nat.cast_mul] at *

Premises used: Complex.exp_nsmul, Nat.cast_mul, nsmul_eq_mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  Tendsto (β := ℂ)
    (fun (m : ℕ+) ↦
      ∑' (n : ℕ+),
        cexp (HMul.hMul (α := ℂ) (↑(↑n : ℕ) : ℂ) (↑(↑m : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * (-(↑1 : ℂ) / (↑z : ℂ)))))
    atTop (𝓝 0)
⊢ ∀ (x : ℕ+),
    Eq (α := ℂ)
      (∑' (n : ℕ+),
        cexp (HMul.hMul (α := ℂ) (↑(↑n : ℕ) : ℂ) (↑(↑x : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * (-(↑1 : ℂ) / (↑z : ℂ)))))
      (∑' (n : ℕ+), cexp ((↑(↑n : ℕ) : ℂ) * (2 * (↑π : ℂ) * I * (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ)))))

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
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:
exact this.congr <| by grind

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
rw :
  Tendsto
    (fun (x : ℕ+) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+),
          (1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))
⊢ Tendsto
    (fun (n : ℕ) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+), (1 / (-(↑n : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑n : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))

Tactic:
rw [← PNat.tendsto_comp_val_iff]

Premises used: PNat.tendsto_comp_val_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
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 : ℕ) : ℂ)
⊢ 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:
ext N
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ+
⊢ (↑π : ℂ) * ((↑π : ℂ) * (↑{ 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 : ℕ) : ℂ)))

Tactic:
have h2 := cot_series_rep <| coe_mem_integerComplement ⟨-N / z, im_pnat_div_pos N z⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ+
h2 :
  (↑π : ℂ) * I -
        2 * (↑π : ℂ) * I *
          ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ n -
      (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ) =
    (↑π : ℂ) * I -
        2 * (↑π : ℂ) * I *
          ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ n -
      (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ)
⊢ Summable (HPow.hPow (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ))))

Tactic:
simpa using norm_exp_two_pi_I_lt_one ⟨-N / z, im_pnat_div_pos N z⟩

Premises used: PNat.val, UpperHalfPlane.coe, UpperHalfPlane.norm_exp_two_pi_I_lt_one, UpperHalfPlane.mk, HDiv.hDiv, Nat.cast, UpperHalfPlane.im_pnat_div_pos, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ) : ℂ)))
h :
  ∀
    (h2 :
      (↑π : ℂ) * I -
            2 * (↑π : ℂ) * I *
              (HPow.hPow (β := ℕ)
                  (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ))) 0 +
                ∑' (n : ℕ+),
                  cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^
                    (↑n : ℕ)) -
          (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ) =
        (↑π : ℂ) * I -
            2 * (↑π : ℂ) * I *
              (HPow.hPow (β := ℕ)
                  (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ))) 0 +
                ∑' (n : ℕ+),
                  cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^
                    (↑n : ℕ)) -
          (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ)),
    2 / (↑z : ℂ) *
          ((↑π : ℂ) * I -
              2 * (↑π : ℂ) * I *
                (HPow.hPow (β := ℕ)
                    (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ))) 0 +
                  ∑' (n : ℕ+),
                    cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^
                      (↑n : ℕ)) -
            (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ)) -
        (-(2 * (↑π : ℂ)) * I / (↑z : ℂ) -
          2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
            ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ)) =
      HDiv.hDiv (α := ℂ) 2 (↑(↑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:
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 *

Premises used: tsum_zero_pnat_eq_tsum_nat, one_div, inv_div, neg_mul, sub_eq_iff_eq_add', pi_mul_cot_pi_q_exp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ+
h2 :
  (↑π : ℂ) * I -
        2 * (↑π : ℂ) * I *
          (HPow.hPow (β := ℕ)
              (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ))) 0 +
            ∑' (n : ℕ+),
              cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ (↑n : ℕ)) -
      (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ) =
    (↑π : ℂ) * I -
        2 * (↑π : ℂ) * I *
          (HPow.hPow (β := ℕ)
              (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ))) 0 +
            ∑' (n : ℕ+),
              cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^ (↑n : ℕ)) -
      (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ)
⊢ 2 / (↑z : ℂ) *
        ((↑π : ℂ) * I -
            2 * (↑π : ℂ) * I *
              (HPow.hPow (β := ℕ)
                  (cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ))) 0 +
                ∑' (n : ℕ+),
                  cexp (2 * (↑π : ℂ) * I * (↑{ coe := -(↑(↑N : ℕ) : ℂ) / (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^
                    (↑n : ℕ)) -
          (↑z : ℂ) / -(↑(↑N : ℕ) : ℂ)) -
      (-(2 * (↑π : ℂ)) * I / (↑z : ℂ) -
        2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) *
          ∑' (m : ℕ+), cexp (2 * (↑π : ℂ) * I * (-(↑(↑N : ℕ) : ℂ) / (↑z : ℂ))) ^ (↑m : ℕ)) =
    HDiv.hDiv (α := ℂ) 2 (↑(↑N : ℕ) : ℂ)

Tactic:
field [ne_zero z]

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ) : ℂ)

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]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ) : ℂ)
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 : ℂ)))
⊢ Tendsto
    (fun (x : ℕ+) ↦
      2 / (↑z : ℂ) *
        ∑' (m : ℕ+),
          (1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) - (↑(↑m : ℕ) : ℂ)) + 1 / (-(↑(↑x : ℕ) : ℂ) / (↑z : ℂ) + (↑(↑m : ℕ) : ℂ))))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))

Tactic:
rw [H0]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ) : ℂ)
⊢ -2 * (↑π : ℂ) * I / (↑z : ℂ) =
    -2 * (↑π : ℂ) * I / (↑z : ℂ) - 2 / (↑z : ℂ) * (2 * (↑π : ℂ) * I) * 0 + HMul.hMul (α := ℂ) 2 0

Tactic:
ring