awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))

Tactic:
⟨N, ‹_›, fun x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro, CongruenceSubgroup.IsCongruenceSubgroup
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))
refine :
  ∀ (x : SL(2, ℤ)) (hx : x ∈ Γ(N)),
    x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))

Tactic:
refine ⟨N, ‹_›, fun x hx ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))
x : SL(2, ℤ)
hx : x ∈ Γ(N)
obtain :
  ∀ (y : SL(2, ℤ)) (hy : y ∈ (↑Γ(M) : Set SL(2, ℤ)))
    (hy' :
      (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) y =
        HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)),
    x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)
⊢ x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)

Tactic:
obtain ⟨y, hy, hy'⟩ := Subgroup.mem_inv_pointwise_smul_iff.mp <| hN' ⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, Iff.mp, Subgroup.mem_inv_pointwise_smul_iff, rfl
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))
x : SL(2, ℤ)
hx : x ∈ Γ(N)
y : SL(2, ℤ)
hy : y ∈ (↑Γ(M) : Set SL(2, ℤ))
hy' :
  (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) y =
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
⊢ x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)

Tactic:
mem_conjGL.mpr ⟨y, hΓM hy, hy'⟩

Premises used: Iff.mpr, CongruenceSubgroup.mem_conjGL, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))
x : SL(2, ℤ)
hx : x ∈ Γ(N)
y : SL(2, ℤ)
hy : y ∈ (↑Γ(M) : Set SL(2, ℤ))
hy' :
  (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) y =
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
⊢ x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)

Tactic:
exact mem_conjGL.mpr ⟨y, hΓM hy, hy'⟩

Premises used: Iff.mpr, CongruenceSubgroup.mem_conjGL, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
f : CuspForm Γ k
z : ℍ
⊢ Eq (α := ℂ) ((((toModularFormₗ : (a : CuspForm Γ k) → ModularForm Γ k) f : ModularForm Γ k) : (a : ℍ) → ℂ) z : ℂ)
    ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
f : CuspForm Γ k
⊢ (toModularFormₗ : (a : CuspForm Γ k) → ModularForm Γ k) f = modularForm f

Tactic:
rfl

Premises used: ModularFormClass.modularForm, rfl
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
⊢ Function.Injective (α := CuspForm Γ k) (β := ModularForm Γ k) (⇑toModularFormₗ : (a : CuspForm Γ k) → ModularForm Γ k)

Tactic:
fun _ _ h ↦ DFunLike.ext _ _ fun z ↦ DFunLike.congr_fun h z

Premises used: DFunLike.congr_fun, DFunLike.ext, Function.Injective
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
f : ModularForm Γ k
⊢ Membership.mem (γ := Submodule ℂ (ModularForm Γ k)) (cuspFormSubmodule Γ k) f ↔ f.IsCuspForm

Tactic:
Iff.rfl

Premises used: ModularForm.IsCuspForm, Iff.rfl
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetOne
f : CuspForm Γ k
⊢ IsCuspForm (Γ := Γ) (k := k) ((CuspForm.toModularFormₗ : (a : CuspForm Γ k) → ModularForm Γ k) f)

Tactic:
simp [← mem_cuspFormSubmodule_iff, ModularForm.cuspFormSubmodule]

Premises used: ModularForm.mem_cuspFormSubmodule_iff, ModularForm.cuspFormSubmodule
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
f : ModularForm Γ k
⊢ f.IsCuspForm ↔ ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt (⇑f : (a : ℍ) → ℂ) k

Tactic:
⟨fun ⟨g, hg⟩ _ ↦ hg ▸ g.zero_at_cusps', fun h ↦ ⟨⟨f, f.holo', h⟩, rfl⟩⟩

Premises used: Eq.rec, SlashInvariantForm.mk, CuspForm.zero_at_cusps', _private.0.ModularForm.isCuspForm_iff.match_1, Iff.intro, Exists.intro, ModularForm.holo', CuspForm.mk, DFunLike.coe, SlashInvariantForm.slash_action_eqn, rfl
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
⊢ 0 < Γ.strictWidthInfty

Tactic:
have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
⊢ Γ.strictWidthInfty ∈ Γ.strictPeriods

Tactic:
have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
⊢ AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0

Tactic:
have hanal := ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0
⊢ Function.Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑Γ.strictWidthInfty : ℂ)

Tactic:
have hper := periodic_comp_ofComplex f hΓ
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0
hper : Function.Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑Γ.strictWidthInfty : ℂ)
simp_rw : Tendsto (⇑f : (a : ℍ) → ℂ) atImInfty (𝓝 (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ) 0))
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)

Tactic:
simp_rw [IsZeroAtImInfty, ZeroAtFilter, ← h, ← cuspFunction_apply_zero hh hanal hper]

Premises used: Filter.ZeroAtFilter, UpperHalfPlane.IsZeroAtImInfty, UpperHalfPlane.cuspFunction_apply_zero
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0
hper : Function.Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑Γ.strictWidthInfty : ℂ)
⊢ Tendsto (⇑f : (a : ℍ) → ℂ) atImInfty (𝓝 (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ) 0))

Tactic:
(hanal.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)).congr
    (fun τ ↦ SlashInvariantFormClass.eq_cuspFunction f τ hΓ hh.ne')

Premises used: SlashInvariantFormClass.eq_cuspFunction, UpperHalfPlane.qParam_tendsto_atImInfty, LT.lt.ne', ContinuousAt.tendsto, Filter.Tendsto.congr, AnalyticAt.continuousAt, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0
hper : Function.Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑Γ.strictWidthInfty : ℂ)
⊢ Tendsto (⇑f : (a : ℍ) → ℂ) atImInfty (𝓝 (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ) 0))

Tactic:
exact (hanal.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)).congr
    (fun τ ↦ SlashInvariantFormClass.eq_cuspFunction f τ hΓ hh.ne')

Premises used: SlashInvariantFormClass.eq_cuspFunction, UpperHalfPlane.qParam_tendsto_atImInfty, LT.lt.ne', ContinuousAt.tendsto, Filter.Tendsto.congr, AnalyticAt.continuousAt, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
rw :
  ∀ (γ : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
          ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
        c →
      IsZeroAtImInfty (α := ℂ)
        (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
          (⇑f : (a : ℍ) → ℂ))
⊢ c.IsZeroAt (⇑f : (a : ℍ) → ℂ) k

Tactic:
rw [isZeroAt_iff_forall_SL2Z hc]

Premises used: OnePoint.isZeroAt_iff_forall_SL2Z
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
_ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
      c →
    IsZeroAtImInfty (α := ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
        (⇑f : (a : ℍ) → ℂ))
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
      c →
    IsZeroAtImInfty (α := ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
        (⇑f : (a : ℍ) → ℂ))

Tactic:
_
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h_1 :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
rw : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
⊢ IsZeroAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (⇑f : (a : ℍ) → ℂ))

Tactic:
rw [show (⇑f ∣[k] γ) = ⇑f from f.slash_action_eq' _ ⟨γ, rfl⟩]

Premises used: SlashInvariantForm.slash_action_eq', Real, ModularForm.toSlashInvariantForm, Exists.intro, Matrix.SpecialLinearGroup.mapGL, DFunLike.coe, rfl
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h_1 :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
rwa rwa₁ rwa₂ rwa₃ :
  Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
⊢ valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0

Tactic:
rwa [← qExpansion_coeff_zero one_pos
      (ModularFormClass.analyticAt_cuspFunction_zero f one_pos one_mem_strictPeriods_SL)
      (periodic_comp_ofComplex f one_mem_strictPeriods_SL)]

Premises used: one_mem_strictPeriods_SL, UpperHalfPlane.qExpansion_coeff_zero, SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.analyticAt_cuspFunction_zero, one_pos
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h_1 :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)

Tactic:
exact isZeroAtImInfty_of_valueAtInfty_eq_zero f <| by
    rwa [← qExpansion_coeff_zero one_pos
      (ModularFormClass.analyticAt_cuspFunction_zero f one_pos one_mem_strictPeriods_SL)
      (periodic_comp_ofComplex f one_mem_strictPeriods_SL)]

Premises used: ModularForm.isZeroAtImInfty_of_valueAtInfty_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
z : ℍ
⊢ Eq (α := ℂ) ((f.toCuspForm h : (a : ℍ) → ℂ) z : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ f.IsCuspForm ↔
    Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)

Tactic:
⟨fun ⟨g, hg⟩ ↦ ?_, fun h ↦ (isCuspForm_iff f).mpr (isZeroAt_of_coeffZero_eq_zero f h)⟩

Premises used: Iff.mpr, ModularForm.isZeroAt_of_coeffZero_eq_zero, UpperHalfPlane.qExpansion, PowerSeries.coeff, _private.0.ModularForm.isCuspForm_iff_coeffZero_eq_zero.match_1, Iff.intro, ModularForm.isCuspForm_iff, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
refine :
  f.IsCuspForm →
    ∀ (g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k)
      (hg :
        (CuspForm.toModularFormₗ :
              (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
            g =
          f),
      Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
⊢ f.IsCuspForm ↔
    Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)

Tactic:
refine ⟨fun ⟨g, hg⟩ ↦ ?_, fun h ↦ (isCuspForm_iff f).mpr (isZeroAt_of_coeffZero_eq_zero f h)⟩
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : f.IsCuspForm
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
      g =
    f
rw :
  valueAtInfty
      (⇑((CuspForm.toModularFormₗ :
                (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                  ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
              g :
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) :
        (a : ℍ) → ℂ) =
    0
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)

Tactic:
rw [← hg, qExpansion_coeff_zero one_pos
    (ModularFormClass.analyticAt_cuspFunction_zero _ one_pos one_mem_strictPeriods_SL)
    (periodic_comp_ofComplex _ one_mem_strictPeriods_SL)]

Premises used: one_mem_strictPeriods_SL, UpperHalfPlane.qExpansion_coeff_zero, SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.analyticAt_cuspFunction_zero, one_pos
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : f.IsCuspForm
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
      g =
    f
⊢ valueAtInfty
      (⇑((CuspForm.toModularFormₗ :
                (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                  ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
              g :
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) :
        (a : ℍ) → ℂ) =
    0

Tactic:
(CuspFormClass.zero_at_infty g).valueAtInfty_eq_zero

Premises used: CuspFormClass.zero_at_infty, UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : f.IsCuspForm
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
      g =
    f
⊢ valueAtInfty
      (⇑((CuspForm.toModularFormₗ :
                (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                  ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
              g :
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) :
        (a : ℍ) → ℂ) =
    0

Tactic:
exact (CuspFormClass.zero_at_infty g).valueAtInfty_eq_zero

Premises used: CuspFormClass.zero_at_infty, UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
A : Type u_2
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : IsPrincipalIdealRing A
⊢ HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) 1) ∞ = ∞

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
A : Type u_2
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : IsPrincipalIdealRing A
⊢ ∃ (g : SL(2, A)),
    HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ = ∞

Tactic:
exact ⟨1, by simp⟩