awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
z : ℍ
⊢ (f - g : (a : ℍ) → ℂ) z = HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((g : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k k_1 k_2 : ℤ
inst : Γ.HasDetPlusMinusOne
f : ModularForm Γ k_1
g : ModularForm Γ k_2
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k_1 + k_2) γ
      (f.mul g.toSlashInvariantForm).toFun)

Tactic:
simpa [mul_slash] using ((f.bdd_at_cusps' hc γ hγ).mul (g.bdd_at_cusps' hc γ hγ)).smul _

Premises used: ModularForm.mul_slash, Filter.BoundedAtFilter.mul, Filter.BoundedAtFilter.smul, ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
x : ℂ
inst : Γ.HasDetOne
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
⊢ IsBoundedAtImInfty
    (@SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g
      (toFun (Γ := Γ) (SlashInvariantForm.const x)))

Tactic:
simpa only [coe_const, slash_def, SlashInvariantForm.toFun_eq_coe,
      Function.const_apply, neg_zero, zpow_zero] using atImInfty.const_boundedAtFilter _

Premises used: Function.const_apply, zpow_zero, UpperHalfPlane.atImInfty, Filter.const_boundedAtFilter, SlashInvariantForm.toFun_eq_coe, ModularForm.coe_const, ModularForm.slash_def, neg_zero
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetOne
x : ℂ
τ : ℍ
⊢ (const x : (a : ℍ) → ℂ) τ = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
x : ℝ
inst : Γ.HasDetPlusMinusOne
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
⊢ IsBoundedAtImInfty
    (@SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g
      (toFun (Γ := Γ) (SlashInvariantForm.constℝ x)))

Tactic:
simpa only [coe_constℝ, slash_def, SlashInvariantForm.toFun_eq_coe,
      Function.const_apply, neg_zero, zpow_zero] using atImInfty.const_boundedAtFilter _

Premises used: Function.const_apply, ModularForm.coe_constℝ, zpow_zero, UpperHalfPlane.atImInfty, Filter.const_boundedAtFilter, SlashInvariantForm.toFun_eq_coe, ModularForm.slash_def, neg_zero
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
x : ℝ
τ : ℍ
⊢ (constℝ x : (a : ℍ) → ℂ) τ = (↑x : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
⊢ Eq (α := (a : ℍ) → ℂ) (⇑1 : (a : ℍ) → ℂ) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
n : ℕ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(↑n : ModularForm Γ 0) : (a : ℍ) → ℂ) (↑n : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
n : ℕ
⊢ Eq (α := SlashInvariantForm Γ 0) (toSlashInvariantForm (↑n : ModularForm Γ 0)) (↑n : SlashInvariantForm Γ 0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
z : ℤ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(↑z : ModularForm Γ 0) : (a : ℍ) → ℂ) (↑z : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
z : ℤ
⊢ Eq (α := SlashInvariantForm Γ 0) (toSlashInvariantForm (↑z : ModularForm Γ 0)) (↑z : SlashInvariantForm Γ 0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
c : OnePoint ℝ
A : IsCusp c Γ
⊢ c.IsZeroAt
    ({ toFun := (⇑f : (a : ℍ) → ℂ), slash_action_eq' := ⋯ : SlashInvariantForm Γ k } +
        { toFun := (⇑g : (a : ℍ) → ℂ), slash_action_eq' := ⋯ : SlashInvariantForm Γ k }).toFun
    k

Tactic:
simpa using (f.zero_at_cusps' A).add (g.zero_at_cusps' A)

Premises used: OnePoint.IsZeroAt.add, CuspForm.zero_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
⊢ (⇑(f + g) : (a : ℍ) → ℂ) = HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
z : ℍ
⊢ (f + g : (a : ℍ) → ℂ) z = HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((g : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g
      (SlashInvariantForm.toFun (Γ := Γ) (k := k) 0))

Tactic:
simpa using Filter.zero_zeroAtFilter _

Premises used: Filter.zero_zeroAtFilter
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
a : α
y z : ℂ
⊢ (a • y) • z = a • y • z

Tactic:
simpa using smul_assoc (a • (1 : ℝ)) y z

Premises used: smul_assoc, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
⊢ MDiff (⇑(c • f.toSlashInvariantForm) : (a : ℍ) → ℂ)

Tactic:
simpa using f.holo'.const_smul (c • (1 : ℂ))

Premises used: MDifferentiable.const_smul, CuspForm.holo', HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
simp_rw :
  Filter.Tendsto
    (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    atImInfty (𝓝 0)
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g
      (c • f.toSlashInvariantForm).toFun)

Tactic:
simp_rw [IsZeroAtImInfty, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe,
        SlashInvariantForm.coe_smulℝ, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]

Premises used: ModularForm.smul_slash, SlashInvariantForm.coe_smulℝ, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe, smul_one_smul, UpperHalfPlane.IsZeroAtImInfty, Complex, DFunLike.coe, CuspForm.toSlashInvariantForm_coe
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ Filter.Tendsto
    (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    atImInfty (𝓝 0)

Tactic:
(f.zero_at_cusps' hc g hg).smul _

Premises used: Filter.ZeroAtFilter, CuspForm.zero_at_cusps', Filter.ZeroAtFilter.smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ Filter.Tendsto
    (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    atImInfty (𝓝 0)

Tactic:
exact (f.zero_at_cusps' hc g hg).smul _

Premises used: CuspForm.zero_at_cusps', Filter.ZeroAtFilter.smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
f : CuspForm Γ k
n : α
⊢ (⇑(n • f) : (a : ℍ) → ℂ) = HSMul.hSMul (β := (a : ℍ) → ℂ) n (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
f : CuspForm Γ k
n : α
z : ℍ
⊢ (n • f : (a : ℍ) → ℂ) z = HSMul.hSMul (β := ℂ) n ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
c : α
f : CuspForm Γ k
⊢ MDiff (⇑(c • f.toSlashInvariantForm) : (a : ℍ) → ℂ)

Tactic:
simpa using f.holo'.const_smul (c • (1 : ℂ))

Premises used: MDifferentiable.const_smul, CuspForm.holo', HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
simp_rw :
  Filter.Tendsto
    (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    atImInfty (𝓝 0)
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g
      (c • f.toSlashInvariantForm).toFun)

Tactic:
simp_rw [IsZeroAtImInfty, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe,
        SlashInvariantForm.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f,
        smul_slash]

Premises used: ModularForm.smul_slash, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe, smul_one_smul, UpperHalfPlane.IsZeroAtImInfty, Complex, SlashInvariantForm.coe_smul, DFunLike.coe, CuspForm.toSlashInvariantForm_coe
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ Filter.Tendsto
    (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    atImInfty (𝓝 0)

Tactic:
(f.zero_at_cusps' hc g hg).smul _

Premises used: Filter.ZeroAtFilter, CuspForm.zero_at_cusps', Filter.ZeroAtFilter.smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ Filter.Tendsto
    (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    atImInfty (𝓝 0)

Tactic:
exact (f.zero_at_cusps' hc g hg).smul _

Premises used: CuspForm.zero_at_cusps', Filter.ZeroAtFilter.smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
f : CuspForm Γ k
n : α
⊢ (⇑(n • f) : (a : ℍ) → ℂ) = HSMul.hSMul (β := (a : ℍ) → ℂ) n (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
f : CuspForm Γ k
n : α
z : ℍ
⊢ (n • f : (a : ℍ) → ℂ) z = HSMul.hSMul (β := ℂ) n ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : CuspForm Γ k
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g
      (-f.toSlashInvariantForm).toFun)

Tactic:
simpa using (f.zero_at_cusps' hc g hg).neg

Premises used: CuspForm.zero_at_cusps', Filter.ZeroAtFilter.neg
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : CuspForm Γ k
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(-f) : (a : ℍ) → ℂ) (-(⇑f : (a : ℍ) → ℂ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : CuspForm Γ k
z : ℍ
⊢ Eq (α := ℂ) ((-f : (a : ℍ) → ℂ) z : ℂ) (-(f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
⊢ (⇑(f - g) : (a : ℍ) → ℂ) = HSub.hSub (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
z : ℍ
⊢ (f - g : (a : ℍ) → ℂ) z = HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((g : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetPlusMinusOne
k₁ k₂ : ℤ
f : CuspForm Γ k₁
g : ModularForm Γ k₂
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k₁ + k₂) γ
      (f.mul g.toSlashInvariantForm).toFun)

Tactic:
simpa [mul_slash] using
      ((f.zero_at_cusps' hc γ hγ).mul_boundedAtFilter (g.bdd_at_cusps' hc γ hγ)).smul _

Premises used: ModularForm.mul_slash, Filter.ZeroAtFilter.mul_boundedAtFilter, CuspForm.zero_at_cusps', Filter.ZeroAtFilter.smul, ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
a b : ℤ
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
h : a = b
hΓ : Γ' = Γ
f : ModularForm Γ a
⊢ mcast h f hΓ = 0 ↔ f = 0

Tactic:
simp [← coe_eq_zero_iff, ← coe_eq_zero_iff (f := f)]

Premises used: ModularForm.coe_eq_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
a b : GradedMonoid (ModularForm Γ)
h : a.fst (β := ModularForm Γ) = b.fst (β := ModularForm Γ)
h2 : mcast h (a.snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)
obtain :
  ∀ (i : ℤ) (a : ModularForm Γ i)
    (h : (Sigma.mk (β := ModularForm Γ) i a).fst (β := ModularForm Γ) = b.fst (β := ModularForm Γ))
    (h2 : mcast h ((Sigma.mk (β := ModularForm Γ) i a).snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)),
    Sigma.mk (β := ModularForm Γ) i a = b
⊢ a = b

Tactic:
obtain ⟨i, a⟩ := a
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
i : ℤ
a : ModularForm Γ i
h : (Sigma.mk (β := ModularForm Γ) i a).fst (β := ModularForm Γ) = b.fst (β := ModularForm Γ)
h2 : mcast h ((Sigma.mk (β := ModularForm Γ) i a).snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)
refl :
  ∀ (a : ModularForm Γ b.1)
    (h2 : mcast ⋯ ((Sigma.mk (β := ModularForm Γ) b.1 a).snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)),
    Sigma.mk (β := ModularForm Γ) b.1 a = b
⊢ Sigma.mk (β := ModularForm Γ) i a = b

Tactic:
cases h
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
a : ModularForm Γ b.1
h2 : mcast ⋯ ((Sigma.mk (β := ModularForm Γ) b.1 a).snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)
⊢ Sigma.mk (β := ModularForm Γ) b.1 a = b

Tactic:
congr_arg _ h2

Premises used: congr_arg, GradedMonoid
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
a : ModularForm Γ b.1
h2 : mcast ⋯ ((Sigma.mk (β := ModularForm Γ) b.1 a).snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)
⊢ Sigma.mk (β := ModularForm Γ) b.1 a = b

Tactic:
exact congr_arg _ h2

Premises used: congr_arg
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ 0 = (↑Nat.zero : ℤ) * k

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n_1 n : ℕ
g : ModularForm Γ ((↑n : ℤ) * k)
⊢ (↑n : ℤ) * k + k = (↑n.succ : ℤ) * k

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ (⇑(f.pow 0) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (β := ℕ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
simp [pow]

Premises used: ModularForm.pow
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : (⇑(f.pow n) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n
⊢ (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)

Tactic:
simp_all only [pow, coe_mcast, coe_mul, pow_succ]

Premises used: ModularForm.coe_mul, ModularForm.pow, pow_succ, ModularForm.coe_mcast
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
zero : (⇑(f.pow 0) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (β := ℕ) (⇑f : (a : ℍ) → ℂ) 0
succ :
  ∀ (n : ℕ) (ih : (⇑(f.pow n) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n),
    (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)
⊢ (⇑(f.pow n) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n

Tactic:
induction n with
  | zero => simp [pow]
  | succ n ih => simp_all only [pow, coe_mcast, coe_mul, pow_succ]

Premises used: ModularForm.coe_mul, ModularForm.pow, pow_succ, ModularForm.coe_mcast
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ Sigma.mk (β := ModularForm Γ) (HSMul.hSMul (α := ℕ) 0 k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) 0 f) =
    Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)

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

Premises used: GradedMonoid.GMonoid.gnpow_zero', GradedMonoid, Sigma.mk, Eq.trans, GradedMonoid.mk
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
zero : 1 = Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)
⊢ Sigma.mk (β := ModularForm Γ) (HSMul.hSMul (α := ℕ) 0 k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) 0 f) =
    Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)

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

Premises used: GradedMonoid.GMonoid.gnpow_zero', Sigma.mk, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ 1 = Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)

Tactic:
gradedMonoid_eq_of_cast (zero_mul k).symm (ModularForm.ext fun _ ↦ rfl)

Premises used: MulZeroClass.zero_mul, ModularForm.gradedMonoid_eq_of_cast, ModularForm.ext, Eq.symm, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ 1 = Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)

Tactic:
exact gradedMonoid_eq_of_cast (zero_mul k).symm (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 : ℕ
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))

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

Premises used: GradedMonoid, GradedMonoid.GMonoid.gnpow_succ', Sigma.mk, Eq.trans, GradedMonoid.mk
-- 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)
succ :
  Sigma.mk (β := ModularForm Γ) (n • (Sigma.mk (β := ModularForm Γ) k f).fst (β := ModularForm Γ))
        (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n
          ((Sigma.mk (β := ModularForm Γ) k f).snd (β := ModularForm Γ))) *
      Sigma.mk (β := ModularForm Γ) k f =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
⊢ Sigma.mk (β := ModularForm Γ) ((n + 1) • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) (n + 1) f) =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))

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

Premises used: GradedMonoid.GMonoid.gnpow_succ', Sigma.mk, Eq.trans
-- 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 • (Sigma.mk (β := ModularForm Γ) k f).fst (β := ModularForm Γ))
        (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n
          ((Sigma.mk (β := ModularForm Γ) k f).snd (β := ModularForm Γ))) *
      Sigma.mk (β := ModularForm Γ) k f =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))

Tactic:
(congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_

Premises used: HMul.hMul, congrArg, Eq.trans
-- 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)
succ :
  Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n) * Sigma.mk (β := ModularForm Γ) k f =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
⊢ Sigma.mk (β := ModularForm Γ) (n • (Sigma.mk (β := ModularForm Γ) k f).fst (β := ModularForm Γ))
        (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n
          ((Sigma.mk (β := ModularForm Γ) k f).snd (β := ModularForm Γ))) *
      Sigma.mk (β := ModularForm Γ) k f =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))

Tactic:
refine (congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_

Premises used: HMul.hMul, congrArg, Eq.trans
-- 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)
⊢ (↑n : ℤ) * k + k = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k

Tactic:
ring