awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : ModularForm Γ k
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
bdd_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
    ((fun (f : ModularForm Γ k) ↦ f.toFun) g)
mk :
  ∀ (toSlashInvariantForm_1 : SlashInvariantForm Γ k) (holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ))
    (bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm_1.toFun k)
    (h :
      Eq (α := (a : ℍ) → ℂ)
        ((fun (f : ModularForm Γ k) ↦ f.toFun)
          { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
        ((fun (f : ModularForm Γ k) ↦ f.toFun)
          { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 })),
    { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' :
        ModularForm Γ k } =
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 }
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' : ModularForm Γ k } =
    g

Tactic:
cases g
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
bdd_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 })
mk : toSlashInvariantForm = toSlashInvariantForm_1
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' : ModularForm Γ k } =
    { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 }

Tactic:
congr
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
bdd_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 })
⊢ toSlashInvariantForm = toSlashInvariantForm_1

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
bdd_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 })
⊢ toSlashInvariantForm = toSlashInvariantForm_1

Tactic:
exact DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_2
inst : FunLike F ℍ ℂ
inst_1 : ModularFormClass F Γ k
f : F
⊢ Continuous (X := ℍ) (Y := ℂ) (⇑f : (a : ℍ) → ℂ)

Tactic:
(ModularFormClass.holo f).continuous

Premises used: MDifferentiable.continuous, ModularFormClass.holo
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
h : Eq (α := (a : ℍ) → ℂ) ((fun (f : CuspForm Γ k) ↦ f.toFun) f) ((fun (f : CuspForm Γ k) ↦ f.toFun) g)
mk :
  ∀ (toSlashInvariantForm : SlashInvariantForm Γ k) (holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ))
    (zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k)
    (h :
      Eq (α := (a : ℍ) → ℂ)
        ((fun (f : CuspForm Γ k) ↦ f.toFun)
          { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
        ((fun (f : CuspForm Γ k) ↦ f.toFun) g)),
    { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } =
      g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : CuspForm Γ k
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
    ((fun (f : CuspForm Γ k) ↦ f.toFun) g)
mk :
  ∀ (toSlashInvariantForm_1 : SlashInvariantForm Γ k) (holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ))
    (zero_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm_1.toFun k)
    (h :
      Eq (α := (a : ℍ) → ℂ)
        ((fun (f : CuspForm Γ k) ↦ f.toFun)
          { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
        ((fun (f : CuspForm Γ k) ↦ f.toFun)
          { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 })),
    { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } =
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 }
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } = g

Tactic:
cases g
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
zero_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 })
mk : toSlashInvariantForm = toSlashInvariantForm_1
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } =
    { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 }

Tactic:
congr
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
zero_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 })
⊢ toSlashInvariantForm = toSlashInvariantForm_1

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
zero_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 })
⊢ toSlashInvariantForm = toSlashInvariantForm_1

Tactic:
exact DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : ModularForm Γ k
⊢ f.toFun = (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
h : ∀ (x : ℍ), Eq (α := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) ((g : (a : ℍ) → ℂ) x : ℂ)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
h : ∀ (x : ℍ), Eq (α := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) ((g : (a : ℍ) → ℂ) x : ℂ)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
c : OnePoint ℝ
hc : IsCusp c Γ
⊢ c.IsBoundedAt
    ({ toFun := (⇑f : (a : ℍ) → ℂ), slash_action_eq' := ⋯ : SlashInvariantForm Γ k } +
        { toFun := (⇑g : (a : ℍ) → ℂ), slash_action_eq' := ⋯ : SlashInvariantForm Γ k }).toFun
    k

Tactic:
simpa using (f.bdd_at_cusps' hc).add (g.bdd_at_cusps' hc)

Premises used: OnePoint.IsBoundedAt.add, ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ 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 : ModularForm Γ 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:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
simp : IsBoundedAtImInfty (α := ℂ) 0
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (toFun (Γ := Γ) (k := k) 0))

Tactic:
simp only [SlashInvariantForm.toFun_eq_coe, coe_zero, SlashAction.zero_slash]

Premises used: SlashAction.zero_slash, SlashInvariantForm.toFun_eq_coe, SlashInvariantForm.coe_zero
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
⊢ IsBoundedAtImInfty (α := ℂ) 0

Tactic:
zero_form_isBoundedAtImInfty

Premises used: UpperHalfPlane.zero_form_isBoundedAtImInfty
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
⊢ IsBoundedAtImInfty (α := ℂ) 0

Tactic:
exact zero_form_isBoundedAtImInfty

Premises used: UpperHalfPlane.zero_form_isBoundedAtImInfty
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑0 : (a : ℍ) → ℂ) 0

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : ModularForm Γ k
rw : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑0 : (a : ℍ) → ℂ) ↔ f = 0
rw₁ : Subgroup (GL (Fin 2) ℝ)
rw₂ : ℤ
rw₃ rw₄ : f = 0 ↔ f = 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0 ↔ f = 0

Tactic:
rw [← coe_zero, DFunLike.coe_fn_eq]

Premises used: DFunLike.coe_fn_eq, ModularForm.coe_zero
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
h : ∀ (z : ℍ), Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((0 : (a : ℍ) → ℂ) z : ℂ)
⊢ f = 0

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
⊢ (f : (a : ℍ) → ℂ) (HSMul.hSMul (α := GL (Fin 2) ℝ) (-1) z) =
    HMul.hMul (β := ℂ) (denom (-1) (↑z : ℂ) ^ k) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
have hf := slash_action_eqn'' f h_neg_one z
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf :
  (f : (a : ℍ) → ℂ) (HSMul.hSMul (α := GL (Fin 2) ℝ) (-1) z) =
    HMul.hMul (β := ℂ) (denom (-1) (↑z : ℂ) ^ k) ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ (f : (a : ℍ) → ℂ) z = HMul.hMul (α := ℂ) (β := ℂ) (-1 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rw [neg_smul, one_smul, denom_neg, denom_one, hk.neg_one_zpow] at hf

Premises used: Odd.neg_one_zpow, one_smul, UpperHalfPlane.denom_neg, UpperHalfPlane.denom_one, UpperHalfPlane.neg_smul
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : (f : (a : ℍ) → ℂ) z = HMul.hMul (α := ℂ) (β := ℂ) (-1 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ HMul.hMul (α := ℂ) (β := ℂ) (2 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) = 0

Tactic:
linear_combination hf
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : (f : (a : ℍ) → ℂ) z = HMul.hMul (α := ℂ) (β := ℂ) (-1 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ HMul.hMul (α := ℂ) (β := ℂ) (2 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) = 0

Tactic:
have h2 : (2 : ℂ) * f z = 0 := by linear_combination hf
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : (f : (a : ℍ) → ℂ) z = HMul.hMul (α := ℂ) (β := ℂ) (-1 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
h2 : HMul.hMul (α := ℂ) (β := ℂ) (2 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) = 0
⊢ ¬Eq (α := ℂ) 2 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : (f : (a : ℍ) → ℂ) z = HMul.hMul (α := ℂ) (β := ℂ) (-1 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
h2 : HMul.hMul (α := ℂ) (β := ℂ) (2 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) = 0
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((0 : (a : ℍ) → ℂ) z : ℂ)

Tactic:
exact (mul_eq_zero.mp h2).resolve_left (by norm_num)

Premises used: Or.resolve_left, mul_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
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:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
c : α
f : ModularForm Γ k
⊢ MDiff (⇑(c • f.toSlashInvariantForm) : (a : ℍ) → ℂ)

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

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

Tactic:
simpa only [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
        SlashInvariantForm.coe_smulℝ, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]
        using (f.bdd_at_cusps' hc g hg).const_smul_left _

Premises used: ModularForm.smul_slash, UpperHalfPlane.IsBoundedAtImInfty, SlashInvariantForm.coe_smulℝ, Asymptotics.IsBigO.const_smul_left, ModularForm.toSlashInvariantForm_coe, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe, smul_one_smul, Complex, DFunLike.coe, ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
f : ModularForm Γ 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_1
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
f : ModularForm Γ k
n : α
z : ℍ
⊢ (n • f : (a : ℍ) → ℂ) z = HSMul.hSMul (β := ℂ) n ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

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

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

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

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

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

Tactic:
(f.bdd_at_cusps' hc g hg).const_smul_left (σ g (c • (1 : ℂ)))

Premises used: Asymptotics.IsBigO.const_smul_left, HSMul.hSMul, UpperHalfPlane.σ, OfNat.ofNat, DFunLike.coe, ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
c : α
f : ModularForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ Asymptotics.IsBigO (F := ℝ) atImInfty
    (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
    1

Tactic:
exact (f.bdd_at_cusps' hc g hg).const_smul_left (σ g (c • (1 : ℂ)))

Premises used: Asymptotics.IsBigO.const_smul_left, HSMul.hSMul, UpperHalfPlane.σ, OfNat.ofNat, DFunLike.coe, ModularForm.bdd_at_cusps'
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
f : ModularForm Γ 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_1
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
f : ModularForm Γ k
n : α
z : ℍ
⊢ (n • f : (a : ℍ) → ℂ) z = HSMul.hSMul (β := ℂ) n ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : ModularForm Γ k
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 : ℍ) ↦ ℂ)) _ k g
      (-f.toSlashInvariantForm).toFun)

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

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Basic
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : ModularForm Γ 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 : ModularForm Γ k
⊢ (⇑(f - g) : (a : ℍ) → ℂ) = HSub.hSub (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl