awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih :
  Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
    Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)
⊢ Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n) * Sigma.mk (β := ModularForm Γ) k f =
    Sigma.mk (β := ModularForm Γ) ((↑(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)

Premises used: ModularForm.gradedMonoid_eq_of_cast, ModularForm.ext, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
zero :
  Sigma.mk (β := ModularForm Γ) (HSMul.hSMul (α := ℕ) 0 k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) 0 f) =
    Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)
succ :
  ∀ (n : ℕ)
    (ih :
      Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
        Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)),
    Sigma.mk (β := ModularForm Γ) ((n + 1) • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) (n + 1) f) =
      Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
⊢ Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
    Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)

Tactic:
induction n with
  | zero =>
    refine (GradedMonoid.GMonoid.gnpow_zero' ⟨k, f⟩).trans ?_
    exact gradedMonoid_eq_of_cast (zero_mul k).symm (ModularForm.ext fun _ ↦ rfl)
  | succ n ih =>
    refine (GradedMonoid.GMonoid.gnpow_succ' n ⟨k, f⟩).trans ?_
    refine (congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_
    exact gradedMonoid_eq_of_cast (show ((n : ℤ) * k + k = (n + 1) * k) by ring)
      (ModularForm.ext fun _ ↦ rfl)

Premises used: GradedMonoid.GMonoid.gnpow_zero', ModularForm.gradedMonoid_eq_of_cast, ModularForm.ext, GradedMonoid.GMonoid.gnpow_succ', Sigma.mk, rfl, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ HPow.hPow (α := DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
      ((DirectSum.of (ModularForm Γ) k : (a : ModularForm Γ k) → DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i) f :
        DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
      n =
    (DirectSum.of (ModularForm Γ) ((↑n : ℤ) * k) :
        (a : ModularForm Γ ((↑n : ℤ) * k)) → DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
      (f.pow n)

Tactic:
grind [DirectSum.ofPow, DirectSum.of_eq_of_gradedMonoid_eq (gnpow_eq_pow f n)]

Premises used: DirectSum.ofPow, ModularForm.gnpow_eq_pow, DirectSum.of_eq_of_gradedMonoid_eq
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
i : ι
hi : i ∈ s
⊢ MDiff ((fun (i : ι) ↦ ((⇑(F i).toSlashInvariantForm : (a : ℍ) → ℂ) : (a : ℍ) → ℂ)) i)

Tactic:
simpa using (F i).holo'

Premises used: ModularForm.holo'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
simp :
  atImInfty.BoundedAtFilter
    (HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) γ) : ℝ)|
        (HSub.hSub (α := ℤ) (↑s.card : ℤ) 1))
      (∏ i ∈ s,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ)))
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ m γ
      (toFun (Γ := Γ)
        (SlashInvariantForm.prod m hm fun (i : ι) ↦
          { toFun := (⇑(F i) : (a : ℍ) → ℂ), slash_action_eq' := ⋯ : SlashInvariantForm Γ (k i) })))

Tactic:
simp only [SlashInvariantForm.toFun_eq_coe, coe_prod, SlashInvariantForm.coe_mk, hm,
      prod_slash_sum_weights, IsBoundedAtImInfty]

Premises used: UpperHalfPlane.IsBoundedAtImInfty, ModularForm.prod_slash_sum_weights, SlashInvariantForm.coe_mk, SlashInvariantForm.toFun_eq_coe, ModularForm.coe_prod
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
⊢ atImInfty.BoundedAtFilter
    (HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) γ) : ℝ)|
        (HSub.hSub (α := ℤ) (↑s.card : ℤ) 1))
      (∏ i ∈ s,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ)))

Tactic:
BoundedAtFilter.smul _ (BoundedAtFilter.prod (s := s) ?_)

Premises used: Filter.BoundedAtFilter.smul, Filter.BoundedAtFilter.prod
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
refine :
  ∀ i ∈ s,
    atImInfty.BoundedAtFilter (β := ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ))
⊢ atImInfty.BoundedAtFilter
    (HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) γ) : ℝ)|
        (HSub.hSub (α := ℤ) (↑s.card : ℤ) 1))
      (∏ i ∈ s,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ)))

Tactic:
refine BoundedAtFilter.smul _ (BoundedAtFilter.prod (s := s) ?_)

Premises used: Filter.BoundedAtFilter.smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
i : ι
hi : i ∈ s
⊢ atImInfty.BoundedAtFilter (β := ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ))

Tactic:
simpa using (F i).bdd_at_cusps' hc γ hγ

Premises used: ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
ι : Type
s : Finset ι
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ k
⊢ (↑s.card : ℤ) * k = ∑ i ∈ s, k

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
rw : (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsBoundedAt (⇑f : (a : ℍ) → ℂ) k
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (SlashInvariantForm.translate f g).toFun)

Tactic:
rw [SlashInvariantForm.toFun_eq_coe, SlashInvariantForm.coe_translate,
      ← SlashAction.slash_mul, ← isBoundedAt_infty_iff, ← OnePoint.IsBoundedAt.smul_iff]

Premises used: SlashInvariantForm.coe_translate, OnePoint.isBoundedAt_infty_iff, SlashInvariantForm.toFun_eq_coe, SlashAction.slash_mul, OnePoint.IsBoundedAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
apply : IsCusp (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞) Γ
⊢ (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsBoundedAt (⇑f : (a : ℍ) → ℂ) k

Tactic:
apply ModularFormClass.bdd_at_cusps f

Premises used: ModularFormClass.bdd_at_cusps
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
⊢ IsCusp (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞) Γ

Tactic:
simpa [mul_smul, hγ] using hc.smul g

Premises used: SemigroupAction.mul_smul, IsCusp.smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(translate f g) : (a : ℍ) → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))

Tactic:
rfl

Premises used: _private.Mathlib.NumberTheory.ModularForms.SlashActions.0.ModularForm.privateSlash, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
rw : (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsZeroAt (⇑f : (a : ℍ) → ℂ) k
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (ModularForm.translate f g).toFun)

Tactic:
rw [SlashInvariantForm.toFun_eq_coe, ModularForm.toSlashInvariantForm_coe,
      ModularForm.coe_translate, ← SlashAction.slash_mul, ← isZeroAt_infty_iff,
      ← OnePoint.IsZeroAt.smul_iff]

Premises used: OnePoint.isZeroAt_infty_iff, ModularForm.toSlashInvariantForm_coe, OnePoint.IsZeroAt.smul_iff, SlashInvariantForm.toFun_eq_coe, SlashAction.slash_mul, ModularForm.coe_translate
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
apply : IsCusp (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞) Γ
⊢ (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsZeroAt (⇑f : (a : ℍ) → ℂ) k

Tactic:
apply CuspFormClass.zero_at_cusps f

Premises used: CuspFormClass.zero_at_cusps
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
⊢ IsCusp (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞) Γ

Tactic:
simpa [mul_smul, hγ] using hc.smul g

Premises used: SemigroupAction.mul_smul, IsCusp.smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : CuspFormClass F Γ k
g : SL(2, ℤ)
⊢ Eq (α := (a : ℍ) → ℂ)
    (⇑(translate f ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))) :
      (a : ℍ) → ℂ)
    (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ?m.1
F : Sort ?u.242482
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
⊢ IsCusp ∞ Γ

Tactic:
simpa [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff]
    using ⟨_, OnePoint.map_infty _⟩

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : ModularFormClass F Γ k
inst_2 : Fact (IsCusp ∞ Γ)
⊢ IsBoundedAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)

Tactic:
isBoundedAt_infty_iff.mp <| bdd_at_cusps f Fact.out

Premises used: OnePoint.isBoundedAt_infty_iff, Iff.mp, ModularFormClass.bdd_at_cusps, Fact.out
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : CuspFormClass F Γ k
inst_2 : Fact (IsCusp ∞ Γ)
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)

Tactic:
isZeroAt_infty_iff.mp <| zero_at_cusps f Fact.out

Premises used: CuspFormClass.zero_at_cusps, OnePoint.isZeroAt_infty_iff, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
rw :
  (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞).IsBoundedAt
    (⇑f : (a : ℍ) → ℂ) k
⊢ IsBoundedAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))

Tactic:
rw [← OnePoint.isBoundedAt_infty_iff, SL_slash, ← OnePoint.IsBoundedAt.smul_iff]

Premises used: ModularForm.SL_slash, OnePoint.isBoundedAt_infty_iff, OnePoint.IsBoundedAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
apply :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞)
    Γ
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞).IsBoundedAt
    (⇑f : (a : ℍ) → ℂ) k

Tactic:
apply bdd_at_cusps f

Premises used: ModularFormClass.bdd_at_cusps
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
rw :
  ∃ (g_1 : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞ =
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞
⊢ IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞)
    Γ

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
simp [mapGL]

Premises used: Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : ModularFormClass F Γ k
⊢ ∃ (g_1 : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞ =
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞

Tactic:
exact ⟨g, by simp [mapGL]⟩
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
rw :
  (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞).IsZeroAt
    (⇑f : (a : ℍ) → ℂ) k
⊢ IsZeroAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ))

Tactic:
rw [← OnePoint.isZeroAt_infty_iff, SL_slash, ← OnePoint.IsZeroAt.smul_iff]

Premises used: ModularForm.SL_slash, OnePoint.isZeroAt_infty_iff, OnePoint.IsZeroAt.smul_iff
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
apply :
  IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞)
    Γ
⊢ (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞).IsZeroAt
    (⇑f : (a : ℍ) → ℂ) k

Tactic:
apply zero_at_cusps f

Premises used: CuspFormClass.zero_at_cusps
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
rw :
  ∃ (g_1 : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞ =
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞
⊢ IsCusp
    (HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞)
    Γ

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) : GL (Fin 2) ℝ)
      ∞ =
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) ∞

Tactic:
simp [mapGL]

Premises used: Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
f : F
inst_1 : Γ.IsArithmetic
g : SL(2, ℤ)
inst_2 : CuspFormClass F Γ k
⊢ ∃ (g_1 : SL(2, ℤ)),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) ((map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
          GL (Fin 2) ℝ)
        ∞ =
      HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g_1 : GL (Fin 2) ℝ) ∞

Tactic:
exact ⟨g, by simp [mapGL]⟩
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : IsZeroAtImInfty f
rw :
  ∀ (hf : Tendsto (β := ℝ) (fun (x : ℍ) ↦ ‖f x‖) atImInfty (nhds 0)),
    Tendsto (β := ℝ)
      (fun (x : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖)
      atImInfty (nhds 0)
⊢ IsZeroAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)

Tactic:
rw [IsZeroAtImInfty, ZeroAtFilter, tendsto_zero_iff_norm_tendsto_zero] at hf ⊢

Premises used: Filter.ZeroAtFilter, tendsto_zero_iff_norm_tendsto_zero, UpperHalfPlane.IsZeroAtImInfty
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : Tendsto (β := ℝ) (fun (x : ℍ) ↦ ‖f x‖) atImInfty (nhds 0)
⊢ Tendsto (β := ℝ)
    (fun (x : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖) atImInfty
    (nhds 0)

Tactic:
simpa [ModularForm.slash_def, denom, hg, mul_assoc]
    using (hf.comp <| tendsto_smul_atImInfty hg).mul_const _

Premises used: UpperHalfPlane.tendsto_smul_atImInfty, mul_assoc, Filter.Tendsto.mul_const, UpperHalfPlane.denom, ModularForm.slash_def, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : IsBoundedAtImInfty f
rw :
  ∀ (hf : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖f x‖) 1),
    Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty
      (fun (x : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖) 1
⊢ IsBoundedAtImInfty (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)

Tactic:
rw [IsBoundedAtImInfty, BoundedAtFilter, ← Asymptotics.isBigO_norm_left] at hf ⊢

Premises used: UpperHalfPlane.IsBoundedAtImInfty, Filter.BoundedAtFilter, Asymptotics.isBigO_norm_left
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖f x‖) 1
this :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦
      ‖HPow.hPow (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) (k - 1)‖ *
          ‖(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ^ (-k)‖ *
        ‖f (g • x)‖)
    1
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖) 1

Tactic:
simpa [ModularForm.slash_def, denom, hg, mul_assoc, mul_comm ‖f _‖]

Premises used: Norm.norm, mul_assoc, UpperHalfPlane.denom, mul_comm, ModularForm.slash_def
-- Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp
Goal:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hf : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty (fun (x : ℍ) ↦ ‖f x‖) 1
suffices :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦
      ‖HPow.hPow (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) (k - 1)‖ *
          ‖(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ^ (-k)‖ *
        ‖f (g • x)‖)
    1
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atImInfty
    (fun (x : ℍ) ↦ ‖@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f x‖) 1

Tactic:
suffices (fun x ↦ (‖g.det.val ^ (k - 1)‖ * ‖g 1 1 ^ (-k)‖) * ‖f (g • x)‖) =O[atImInfty] 1 by
    simpa [ModularForm.slash_def, denom, hg, mul_assoc, mul_comm ‖f _‖]