mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

Goal state after:
k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
a b : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
c : ℂ
a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
]

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ -(2 * ↑π * I * iteratedDerivWithin k (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z) =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z

pp: case hf
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ContDiffWithinAt ℂ (↑k) (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z

Tactic:
]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ -(2 * ↑π * I * iteratedDerivWithin k (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z) =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z

case hf
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ContDiffWithinAt ℂ (↑k) (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
z : ℍ
⊢ f z = f z

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hcusp : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ qExpansion 1 (⇑CuspForm.discriminant * ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))) =
    qExpansion 1 ⇑CuspForm.discriminant * qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))

Tactic:
]

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hcusp : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ qExpansion 1 (⇑CuspForm.discriminant * ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))) =
    qExpansion 1 ⇑CuspForm.discriminant * qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
this :
  ∑' (n : ℕ) (c : ℕ+), ↑↑c ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ((n + 1) * ↑c) =
    ∑' (e : ℕ+), ↑((σ 1) ↑e) * cexp (2 * ↑π * I * ↑z) ^ ↑e
⊢ -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
]

Goal state after:
z : ℍ
this :
  ∑' (n : ℕ) (c : ℕ+), ↑↑c ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ((n + 1) * ↑c) =
    ∑' (e : ℕ+), ↑((σ 1) ↑e) * cexp (2 * ↑π * I * ↑z) ^ ↑e
⊢ -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
this :
  Module.rank ℂ
      (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1
⊢ 1 + Module.rank ℂ ↥(cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1 + Module.rank ℂ ↥(cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h : E hk ∈ cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
hE : (PowerSeries.coeff 0) (qExpansion 1 ⇑(E hk)) = 1
⊢ False

Tactic:
]

Goal state after:
case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h : E hk ∈ cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
hE : (PowerSeries.coeff 0) (qExpansion 1 ⇑(E hk)) = 1
⊢ False
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
this :
  -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
⊢ Tendsto (fun N ↦ ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)) atTop
    (𝓝 (∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)))

Tactic:
]

Goal state after:
z : ℍ
this :
  -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
⊢ Tendsto (fun N ↦ ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)) atTop
    (𝓝 (∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
this :
  -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
⊢ Summable fun x ↦ ∑' (c : ℕ+), ↑↑c * cexp (2 * ↑π * I * ↑z) ^ (↑x * ↑c)

Tactic:
]

Goal state after:
z : ℍ
this :
  -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
⊢ Summable fun x ↦ ∑' (c : ℕ+), ↑↑c * cexp (2 * ↑π * I * ↑z) ^ (↑x * ↑c)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 = 0

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

Tactic:
]

Goal state after:
case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ HasSum (fun m ↦ (if m = 0 then 1 else -24 * ↑((σ 1) m)) • cexp (2 * ↑π * I * ↑z) ^ m) (E2 z)

Tactic:
← hasSum_nat_add_iff' 1

Goal state after:
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ HasSum (fun n ↦ (if n + 1 = 0 then 1 else -24 * ↑((σ 1) (n + 1))) • cexp (2 * ↑π * I * ↑z) ^ (n + 1))
    (E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ HasSum (fun n ↦ (if n + 1 = 0 then 1 else -24 * ↑((σ 1) (n + 1))) • cexp (2 * ↑π * I * ↑z) ^ (n + 1))
    (E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i)

Tactic:
]

Goal state after:
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ HasSum (fun n ↦ (if n + 1 = 0 then 1 else -24 * ↑((σ 1) (n + 1))) • cexp (2 * ↑π * I * ↑z) ^ (n + 1))
    (E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ ↑z =
    iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z

Tactic:
]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ ↑z =
    iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
⊢ qExpansion 1 ⇑(f.mul f) = qExpansion 1 ⇑(f.mul f)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 ⇑E₄ = qExpansion 1 ⇑f ^ 2
⊢ qExpansion 1 ⇑((f.mul f).mul f) = qExpansion 1 ⇑((f.mul f).mul f)

Tactic:
]

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

Goal state before:
pp: case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ 1 - 24 * ∑' (n : ℕ), ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1) -
      ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    -24 * ∑' (x : ℕ), ↑((σ 1) (x + 1)) * cexp (2 * ↑π * I * ↑z) ^ (x + 1)

Tactic:
]

Goal state after:
case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ 1 - 24 * ∑' (n : ℕ), ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1) -
      ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    -24 * ∑' (x : ℕ), ↑((σ 1) (x + 1)) * cexp (2 * ↑π * I * ↑z) ^ (x + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ (-2 * ↑π * I) ^ (k + 1) = (-(2 * ↑π * I)) ^ (k + 1)

Tactic:
]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ (-2 * ↑π * I) ^ (k + 1) = (-(2 * ↑π * I)) ^ (k + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z = ∑'[symmetricIcc ℤ] (b : ℤ), e2Summand b z

pp: z : ℍ
⊢ Tendsto (fun N ↦ -e2Summand (↑N) z) atTop (𝓝 0)

Tactic:
]

Goal state after:
z : ℍ
⊢ Tendsto (fun N ↦ -e2Summand (↑N) z) atTop (𝓝 0)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc : 0 ≤ ↑g 1 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

Tactic:
]

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc : 0 ≤ ↑g 1 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / (↑m * ↑z + ↑a) * (↑m * ↑z + ↑b - (↑m * ↑z + ↑a)) * (1 / (↑m * ↑z + ↑b)) =
    (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

pp: case ha
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑a ≠ 0

pp: case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0

Tactic:
]

Goal state after:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / (↑m * ↑z + ↑a) * (↑m * ↑z + ↑b - (↑m * ↑z + ↑a)) * (1 / (↑m * ↑z + ↑b)) =
    (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

case ha
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑a ≠ 0

case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)) =
    (-1) ^ (k + 1) * (2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)

Tactic:
]

Goal state after:
case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ ((-1) ^ k * ↑k !)⁻¹ * (-(2 * ↑π * I) ^ (k + 1) * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)) =
    (-1) ^ (k + 1) * (2 * ↑π * I) ^ (k + 1) / ↑k ! * (↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ 1 + 0 = ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
]

Goal state after:
case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ 1 + 0 = ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
a b : ℤ
this : Summable fun x ↦ (↑b - ↑a) * ((↑↑x * ↑z + ↑a) * (↑↑x * ↑z + ↑b))⁻¹
⊢ Summable fun x ↦ 1 / (↑↑x * ↑z + ↑a) - 1 / (↑↑x * ↑z + ↑b)

Tactic:
]

Goal state after:
z : ℍ
a b : ℤ
this : Summable fun x ↦ (↑b - ↑a) * ((↑↑x * ↑z + ↑a) * (↑↑x * ↑z + ↑b))⁻¹
⊢ Summable fun x ↦ 1 / (↑↑x * ↑z + ↑a) - 1 / (↑↑x * ↑z + ↑b)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
m : ℤ
this : Summable fun x ↦ ((↑m * ↑z + ↑↑x + 1) * (↑m * ↑z + ↑↑x))⁻¹
⊢ Summable fun x ↦ 1 / (↑m * ↑z + ↑↑x) - 1 / (↑m * ↑z + ↑↑x + 1)

Tactic:
]

Goal state after:
z : ℍ
m : ℤ
this : Summable fun x ↦ ((↑m * ↑z + ↑↑x + 1) * (↑m * ↑z + ↑↑x))⁻¹
⊢ Summable fun x ↦ 1 / (↑m * ↑z + ↑↑x) - 1 / (↑m * ↑z + ↑↑x + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

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

pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
]

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ (-2 * ↑π * I) ^ (k + 1) / ↑k ! *
      (↑0 ^ k * cexp (2 * ↑π * I * ↑z) ^ 0 + ∑' (n : ℕ+), ↑↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ ↑n) =
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * ∑' (n : ℕ+), ↑↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ ↑n

k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inr
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ 1 + ↑(if k - 12 ≡ 2 [MOD 12] then (k - 12) / 12 else (k - 12) / 12 + 1) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
]

Goal state after:
case h.inr.inr
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ 1 + ↑(if k - 12 ≡ 2 [MOD 12] then (k - 12) / 12 else (k - 12) / 12 + 1) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ
⊢ ∑ x ∈ Ico (-↑N) ↑N, (↑z ^ 2)⁻¹ * ∑' (n : ℤ), ((-(↑x * (↑z)⁻¹) + ↑n) ^ 2)⁻¹ =
    ∑ i ∈ Ico (-↑N) ↑N, ∑' (b : ℤ), ((↑b * ↑z + ↑i) ^ 2)⁻¹

Tactic:
]

Goal state after:
z : ℍ
N : ℕ
⊢ ∑ x ∈ Ico (-↑N) ↑N, (↑z ^ 2)⁻¹ * ∑' (n : ℤ), ((-(↑x * (↑z)⁻¹) + ↑n) ^ 2)⁻¹ =
    ∑ i ∈ Ico (-↑N) ↑N, ∑' (b : ℤ), ((↑b * ↑z + ↑i) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ
n : ℤ
hn : n ∈ Ico (-↑N) ↑N
⊢ ∑' (d : ℤ), (↑z ^ 2)⁻¹ * ((-(↑n * (↑z)⁻¹) + ↑(-d)) ^ 2)⁻¹ = ∑' (b : ℤ), ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
]

Goal state after:
z : ℍ
N : ℕ
n : ℤ
hn : n ∈ Ico (-↑N) ↑N
⊢ ∑' (d : ℤ), (↑z ^ 2)⁻¹ * ((-(↑n * (↑z)⁻¹) + ↑(-d)) ^ 2)⁻¹ = ∑' (b : ℤ), ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
]

Goal state after:
k : ℤ
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inl
k : ℤ
hk_neg : k < 0
⊢ 0 < Cardinal.aleph0

Tactic:
]

Goal state after:
case inl
k : ℤ
hk_neg : k < 0
⊢ 0 < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inl
k : ℕ
hk_even : Even ↑k
⊢ ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) < Cardinal.aleph0

Tactic:
]

Goal state after:
case inr.inl
k : ℕ
hk_even : Even ↑k
⊢ ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℤ), ∑ m ∈ Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) atTop
    (𝓝 (∑'[symmetricIco ℤ] (x : ℤ), (↑z ^ 2)⁻¹ * e2Summand x (S • z)))

Tactic:
]

Goal state after:
z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℤ), ∑ m ∈ Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2) atTop
    (𝓝 (∑'[symmetricIco ℤ] (x : ℤ), (↑z ^ 2)⁻¹ * e2Summand x (S • z)))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ 0 < Cardinal.aleph0

Tactic:
]

Goal state after:
case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ 0 < Cardinal.aleph0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this : T • z ≠ z
⊢ ¬T • z = z

Tactic:
]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this : T • z ≠ z
⊢ ¬T • z = z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ ∑' (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

pp: case h₁
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n : ℤ
⊢ ∑' (c : ℤ), eisSummand ↑k ![(-n, c).1, (-n, c).2] z = ∑' (c : ℤ), eisSummand ↑k ![(n, c).1, (n, c).2] z

Tactic:
]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ ∑' (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

case h₁
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n : ℤ
⊢ ∑' (c : ℤ), eisSummand ↑k ![(-n, c).1, (-n, c).2] z = ∑' (c : ℤ), eisSummand ↑k ![(n, c).1, (n, c).2] z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑ n ∈ Ico (-↑N) ↑N, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) atTop (𝓝 ((↑z ^ 2)⁻¹ * G2 (S • z)))

Tactic:
]

Goal state after:
z : ℍ
⊢ Tendsto (fun N ↦ ∑ n ∈ Ico (-↑N) ↑N, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) atTop (𝓝 ((↑z ^ 2)⁻¹ * G2 (S • z)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

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

pp: z : ℍ
x : ℕ
⊢ ∀ i ∈ Ico (-↑x) ↑x, Summable fun n ↦ 1 / (↑n * ↑z + ↑i) ^ 2

Tactic:
]

Goal state after:
z : ℍ
x : ℕ
⊢ ∀ i ∈ Ico (-↑x) ↑x, Summable fun n ↦ 1 / (↑n * ↑z + ↑i) ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : I = z ∨ ↑I = -↑z
⊢ z = I

Tactic:
]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : I = z ∨ ↑I = -↑z
⊢ z = I
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
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯ = 0

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
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯ = 0