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

Goal state before:
pp: 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)
⊢ HasSum (fun m ↦ c m • 𝕢 1 ↑τ ^ m) ((E hk) τ)

Tactic:
← hasSum_nat_add_iff' 1

Goal state after:
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)
⊢ HasSum (fun n ↦ c (n + 1) • 𝕢 1 ↑τ ^ (n + 1)) ((E hk) τ - ∑ i ∈ Finset.range 1, c i • 𝕢 1 ↑τ ^ i)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: 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)
⊢ HasSum (fun n ↦ c (n + 1) • 𝕢 1 ↑τ ^ (n + 1)) ((E hk) τ - ∑ i ∈ Finset.range 1, c i • 𝕢 1 ↑τ ^ i)

Tactic:
]

Goal state after:
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)
⊢ HasSum (fun n ↦ c (n + 1) • 𝕢 1 ↑τ ^ (n + 1)) ((E hk) τ - ∑ i ∈ Finset.range 1, c i • 𝕢 1 ↑τ ^ i)
Module: Mathlib.NumberTheory.Modular

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

Tactic:
]

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ x ∈ 𝒟ᵒ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))

Tactic:
]

Goal state after:
y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))
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 𝒟
⊢ ‖↑x‖ ∈ interior (Set.Ici 1)

Tactic:
]

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

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

Tactic:
]

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' Set.Ici 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: 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)
this : (E hk) τ = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n
⊢ 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n - 1 =
    β * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n

Tactic:
]

Goal state after:
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)
this : (E hk) τ = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n
⊢ 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n - 1 =
    β * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n
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 ∈ interior (Set.Icc (-(1 / 2)) (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 ∈ interior (Set.Icc (-(1 / 2)) (1 / 2))
Module: Mathlib.NumberTheory.Modular

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

Tactic:
]

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 𝒟 ⊆ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: 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)
⊢ HasSum (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1))
    (β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1))

Tactic:
]

Goal state after:
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)
⊢ HasSum (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1))
    (β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1))
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) =
    β * ∑' (x : ℕ), ↑((σ (k - 1)) (x + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (x + 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
]

Goal state after:
y : ℝ
⊢ IsClosed {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} ∧
    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 ≤ (1 / 2) ^ 2 + y ^ 2

Tactic:
]

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.ModularForms.LevelOne.GradedRing

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆) =
    1728

Tactic:
]

Goal state after:
⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆) =
    1728
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| ≤ 1 / 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| ≤ 1 / 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 ≤ y

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 ≤ y
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hcΔ : c • ⇑CuspForm.discriminant = ⇑g
hgΔ : qExpansion 1 ⇑E₄CubeSubE₆SqForm = c • qExpansion 1 ⇑CuspForm.discriminant
⊢ c = 1728

Tactic:
]

Goal state after:
z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hcΔ : c • ⇑CuspForm.discriminant = ⇑g
hgΔ : qExpansion 1 ⇑E₄CubeSubE₆SqForm = c • qExpansion 1 ⇑CuspForm.discriminant
⊢ c = 1728
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hc_eq : c = 1728
⊢ E₄ z ^ 3 - E₆ z ^ 2 = E₄ z ^ 3 - E₆ z ^ 2

Tactic:
]

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

Goal state before:
pp: ⊢ (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (modularForm CuspForm.discriminant) =
    (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) ((1 / 1728) • (E₄.pow 3 - E₆.pow 2))

Tactic:
]

Goal state after:
⊢ (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (modularForm CuspForm.discriminant) =
    (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) ((1 / 1728) • (E₄.pow 3 - E₆.pow 2))
Module: Mathlib.NumberTheory.Modular

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

Tactic:
]

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ

Tactic:
]

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g

Tactic:
]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g
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✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) =O[atImInfty] 1

Tactic:
]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) =O[atImInfty] 1
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✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 (∑ c, 0))

Tactic:
]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 (∑ c, 0))
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: ⊢ Tendsto (UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)) atTop atTop

Tactic:
]

Goal state after:
⊢ Tendsto (UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)) atTop atTop
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
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (|↑(Matrix.GeneralLinearGroup.det γ)| ^ (↑Finset.univ.card - 1) • ∏ i, quotientFunc f i ∣[k] γ) =O[atImInfty] 1

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
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (|↑(Matrix.GeneralLinearGroup.det γ)| ^ (↑Finset.univ.card - 1) • ∏ i, quotientFunc f i ∣[k] γ) =O[atImInfty] 1
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
S : Subgroup Γ
⊢ (∀ {K L : Set α}, IsCompact K → IsCompact L → {m | (m • K ∩ L).Nonempty}.Finite) ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
]

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
S : Subgroup Γ
⊢ (∀ {K L : Set α}, IsCompact K → IsCompact L → {m | (m • K ∩ L).Nonempty}.Finite) ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite
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
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (fun a ↦ ∏ c, (quotientFunc f c ∣[k] γ) a) =O[atImInfty] fun x ↦ ∏ i, 1

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
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (fun a ↦ ∏ c, (quotientFunc f c ∣[k] γ) a) =O[atImInfty] fun x ↦ ∏ i, 1
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
]

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
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

𝒢 ℋ : 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)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ f (↑ofComplex (I * ↑(1 / t))) =
    (I ^ k * ↑(t ^ ↑k)) •
      (fun τ ↦
          (σ (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
                (f
                  (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
                    τ)) *
              ↑|↑(Matrix.GeneralLinearGroup.det
                        (Matrix.SpecialLinearGroup.toGL
                          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))| ^
                (k - 1) *
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
                ↑τ ^
              (-k))
        (↑ofComplex (I * ↑t))

Tactic:
]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ f (↑ofComplex (I * ↑(1 / t))) =
    (I ^ k * ↑(t ^ ↑k)) •
      (fun τ ↦
          (σ (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))
                (f
                  (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
                    τ)) *
              ↑|↑(Matrix.GeneralLinearGroup.det
                        (Matrix.SpecialLinearGroup.toGL
                          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))| ^
                (k - 1) *
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
                ↑τ ^
              (-k))
        (↑ofComplex (I * ↑t))
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
]

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
x✝ : ℍ
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 0) (Matrix.SpecialLinearGroup.mapGL ℝ).range 0

Tactic:
]

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 0) (Matrix.SpecialLinearGroup.mapGL ℝ).range 0
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ f { coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    1 *
      f
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
          { coe := I * ↑t, coe_im_pos := ⋯ })

Tactic:
]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ f { coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    1 *
      f
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S) •
          { coe := I * ↑t, coe_im_pos := ⋯ })
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e_6
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ ↑{ coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    num (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ } /
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ }

Tactic:
]

Goal state after:
case e_6
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ ↑{ coe := I * ↑t⁻¹, coe_im_pos := ⋯ } =
    num (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ } /
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))
        ↑{ coe := I * ↑t, coe_im_pos := ⋯ }