mathlib-initiative/mathlib-tactics huggingface dataset:
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 0 = 0 ∨ ↑g 1 0 = 1

Tactic:
by

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

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ![↑m, ↑a] ≠ 0

Tactic:
by

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

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ![↑m, ↑b] ≠ 0

Tactic:
by

Goal state after:
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) - 1 / (↑m * ↑z + ↑b) = (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

Tactic:
by

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

Goal state before:
pp: 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
⊢ ↑k - 12 < 0

Tactic:
by

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

Goal state before:
pp: 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
⊢ k ∈ Finset.filter Even (Finset.Icc 3 11)

Tactic:
by

Goal state after:
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))⁻¹
m : { x // x ∉ {0} }
⊢ ↑m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: k : ℕ
e : ℕ+
z : ℍ
⊢ 0 < (↑↑e * ↑z).im

Tactic:
by

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

Goal state before:
pp: k : ℕ
e : ℕ+
z : ℍ
he : 0 < (↑↑e * ↑z).im
⊢ 0 < 1

Tactic:
by

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

Goal state before:
pp: k : ℕ
e : ℕ+
z : ℍ
he : 0 < (↑↑e * ↑z).im
⊢ (fun n ↦ ↑n ^ k) =O[atTop] fun n ↦ ↑n ^ k

Tactic:
by

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

Goal state before:
pp: k : ℕ
e : ℕ+
z : ℍ
⊢ Summable fun c ↦ ↑c ^ k * cexp (2 * ↑π * I * ↑↑e * ↑z) ^ c

Tactic:
have he : 0 < (e * (z : ℂ)).im := by
    simpa using z.2
  apply ((summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp 0 k (p := 1)
    (f := fun n ↦ (n ^ k : ℂ)) (by norm_num)
    (by simp [← Complex.isBigO_ofReal_right, Asymptotics.isBigO_refl])).summable he).congr
  grind [ofReal_one, iteratedDerivWithin_zero, Pi.smul_apply, smul_eq_mul]

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

Goal state before:
pp: k : ℕ
e : ℕ+
z : ℍ
⊢ Summable fun c ↦ ↑c ^ k * cexp (2 * ↑π * I * ↑↑e * ↑z) ^ c

Tactic:
by

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

Goal state before:
pp: z : ℍ
m : ℤ
this : Summable fun x ↦ ((↑m * ↑z + ↑↑x + 1) * (↑m * ↑z + ↑↑x))⁻¹
b : { x // x ∉ {0, -1} }
⊢ m ≠ 0 ∨ ↑b ≠ 0 ∧ ↑b + 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: 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
⊢ 3 ≤ k

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ k - 12 < k

Tactic:
by

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

Goal state before:
pp: 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
⊢ Even (k - 12)

Tactic:
by

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

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

Tactic:
rw [EisensteinSeries.qExpansion_identity hk z, ← tsum_zero_pnat_eq_tsum_nat]

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.EisensteinSeries.QExpansion

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

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk2 : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ Summable fun x ↦ eisSummand ↑k ![x.1, x.2] z

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
⊢ (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:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ Summable fun b ↦ ∑' (c : ℤ), eisSummand ↑k ![(b, c).1, (b, c).2] z

Tactic:
by

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

Goal state before:
pp: k : ℤ
⊢ FiniteDimensional ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)

Tactic:
by

Goal state after:
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 +ᵥ ρ
⊢ T • z ≠ z

Tactic:
by

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

Goal state before:
pp: 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
this : CuspForm.discriminantEquiv (f.toCuspForm h0) = 0
⊢ f = 0

Tactic:
by

Goal state after:
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:
by

Goal state after:
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 (𝓝 ((↑z ^ 2)⁻¹ * G2 (S • z)))

Tactic:
by

Goal state after:
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
this : T⁻¹ • z ≠ z
⊢ ↑z ≠ -↑I

Tactic:
by

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

Goal state before:
pp: z : ℍ
x : ℕ
i : ℤ
hi : i ∈ Ico (-↑x) ↑x
⊢ Summable fun n ↦ 1 / (↑n * ↑z + ↑i) ^ 2

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n y : ℤ
⊢ eisSummand ↑k ![(-n, -y).1, (-n, -y).2] z = eisSummand ↑k ![(n, y).1, (n, y).2] z

Tactic:
by

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

Goal state before:
pp: z : ℍ
⊢ ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 = (↑z ^ 2)⁻¹ * G2 (S • z)

Tactic:
by

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

Goal state before:
pp: 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 : k < 12
⊢ ↑k - 12 < 0

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
b : ℕ+
⊢ 1 ≤ k - 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
b : ℕ+
⊢ 0 < (↑↑b * ↑z).im

Tactic:
by

Goal state after:
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
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
⊢ S • z ≠ z

Tactic:
by

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

Goal state before:
pp: z : ℍ
m : ℤ
⊢ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 0

Tactic:
by

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

Goal state before:
pp: 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
⊢ ↑k - 12 = ↑(k - 12)

Tactic:
by

Goal state after:
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 +ᵥ ρ
⊢ g = 1 ∨ g = -1

Tactic:
by

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

Goal state before:
pp: 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
⊢ k - 12 < k

Tactic:
by

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

Goal state before:
pp: 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
⊢ k / 12 = (k - 12) / 12 + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∑' (m : ℤ), (1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)) =
    -(2 / ↑↑d) +
      ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d))

Tactic:
by

Goal state after:
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
⊢ 2 ≤ k

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ S • ρ ≠ ρ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∀ (b : ℕ+),
    1 / (↑↑b * ↑z - ↑↑d) + 1 / (-↑↑b * ↑z + -↑↑d) - 1 / (↑↑b * ↑z + ↑↑d) - 1 / (-↑↑b * ↑z + ↑↑d) =
      2 / ↑z * (1 / (-↑↑d / ↑z - ↑↑b) + 1 / (-↑↑d / ↑z + ↑↑b))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ -↑↑d ≠ 0

Tactic:
by

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ?m.161 ∈ integerComplement

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

Goal state after:
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
this :
  ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑m * ↑z)) ^ ↑n =
    ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * ↑z) ^ (↑m * ↑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:
by

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

Goal state before:
pp: τ : ℂ
⊢ ∀ (b : ℤ), cexp (↑π * I * ↑b ^ 2 * τ) = jacobiTheta₂_term b 0 τ

Tactic:
by

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

Goal state before:
pp: τ : ℂ
⊢ jacobiTheta (2 + τ) = jacobiTheta τ

Tactic:
by

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

Goal state before:
pp: τ : ℂ
⊢ jacobiTheta (2 + τ) = jacobiTheta τ

Tactic:
by
  simp_rw [jacobiTheta_eq_jacobiTheta₂, add_comm, jacobiTheta₂_add_right]

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

Goal state before:
pp: τ : ℍ
this : ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ

Tactic:
by

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

Goal state before:
pp: τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ

Tactic:
by

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

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
⊢ (-I * ↑τ) ^ (1 / 2) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

Goal state after:
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)) =
    2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ (T * S * T) • ρ ≠ ρ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑' (n : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑n) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ g ≠ T * S * T ∧ g ≠ -(T * S * T)

Tactic:
by

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

Goal state before:
pp: τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

Tactic:
by

Goal state after:
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
m n : ℕ+
⊢ ↑↑n ^ (k - 1) * cexp (↑↑n * (2 * ↑π * I * (↑↑m * ↑z))) = ↑↑n ^ (k - 1) * cexp (↑(↑m * ↑n) * (2 * ↑π * I * ↑z))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

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

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N
⊢ Summable (HPow.hPow (cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ })))

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by

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

Goal state before:
pp: z : ℍ
⊢ (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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ 1 < k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
⊢ ρ ∉ 𝒟ᵒ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
h : 1 +ᵥ ρ ∈ 𝒟ᵒ
⊢ (1 +ᵥ ρ).re = 1 / 2

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun x ↦ ‖1 / ↑x ^ k‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
⊢ 1 +ᵥ ρ ∉ 𝒟ᵒ

Tactic:
by

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 : (r : ℕ) × ↑(gammaSet 1 r 0)),
    ((fun x ↦ eisSummand (↑k) x z) ∘ ⇑gammaSetDivGcdSigmaEquiv.symm) b = eisSummand (↑k) (↑b.snd) z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
⊢ g = 1 ∨ g = -1

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ ↑g 1 0 = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun x ↦ ‖(↑x ^ k)⁻¹‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ z = g • z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ Continuous fun z ↦ normSq ↑z

Tactic:
by

Goal state after: