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

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k
f : F
γ : SL(2, ℤ)
hγ : γ ∈ Γ
z : ℍ
⊢ (Matrix.SpecialLinearGroup.mapGL ℝ) γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ

Tactic:
simpa using hγ

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : g * j * g⁻¹ ∈ Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g

Tactic:
simpa using

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : g * j * g⁻¹ ∈ Γ
⊢ ⇑f ∣[k] (g * j) = ⇑f ∣[k] g
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (↑(↑N * n) +ᵥ z) = f z

Tactic:
simpa using

Goal state after:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (↑N * ↑n +ᵥ z) = f z
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h✝ : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
h : -upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢

Tactic:
simpa using

Goal state after:
case neg.inr
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h✝ : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
h : -upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: case mpr
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ f ∣[k] γ = f

Tactic:
apply Subgroup.closure_induction (p := fun γ _ ↦ f ∣[k] γ = f) h (by simp)

Goal state after:
case mpr.mul
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ∀ (x y : GL (Fin 2) ℝ),
    x ∈ Subgroup.closure s → y ∈ Subgroup.closure s → f ∣[k] x = f → f ∣[k] y = f → f ∣[k] (x * y) = f

case mpr.inv
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ∀ x ∈ Subgroup.closure s, f ∣[k] x = f → f ∣[k] x⁻¹ = f

case mpr.hx
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ γ ∈ Subgroup.closure s
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
x✝ : ∃ x_1 ∈ Γ, (algebraMap ℤ ℝ).mapMatrix ↑x_1 = ↑(upperRightHom x)
g : SL(2, ℤ)
left✝ : g ∈ Γ
hg : (algebraMap ℤ ℝ).mapMatrix ↑g = ↑(upperRightHom x)
⊢ (fun x ↦ x • 1) (↑g 0 1) = x

Tactic:
simpa using

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
x✝ : ∃ x_1 ∈ Γ, (algebraMap ℤ ℝ).mapMatrix ↑x_1 = ↑(upperRightHom x)
g : SL(2, ℤ)
left✝ : g ∈ Γ
hg : (algebraMap ℤ ℝ).mapMatrix ↑g = ↑(upperRightHom x)
⊢ ↑(↑g 0 1) = x
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: ⊢ (mapGL ℝ).range.strictPeriods = AddSubgroup.zmultiples 1

Tactic:
simpa using

Goal state after:
⊢ (map (mapGL ℝ) ⊤).strictPeriods = AddSubgroup.zmultiples 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: ⊢ (mapGL ℝ).range.strictWidthInfty = 1

Tactic:
simpa using

Goal state after:
⊢ (map (mapGL ℝ) ⊤).strictWidthInfty = 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case inl
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
simpa using

Goal state after:
case inl
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ upperRightHom (2 * 𝒢.widthInfty) ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case inr
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : -upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
simpa using

Goal state after:
case inr
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : -upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ upperRightHom (2 * 𝒢.widthInfty) ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 0 =
      ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 1 1 ∧
    ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 1 ≠ 0

Tactic:
simpa using

Goal state after:
case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ¬𝒢.strictWidthInfty = 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : -upperRightHom x ∈ 𝒢
hgi : ↑(-upperRightHom x) 1 0 = 0
⊢ upperRightHom (2 • x) ∈ 𝒢

Tactic:
simpa using

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : -upperRightHom x ∈ 𝒢
hgi : ↑(-upperRightHom x) 1 0 = 0
⊢ upperRightHom x ^ 2 ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ IsCusp ∞ 𝒢

Tactic:
simpa using

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ ∃ y, OnePoint.map Rat.cast y = ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ x = ↑(↑g 0 1)

Tactic:
simpa using

Goal state after:
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ x = ↑(↑g 0 1)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ 0 < ↑(Matrix.GeneralLinearGroup.det (J * g))

Tactic:
simpa using

Goal state after:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ (↑g).det < 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
⊢ c✝.IsBoundedAt ({ toFun := ⇑f, slash_action_eq' := ⋯ } + { toFun := ⇑g, slash_action_eq' := ⋯ }).toFun k

Tactic:
simpa using

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
⊢ c✝.IsBoundedAt (⇑f + ⇑g) k
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty (toFun 0 ∣[k] g)

Tactic:
simpa using

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
a : α
y z : ℂ
⊢ (a • y) • z = a • y • z

Tactic:
simpa using

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
a : α
y z : ℂ
⊢ a • y * z = a • (y * z)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : ModularForm Γ k
⊢ MDiff ⇑(c • f.toSlashInvariantForm)

Tactic:
simpa using

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : ModularForm Γ k
⊢ MDiff (c • ⇑f)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
simpa using

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ ((σ g) (c • 1) • ⇑f ∣[k] g) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
τ : ℍ
hh : h ≠ 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
⊢ cuspFunction h f (𝕢 h ↑τ) = f τ

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
τ : ℍ
hh : h ≠ 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
⊢ Periodic.cuspFunction h (f ∘ ↑ofComplex) (𝕢 h ↑τ) = f τ
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
⊢ MDiff ⇑(c • f.toSlashInvariantForm)

Tactic:
simpa using

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
⊢ MDiff (c • ⇑f)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ ball 0 1 ∈ 𝓝 0

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ {x | ‖x‖ < 1} ∈ 𝓝 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
τ : ℍ
⊢ (cuspFunction h f ∘ fun τ ↦ 𝕢 h ↑τ) τ = f τ

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
τ : ℍ
⊢ cuspFunction h f (𝕢 h ↑τ) = f τ
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
this : (cuspFunction h f ∘ fun τ ↦ 𝕢 h ↑τ) = f
⊢ Tendsto f atImInfty (𝓝 (cuspFunction h f 0))

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
this : (cuspFunction h f ∘ fun τ ↦ 𝕢 h ↑τ) = f
⊢ Tendsto f atImInfty (𝓝 (cuspFunction h f 0))
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
c✝ : OnePoint ℝ
A : IsCusp c✝ Γ
⊢ c✝.IsZeroAt ({ toFun := ⇑f, slash_action_eq' := ⋯ } + { toFun := ⇑g, slash_action_eq' := ⋯ }).toFun k

Tactic:
simpa using

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
c✝ : OnePoint ℝ
A : IsCusp c✝ Γ
⊢ c✝.IsZeroAt (⇑f + ⇑g) k
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
a : α
y z : ℂ
⊢ (a • y) • z = a • y • z

Tactic:
simpa using

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
a : α
y z : ℂ
⊢ a • y * z = a • (y * z)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
⊢ MDiff ⇑(c • f.toSlashInvariantForm)

Tactic:
simpa using

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
⊢ MDiff (c • ⇑f)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
⊢ MDiff ⇑(c • f.toSlashInvariantForm)

Tactic:
simpa using

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
⊢ MDiff (c • ⇑f)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
⊢ (w + ↑h).im ≤ 0

Tactic:
simpa using

Goal state after:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
⊢ w.im ≤ 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case succ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩
⊢ ⟨(n + 1) • k, GradedMonoid.GMonoid.gnpow (n + 1) f⟩ = ⟨↑(n + 1) * k, f.pow (n + 1)⟩

Tactic:
refine (GradedMonoid.GMonoid.gnpow_succ' n ⟨k, f⟩).trans ?_

Goal state after:
case succ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩
⊢ ⟨n • ⟨k, f⟩.fst, GradedMonoid.GMonoid.gnpow n ⟨k, f⟩.snd⟩ * ⟨k, f⟩ = ⟨↑(n + 1) * k, f.pow (n + 1)⟩
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case succ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩
⊢ ⟨↑n * k, f.pow n⟩ * ⟨k, f⟩ = ⟨↑(n + 1) * k, f.pow (n + 1)⟩

Tactic:
exact gradedMonoid_eq_of_cast (show ((n : ℤ) * k + k = (n + 1) * k) by ring)
      (ModularForm.ext fun _ ↦ rfl)

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ ?m.56 ∈ ball 0 1

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
⊢ ‖?m.56‖ < 1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
this : ‖𝕢 h ↑τ‖ < 1
⊢ HasSum (fun m ↦ (PowerSeries.coeff m) (qExpansion h f) • 𝕢 h ↑τ ^ m) (f τ)

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
this : ‖𝕢 h ↑τ‖ < 1
⊢ HasSum (fun m ↦ (PowerSeries.coeff m) (qExpansion h f) * 𝕢 h ↑τ ^ m) (f τ)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsCusp ((g * γ) • ∞) Γ

Tactic:
simpa using

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsCusp (g • c) Γ
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ ‖↑↑r‖ < 1

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ r < 1
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsCusp ((g * γ) • ∞) Γ

Tactic:
simpa using

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsCusp (g • c) Γ
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ?m.1
F : Sort ?u.11
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : Γ.IsArithmetic
⊢ IsCusp ∞ Γ

Tactic:
simpa using

Goal state after:
k : ?m.1
F : Sort ?u.11
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : Γ.IsArithmetic
⊢ ∃ y, OnePoint.map Rat.cast y = ∞
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
h : Int.cast ∘ p = 0
i : Fin 2
⊢ p i = 0 i

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
h : Int.cast ∘ p = 0
i : Fin 2
⊢ p i = 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
⊢ ↑(p 0) * ↑z + ↑(p 1) ≠ 0

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
⊢ ¬↑(p 0) * ↑z + ↑(p 1) = 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case r_le.inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
r : NNReal
hr : ↑r < 1
hr' : ↑r ≠ 0
this : FiniteDimensional ℝ ℂ := ⋯
⊢ Summable fun n ↦ ‖FormalMultilinearSeries.ofScalars ℂ c n‖ * ↑r ^ n

Tactic:
simpa using

Goal state after:
case r_le.inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
r : NNReal
hr : ↑r < 1
hr' : ↑r ≠ 0
this : FiniteDimensional ℝ ℂ := Module.Basis.finiteDimensional_of_finite basisOneI
⊢ Summable fun n ↦ ↑r ^ n * ‖c n‖
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
r : NNReal
hr : ↑r < 1
hr' : ↑r ≠ 0
this : FiniteDimensional ℝ ℂ := Module.Basis.finiteDimensional_of_finite basisOneI
⊢ ‖↑↑r‖ < 1

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
r : NNReal
hr : ↑r < 1
hr' : ↑r ≠ 0
this : FiniteDimensional ℝ ℂ := Module.Basis.finiteDimensional_of_finite basisOneI
⊢ r < 1
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
⊢ petersson k (⇑f) (⇑f') (g • τ) = petersson k (⇑f) (⇑f') τ

Tactic:
simpa using

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
⊢ petersson k (⇑f) (⇑f') (g • τ) = petersson k (⇑f) (⇑f') τ
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
⊢ ∃ E_1, ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E_1

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
⊢ ∃ E_1, ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E_1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case hasSum.inl
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hy : ‖0‖ < 1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ 0) (update (cuspFunction h f) 0 (c 0) (0 + 0))

Tactic:
simpa using

Goal state after:
case hasSum.inl
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hy : ‖0‖ < 1
⊢ HasSum (fun n ↦ if n = 0 then c 0 else 0) (c 0)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case hasSum.inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
hy' : y ≠ 0
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))

Tactic:
simpa using

Goal state after:
case hasSum.inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
hy' : y ≠ 0
⊢ HasSum (fun n ↦ c n * y ^ n) (cuspFunction h f y)
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
hf' : IsBoundedAtImInfty ⇑f'
⊢ (fun t ↦ Real.exp (-b * t) * t ^ k) =O[atTop] fun t ↦ Real.exp (-a * t)

Tactic:
simpa using

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
hf' : IsBoundedAtImInfty ⇑f'
⊢ (fun t ↦ Real.exp (-(b * t)) * t ^ k) =O[atTop] fun t ↦ Real.exp (-(a * t))
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hfeq : f = fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)
⊢ Tendsto (fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)) atImInfty (𝓝 (c 0))

Tactic:
simpa using

Goal state after:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hfeq : f = fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)
⊢ Tendsto (fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)) atImInfty (𝓝 (c 0))