awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ) : ℂ)
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))
⊢ 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:
nth_rw 2 [show -2 * π * I / z = (-2 * π * I / z) - (2 / z * (2 * π * I)) * 0 + 2 * 0 by ring]
-- 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 : ℕ) : ℂ)
⊢ 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:
aux_tendsto_tsum_cexp_pnat z |>.const_mul _ |>.const_sub _ |>.add (.const_mul _ ?_)

Premises used: _private.0.EisensteinSeries.aux_tendsto_tsum_cexp_pnat, Filter.Tendsto.const_sub, Filter.Tendsto.const_mul, Filter.Tendsto.add
-- 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 : ℕ) : ℂ)
refine : Tendsto (β := ℂ) (fun (n : ℕ+) ↦ (↑(↑n : ℕ) : ℂ)⁻¹) atTop (𝓝 0)
⊢ 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:
refine aux_tendsto_tsum_cexp_pnat z |>.const_mul _ |>.const_sub _ |>.add (.const_mul _ ?_)

Premises used: _private.0.EisensteinSeries.aux_tendsto_tsum_cexp_pnat, Filter.Tendsto.const_sub, Filter.Tendsto.const_mul, Filter.Tendsto.add
-- 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 : ℕ) : ℂ)
⊢ Tendsto (β := ℂ) (fun (n : ℕ+) ↦ (↑(↑n : ℕ) : ℂ)⁻¹) atTop (𝓝 0)

Tactic:
PNat.tendsto_comp_val_iff.mpr tendsto_inv_atTop_nhds_zero_nat

Premises used: Iff.mpr, PNat.tendsto_comp_val_iff, tendsto_inv_atTop_nhds_zero_nat
-- 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 : ℕ) : ℂ)
⊢ Tendsto (β := ℂ) (fun (n : ℕ+) ↦ (↑(↑n : ℕ) : ℂ)⁻¹) atTop (𝓝 0)

Tactic:
exact PNat.tendsto_comp_val_iff.mpr tendsto_inv_atTop_nhds_zero_nat

Premises used: Iff.mpr, PNat.tendsto_comp_val_iff, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ+
rw :
  ∀ (i : ℤ) (hi : Membership.mem (γ := Finset ℤ) (Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ)) i),
    Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ) + 1)
⊢ 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:
rw [Summable.tsum_finsetSum (fun i hi ↦ ?_)]

Premises used: Summable.tsum_finsetSum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ+
i : ℤ
hi : Membership.mem (γ := Finset ℤ) (Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ)) i
apply :
  ∀ (b : ℤ),
    1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑(i + 1) : ℂ)) =
      1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ) + 1)
⊢ Summable (α := ℂ) fun (m : ℤ) ↦ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑i : ℂ) + 1)

Tactic:
apply (summable_left_one_div_linear_sub_one_div_linear z i (i + 1)).congr

Premises used: EisensteinSeries.summable_left_one_div_linear_sub_one_div_linear, HAdd.hAdd, Summable.congr, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N : ℕ+
i : ℤ
hi : Membership.mem (γ := Finset ℤ) (Ico (-(↑(↑N : ℕ) : ℤ)) (↑(↑N : ℕ) : ℤ)) i
⊢ ∀ (b : ℤ),
    1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑(i + 1) : ℂ)) =
      1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ)) - 1 / ((↑b : ℂ) * (↑z : ℂ) + (↑i : ℂ) + 1)

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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)))

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
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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)))
⊢ ∀ (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

Premises used: _private.0.EisensteinSeries.telescope_aux, _private.0.EisensteinSeries.aux_tsum_identity_1
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ) : ℂ)))
⊢ -2 * (↑π : ℂ) * I / (↑z : ℂ) = 0 + -2 * (↑π : ℂ) * I / (↑z : ℂ)

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

Tactic:
rw [funext this, show -2 * π * I / z = 0 + -2 * π * I / z by ring]

Premises used: funext
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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)
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 : ℂ)))
⊢ 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:
apply Tendsto.add

Premises used: Filter.Tendsto.add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ) : ℂ)) atTop (𝓝 0)

Tactic:
simpa [← PNat.tendsto_comp_val_iff] using
      (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℂ)).const_mul (-2)

Premises used: PNat.tendsto_comp_val_iff, Filter.Tendsto.const_mul, OfNat.ofNat, Neg.neg, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
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 : ℕ+) ↦
      ∑' (m : ℕ+),
        (1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) - (↑(↑x : ℕ) : ℂ)) + 1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + -(↑(↑x : ℕ) : ℂ)) -
            1 / ((↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ)) -
          1 / (-(↑(↑m : ℕ) : ℂ) * (↑z : ℂ) + (↑(↑x : ℕ) : ℂ))))
    atTop (𝓝 (-2 * (↑π : ℂ) * I / (↑z : ℂ)))

Tactic:
simpa only [aux_tsum_identity_2, ← PNat.tendsto_comp_val_iff] using aux_tendsto_tsum z

Premises used: PNat.tendsto_comp_val_iff, _private.0.EisensteinSeries.aux_tsum_identity_2, _private.0.EisensteinSeries.aux_tendsto_tsum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
ha :
  HasSum (fun (b : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)))
    (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)
⊢ ∑'[symmetricIco ℤ] (n : ℤ),
      ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)) =
    -2 * (↑π : ℂ) * I / (↑z : ℂ)

Tactic:
apply HasSum.tsum_eq

Premises used: HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ HasSum (fun (b : ℤ) ↦ ∑' (m : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) + 1)))
    (-2 * (↑π : ℂ) * I / (↑z : ℂ)) (symmetricIco ℤ)

Tactic:
simpa [HasSum, ← Nat.map_cast_int_atTop, ← PNat.tendsto_comp_val_iff]
    using tendsto_tsum_one_div_linear_sub_succ_eq z

Premises used: PNat.tendsto_comp_val_iff, HasSum, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, Nat.map_cast_int_atTop, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ Eq (α := ℂ) (∑' (x : ℤ), 0) 0

Tactic:
tsum_zero

Premises used: tsum_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
h :
  ∀ (x : ℤ),
    Eq (α := ℂ)
      (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))) 0
⊢ Eq (α := ℂ)
    (∑' (m : ℤ),
      ∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1)))
    0

Tactic:
convert! tsum_zero

Premises used: tsum_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
x : ℤ
⊢ Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))) 0

Tactic:
tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z _

Premises used: EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
x : ℤ
⊢ Eq (α := ℂ)
    (∑'[symmetricIco ℤ] (n : ℤ), (1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ)) - 1 / ((↑x : ℂ) * (↑z : ℂ) + (↑n : ℂ) + 1))) 0

Tactic:
exact tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z _

Premises used: EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
⊢ δ ![0, 0] = 1

Tactic:
simp [δ]

Premises used: _private.0.EisensteinSeries.δ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
⊢ δ ![0, -1] = 2

Tactic:
simp [δ]

Premises used: _private.0.EisensteinSeries.δ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
h : ∀ (x : Fin 2 → ℤ) (hx : x ≠ ![0, 0]) (hx' : x ≠ ![0, -1]), δ x = 0 x
⊢ δ =ᶠ[cofinite] 0

Tactic:
filter_upwards [eventually_cofinite_ne ![0, 0], eventually_cofinite_ne ![0, -1]] with x hx hx'

Premises used: Filter.eventually_cofinite_ne, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
x : Fin 2 → ℤ
hx : x ≠ ![0, 0]
hx' : x ≠ ![0, -1]
⊢ δ x = 0 x

Tactic:
simp_all [δ]

Premises used: _private.0.EisensteinSeries.δ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
simp_rw :
  Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦
    (HPow.hPow (β := ℕ) ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ)) 2 * ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + 1))⁻¹
⊢ Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦ G2Term z m - δ m

Tactic:
simp_rw [G2Term, add_sub_cancel_right]

Premises used: _private.0.EisensteinSeries.G2Term, add_sub_cancel_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
linarith : LE.le (α := ℝ) 3 2 → -1 + HSub.hSub (α := ℝ) 3 2 = 0
⊢ LT.lt (α := ℝ) 2 3

Tactic:
linarith
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
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)⁻¹
⊢ Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦
    (HPow.hPow (β := ℕ) ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ)) 2 * ((↑(m 0) : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + 1))⁻¹

Tactic:
apply summable_of_isBigO_rpow_norm (a := 3) (by linarith)

Premises used: EisensteinSeries.summable_of_isBigO_rpow_norm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ 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:
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)

Premises used: pow_two, mul_assoc, pow_three, Asymptotics.IsBigO.mul, EisensteinSeries.isBigO_linear_add_const_vec, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ 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)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
H : Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦ G2Term z m - δ m
⊢ ∀ (x : Fin 2 → ℤ), δ x = 0 x → (fun (m : Fin 2 → ℤ) ↦ G2Term z m - δ m) x = G2Term z x

Tactic:
simp +contextual
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
H : Summable (α := ℂ) fun (m : Fin 2 → ℤ) ↦ G2Term z m - δ m
⊢ Summable (G2Term z)

Tactic:
exact H.congr_cofinite <| δ_eventually_cofinite.mp <| .of_forall <| by simp +contextual

Premises used: _private.0.EisensteinSeries.δ_eventually_cofinite, Summable.congr_cofinite, Filter.Eventually.mp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
⊢ Summable (α := ℂ) fun (p : ℤ × ℤ) ↦ G2Term z ![p.1, p.2]

Tactic:
apply (finTwoArrowEquiv _).symm.summable_iff.mpr (G2Term_summable z)

Premises used: Iff.mpr, Equiv.summable_iff, _private.0.EisensteinSeries.G2Term_summable, Equiv.symm, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)⁻¹
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)⁻¹
⊢ ((↑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
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)⁻¹

Tactic:
simp [h.1, h.2]

Premises used: And.right, And.left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
z : ℍ
b n : ℤ
h : ¬(b = 0 ∧ n = 0)
⊢ b = 0 → ¬n = 0

Tactic:
simp only [not_and] at h

Premises used: not_and
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)⁻¹
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)⁻¹
⊢ ((↑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