mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ 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))

pp: z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)

Tactic:
]

Goal state after:
z : ℍ
d : ℕ+
⊢ 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))

z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∑' (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)⁻¹)

pp: case hf
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d + ↑↑n * ↑z)⁻¹ - (↑↑d + ↑↑n * ↑z)⁻¹

pp: case hg
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d - ↑z * ↑↑n)⁻¹ - (↑↑d - ↑z * ↑↑n)⁻¹

Tactic:
]

Goal state after:
z : ℍ
d : ℕ+
⊢ ∑' (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)⁻¹)

case hf
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d + ↑↑n * ↑z)⁻¹ - (↑↑d + ↑↑n * ↑z)⁻¹

case hg
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d - ↑z * ↑↑n)⁻¹ - (↑↑d - ↑z * ↑↑n)⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ ↑{ coe := (-↑I)⁻¹, coe_im_pos := ⋯ } = ↑I

Tactic:
]

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ ↑{ coe := (-↑I)⁻¹, coe_im_pos := ⋯ } = ↑I
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (c : ℤ), eisSummand ↑k ![(0, c).1, (0, c).2] z +
      ↑2 * ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n)

Tactic:
]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (c : ℤ), eisSummand ↑k ![(0, c).1, (0, c).2] z +
      ↑2 * ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
h : ↑((k - 12) / 12) + 1 < (qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm h0))).order + 1
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ ↑((k - 12) / 12) < (qExpansion 1 ⇑(mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯)).order

Tactic:
]

Goal state after:
case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
h : ↑((k - 12) / 12) + 1 < (qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm h0))).order + 1
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ ↑((k - 12) / 12) < (qExpansion 1 ⇑(mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯)).order
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ ¬((-↑ρ)⁻¹.re = (↑ρ).re ∧ (-↑ρ)⁻¹.im = (↑ρ).im)

Tactic:
]

Goal state after:
g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ ¬((-↑ρ)⁻¹.re = (↑ρ).re ∧ (-↑ρ)⁻¹.im = (↑ρ).im)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∑' (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))

pp: case hf
z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m)

Tactic:
]

Goal state after:
z : ℍ
d : ℕ+
⊢ ∑' (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))

case hf
z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ ¬↑1 + ↑ρ = ↑ρ

Tactic:
]

Goal state after:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ ¬↑1 + ↑ρ = ↑ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case hf
z : ℍ
d : ℕ+
this : Summable fun n ↦ (-↑↑d / ↑z - ↑n)⁻¹ + (-↑↑d / ↑z + ↑n)⁻¹
⊢ Summable fun m ↦ (-↑↑d / ↑z - ↑↑m)⁻¹ + (-↑↑d / ↑z + ↑↑m)⁻¹

Tactic:
]

Goal state after:
case hf
z : ℍ
d : ℕ+
this : Summable fun n ↦ (-↑↑d / ↑z - ↑n)⁻¹ + (-↑↑d / ↑z + ↑n)⁻¹
⊢ Summable fun m ↦ (-↑↑d / ↑z - ↑↑m)⁻¹ + (-↑↑d / ↑z + ↑↑m)⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
⊢ ¬T • ρ = ρ

Tactic:
]

Goal state after:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
this : T • ρ ≠ ρ
⊢ ¬T • ρ = ρ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
⊢ ¬-I * ↑τ = 0 ∨ ¬1 / 2 ≠ 0

Tactic:
]

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ ¬-I * ↑τ = 0 ∨ ¬1 / 2 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun x ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑x / ↑z - ↑↑m) + 1 / (-↑↑x / ↑z + ↑↑m))) atTop (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
]

Goal state after:
z : ℍ
⊢ Tendsto (fun x ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑x / ↑z - ↑↑m) + 1 / (-↑↑x / ↑z + ↑↑m))) atTop (𝓝 (-2 * ↑π * I / ↑z))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
let y := rexp (-π * τ.im)

Goal state after:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ rexp (↑π * I * ↑n ^ 2 * τ).re = y ^ n ^ 2

Tactic:
]

Goal state after:
case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ rexp (↑π * I * ↑n ^ 2 * τ).re = y ^ n ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ π * ↑n ^ 2 * -τ.im = -π * τ.im * ↑n ^ 2

Tactic:
]

Goal state after:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ π * ↑n ^ 2 * -τ.im = -π * τ.im * ↑n ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ ↑ρ = ↑{ coe := (-↑(1 +ᵥ ρ))⁻¹, coe_im_pos := ⋯ }

Tactic:
]

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ ↑ρ = ↑{ coe := (-↑(1 +ᵥ ρ))⁻¹, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * I -
        2 * ↑π * I *
          (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 *
          (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 *
              (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) =
    2 / ↑↑N

Tactic:
]

Goal state after:
z : ℍ
N : ℕ+
h2 :
  ↑π * I -
        2 * ↑π * I *
          (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 *
          (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 *
              (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) =
    2 / ↑↑N
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℤ
z : ℍ
n : ℕ
v : ↑(gammaSet 1 n 0)
⊢ (↑((n • divIntMap ↑n ↑v) 0) * ↑z + ↑((n • divIntMap ↑n ↑v) 1)) ^ (-k) =
    (↑n ^ k)⁻¹ * (↑(divIntMap (↑n) (↑v) 0) * ↑z + ↑(divIntMap (↑n) (↑v) 1)) ^ (-k)

Tactic:
]

Goal state after:
k : ℤ
z : ℍ
n : ℕ
v : ↑(gammaSet 1 n 0)
⊢ (↑((n • divIntMap ↑n ↑v) 0) * ↑z + ↑((n • divIntMap ↑n ↑v) 1)) ^ (-k) =
    (↑n ^ k)⁻¹ * (↑(divIntMap (↑n) (↑v) 0) * ↑z + ↑(divIntMap (↑n) (↑v) 1)) ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
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
⊢ Tendsto
    (fun n ↦ -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n)
    atTop (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
]

Goal state after:
z : ℍ
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
⊢ Tendsto
    (fun n ↦ -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n)
    atTop (𝓝 (-2 * ↑π * I / ↑z))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (-π * τ.im) ^ n ^ 2 = y ^ n ^ 2

Tactic:
hm,

Goal state after:
case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (-π * τ.im) ^ ↑m = y ^ ↑m
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (-π * τ.im) ^ m = rexp (-π * τ.im) ^ m

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑⟨b, c⟩.snd) z =
    ∑' (z_1 : ℕ × { x // x ∈ gammaSet 1 1 0 }), 1 / ↑z_1.1 ^ k * eisSummand (↑k) (↑z_1.2) z

pp: case hsumm
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun c ↦ eisSummand (↑k) (↑c.snd) z

Tactic:
]

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑⟨b, c⟩.snd) z =
    ∑' (z_1 : ℕ × { x // x ∈ gammaSet 1 1 0 }), 1 / ↑z_1.1 ^ k * eisSummand (↑k) (↑z_1.2) z

case hsumm
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun c ↦ eisSummand (↑k) (↑c.snd) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
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
⊢ Tendsto
    (fun n ↦ -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n)
    atTop (𝓝 (-2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * 0 + 2 * 0))

Tactic:
]

Goal state after:
z : ℍ
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
⊢ Tendsto
    (fun n ↦ -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n)
    atTop (𝓝 (-2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * 0 + 2 * 0))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ n ^ 2 = n ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (b : ℕ) (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

pp: case h₁
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun z_1 ↦ (↑z_1.1 ^ k)⁻¹ * eisSummand (↑k) (↑z_1.2) z

pp: case h₂
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
⊢ Summable fun c ↦ (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

Tactic:
]

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (b : ℕ) (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

case h₁
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun z_1 ↦ (↑z_1.1 ^ k)⁻¹ * eisSummand (↑k) (↑z_1.2) z

case h₂
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
⊢ Summable fun c ↦ (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: case refine_2
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : n ^ 2 = ↑(n.natAbs ^ 2)
⊢ y ^ n.natAbs ^ 2 ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
]

Goal state after:
case refine_2
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : n ^ 2 = ↑(n.natAbs ^ 2)
⊢ y ^ n.natAbs ^ 2 ≤ rexp (-π * τ.im) ^ n.natAbs
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
⊢ ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
    ∑ i ∈ Ico (-↑↑N) ↑↑N, ∑' (b : ℤ), (1 / (↑b * ↑z + ↑i) - 1 / (↑b * ↑z + ↑i + 1))

pp: z : ℍ
N : ℕ+
i : ℤ
hi : i ∈ Ico (-↑↑N) ↑↑N
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑i) - 1 / (↑m * ↑z + ↑i + 1)

Tactic:
]

Goal state after:
z : ℍ
N : ℕ+
i : ℤ
hi : i ∈ Ico (-↑↑N) ↑↑N
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑i) - 1 / (↑m * ↑z + ↑i + 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ IsOpen 𝒟ᵒ

Tactic:
by
  refine .inter (.preimage (by fun_prop) isOpen_Ioi) ?_
  exact isOpen_lt (f := fun z : ℍ ↦ |z.re|) (by fun_prop) continuous_const

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
      -(2 / ↑↑N) +
        ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑N) + 1 / (-↑↑m * ↑z + -↑↑N) - 1 / (↑↑m * ↑z + ↑↑N) - 1 / (-↑↑m * ↑z + ↑↑N))
⊢ Tendsto
    (fun x ↦
      -(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:
]

Goal state after:
z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
      -(2 / ↑↑N) +
        ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑N) + 1 / (-↑↑m * ↑z + -↑↑N) - 1 / (↑↑m * ↑z + ↑↑N) - 1 / (-↑↑m * ↑z + ↑↑N))
⊢ Tendsto
    (fun x ↦
      -(2 / ↑↑x) +
        ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑x) + 1 / (-↑↑m * ↑z + -↑↑x) - 1 / (↑↑m * ↑z + ↑↑x) - 1 / (-↑↑m * ↑z + ↑↑x)))
    atTop (𝓝 (0 + -2 * ↑π * I / ↑z))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ IsClosed {z | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
]

Goal state after:
⊢ IsClosed {z | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑↑n ^ 2 * τ) + cexp (↑π * I * ↑(-↑n) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
← hasSum_nat_add_iff' 1

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ) -
      ∑ i ∈ Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * τ) + cexp (↑π * I * ↑(-↑i) ^ 2 * τ)))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ) -
      ∑ i ∈ Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * τ) + cexp (↑π * I * ↑(-↑i) ^ 2 * τ)))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
]

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this :
  HasSum (fun n ↦ cexp (↑π * I * ↑↑(n + 1) ^ 2 * τ) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * τ))
    (jacobiTheta τ + cexp (↑π * I * ↑0 ^ 2 * τ) -
      ∑ i ∈ Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * τ) + cexp (↑π * I * ↑(-↑i) ^ 2 * τ)))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (1 / 2) • ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (1 / 2) • ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
a : ℝ
ha : 0 < a
ha' : a ∈ Set.Iio 1
⊢ |(↑{ coe := ↑a * ↑x, coe_im_pos := ⋯ }).re| < 1 / 2

Tactic:
]

Goal state after:
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
a : ℝ
ha : 0 < a
ha' : a ∈ Set.Iio 1
⊢ |(↑{ coe := ↑a * ↑x, coe_im_pos := ⋯ }).re| < 1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun x_1 ↦ ↑(↑ofComplex (↑x_1 * ↑x))) (𝓝 1) (𝓝 ↑x)

Tactic:
]

Goal state after:
case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun x_1 ↦ ↑(↑ofComplex (↑x_1 * ↑x))) (𝓝 1) (𝓝 ↑x)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 (↑1 * ↑x))

Tactic:
]

Goal state after:
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 (↑1 * ↑x))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun t ↦ ↑t * ↑x) (𝓝 1) (𝓝 ↑x)
a : ℝ
ha : 0 < a
⊢ ↑a * ↑x = ↑{ coe := ↑a * ↑x, coe_im_pos := ⋯ }

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta τ = jacobiTheta τ

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure (closure 𝒟ᵒ)

Tactic:
]

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure (closure 𝒟ᵒ)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        ((-2) ^ (2 * (m + 1)) * ↑π ^ (2 * (m + 1)) * (-1) ^ (m + 1)) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))

Tactic:
]

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        ((-2) ^ (2 * (m + 1)) * ↑π ^ (2 * (m + 1)) * (-1) ^ (m + 1)) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ = 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < ‖↑x‖ ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im
⊢ 1 < normSq ↑{ coe := ↑x + ↑↑a * Complex.I, coe_im_pos := ⋯ }

Tactic:
]

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < ‖↑x‖ ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im
⊢ 1 < normSq ↑{ coe := ↑x + ↑↑a * Complex.I, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2 = rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) * 2

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n =
    1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ 0 < ↑a ^ 2 + 2 * ↑a * x.im

Tactic:
]

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ 0 < ↑a ^ 2 + 2 * ↑a * x.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hx : 1 ≤ normSq ↑x
hx' : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ

Tactic:
one_le_normSq_iff

Goal state after:
x : ℍ
hx : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hx : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ

Tactic:
]

Goal state after:
x : ℍ
hx : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ