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))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S, -S} → g • I = I

Tactic:
·

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S, -S} → g • I = I
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)⁻¹)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
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:
case hf
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d + ↑↑n * ↑z)⁻¹ - (↑↑d + ↑↑n * ↑z)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

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

Tactic:
·

Goal state after:
case hg
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d - ↑z * ↑↑n)⁻¹ - (↑↑d - ↑z * ↑↑n)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

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

Tactic:
·

Goal state after:
z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
g : SL(2, ℤ)
⊢ g • ρ = ρ → g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

pp: case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ

Tactic:
·

Goal state after:
case mp
g : SL(2, ℤ)
⊢ g • ρ = ρ → g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_a
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 * riemannZeta ↑k

pp: case e_a.e_a
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
⊢ ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
·

Goal state after:
case e_a
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 * riemannZeta ↑k
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inl
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : k < 0
⊢ f = 0

pp: case inr
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : 0 ≤ k
⊢ f = 0

Tactic:
·

Goal state after:
case inl
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : k < 0
⊢ f = 0
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))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : 0 ≤ k
⊢ f = 0

Tactic:
·

Goal state after:
case inr
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : 0 ≤ k
⊢ f = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_a.e_a
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
⊢ ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
·

Goal state after:
case e_a.e_a
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
⊢ ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

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

Tactic:
·

Goal state after:
case hf
z : ℍ
d : ℕ+
⊢ Summable fun m ↦ 1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

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

Tactic:
·

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

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ

Tactic:
·

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

Tactic:
·

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

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

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case refine_1
⊢ IsClosed fun z ↦ Real.le✝ 0 z.im

pp: case refine_2
⊢ IsClosed fun z ↦ Real.le✝ 1 ‖z‖

pp: case refine_3
⊢ IsClosed fun z ↦ Real.le✝ |z.re| (1 / 2)

Tactic:
·

Goal state after:
case refine_1
⊢ IsClosed fun z ↦ Real.le✝ 0 z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case refine_2
⊢ IsClosed fun z ↦ Real.le✝ 1 ‖z‖

pp: case refine_3
⊢ IsClosed fun z ↦ Real.le✝ |z.re| (1 / 2)

Tactic:
·

Goal state after:
case refine_2
⊢ IsClosed fun z ↦ Real.le✝ 1 ‖z‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case refine_3
⊢ IsClosed fun z ↦ Real.le✝ |z.re| (1 / 2)

Tactic:
·

Goal state after:
case refine_3
⊢ IsClosed fun z ↦ Real.le✝ |z.re| (1 / 2)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case hf
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)) atTop (𝓝 0)

pp: case hg
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 ↦
      ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑x) + 1 / (-↑↑m * ↑z + -↑↑x) - 1 / (↑↑m * ↑z + ↑↑x) - 1 / (-↑↑m * ↑z + ↑↑x)))
    atTop (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
·

Goal state after:
case hf
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)) atTop (𝓝 0)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∃ᶠ (x_1 : ℝ) in 𝓝[<] 1, ↑ofComplex (↑x_1 * ↑x) ∈ 𝒟ᵒ

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

Tactic:
·

Goal state after:
case h
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∃ᶠ (x_1 : ℝ) in 𝓝[<] 1, ↑ofComplex (↑x_1 * ↑x) ∈ 𝒟ᵒ
Module: Mathlib.NumberTheory.Modular

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

pp: case h.refine_2
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |(↑ofComplex (↑x_1 * ↑x)).re| < 1 / 2

Tactic:
·

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

Goal state before:
pp: case hg
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 ↦
      ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑x) + 1 / (-↑↑m * ↑z + -↑↑x) - 1 / (↑↑m * ↑z + ↑↑x) - 1 / (-↑↑m * ↑z + ↑↑x)))
    atTop (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
·

Goal state after:
case hg
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 ↦
      ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑x) + 1 / (-↑↑m * ↑z + -↑↑x) - 1 / (↑↑m * ↑z + ↑↑x) - 1 / (-↑↑m * ↑z + ↑↑x)))
    atTop (𝓝 (-2 * ↑π * I / ↑z))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.refine_2
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |(↑ofComplex (↑x_1 * ↑x)).re| < 1 / 2

Tactic:
·

Goal state after:
case h.refine_2
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |(↑ofComplex (↑x_1 * ↑x)).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 t ↦ ↑ofComplex (↑t * ↑x)) (𝓝[<] 1) (𝓝 x)

Tactic:
·

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

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

Tactic:
add_sub_cancel_left

Goal state after:
τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta τ = jacobiTheta τ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ ∃ᶠ (x_1 : ℝ≥0) in 𝓝[>] 0, { coe := ↑x + ↑↑x_1 * Complex.I, coe_im_pos := ⋯ } ∈ closure 𝒟ᵒ

pp: case hf
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ { coe := ↑x + ↑↑t * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)

Tactic:
·

Goal state after:
case h
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ ∃ᶠ (x_1 : ℝ≥0) in 𝓝[>] 0, { coe := ↑x + ↑↑x_1 * Complex.I, coe_im_pos := ⋯ } ∈ closure 𝒟ᵒ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hf
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ { coe := ↑x + ↑↑t * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)

Tactic:
·

Goal state after:
case hf
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun t ↦ { coe := ↑x + ↑↑t * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)
Module: Mathlib.NumberTheory.Modular

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

pp: case inr
x : ℍ
hx✝ : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
hx : 1 = ‖↑x‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 1 < normSq ↑x

pp: case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ |x.re| < 1 / 2

Tactic:
·

Goal state after:
case left
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 1 < normSq ↑x
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ |x.re| < 1 / 2

Tactic:
·

Goal state after:
case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ |x.re| < 1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
y : ℝ
z : ℂ
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y → z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

pp: case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y

Tactic:
·

Goal state after:
case mp
y : ℝ
z : ℂ
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y → z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e'_5
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1)) = fun i ↦
    β * (↑((σ (k - 1)) (i + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (i + 1))

pp: case e'_6
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1) =
    ∑' (b : ℕ), β * (↑((σ (k - 1)) (b + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (b + 1))

Tactic:
·

Goal state after:
case e'_5
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1)) = fun i ↦
    β * (↑((σ (k - 1)) (i + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (i + 1))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y

Tactic:
·

Goal state after:
case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e'_6
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1) =
    ∑' (b : ℕ), β * (↑((σ (k - 1)) (b + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (b + 1))

Tactic:
·

Goal state after:
case e'_6
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1) =
    ∑' (b : ℕ), β * (↑((σ (k - 1)) (b + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (b + 1))
Module: Mathlib.NumberTheory.Modular

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

pp: case right
y : ℝ
⊢ Bornology.IsBounded {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
·

Goal state after:
case left
y : ℝ
⊢ IsClosed {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
y : ℝ
⊢ Bornology.IsBounded {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
·

Goal state after:
case right
y : ℝ
⊢ Bornology.IsBounded {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ √(z.re ^ 2 + z.im ^ 2) ^ 2 ≤ (1 / 2) ^ 2 + y ^ 2

Tactic:
Real.sq_sqrt (by positivity)

Goal state after:
case right
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.re ^ 2 + z.im ^ 2 ≤ (1 / 2) ^ 2 + y ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.re ^ 2 ≤ (1 / 2) ^ 2

pp: case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ^ 2 ≤ y ^ 2

Tactic:
·

Goal state after:
case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.re ^ 2 ≤ (1 / 2) ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ^ 2 ≤ y ^ 2

Tactic:
·

Goal state after:
case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ^ 2 ≤ y ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

pp: case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

Tactic:
·

Goal state after:
case inl
τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

Tactic:
·

Goal state after:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous

Goal state before:
pp: ⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ

Tactic:
let 𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
  have : ProperlyDiscontinuousSMul 𝒮ℒ' ℍ := inferInstance
  simp only [Subgroup.properlyDiscontinuousSMul_iff] at this ⊢
  refine fun K L hK hL ↦ ((this hK hL).map SpecialLinearGroup.toGL).subset fun g ↦ ?_
  rintro ⟨⟨γ, rfl⟩, hγ⟩
  exact ⟨γ, ⟨by simp [𝒮ℒ'], hγ⟩, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ∃ i ∈ Finset.univ, quotientFunc f i = 0
⊢ ⇑f = 0

pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ∏ q, quotientFunc f q = 0
⊢ ∀ i ∈ Finset.univ, MDiff (quotientFunc f i)

Tactic:
·

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ∃ i ∈ Finset.univ, quotientFunc f i = 0
⊢ ⇑f = 0