awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
f : F
⊢ ∃ (c : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c

Tactic:
⟨_, levelOne_nonpos_wt_const le_rfl f⟩

Premises used: le_rfl, _private.0.ModularFormClass.levelOne_nonpos_wt_const, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
⊢ Ne (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) (const 1) 0

Tactic:
simp [DFunLike.ne_iff]

Premises used: DFunLike.ne_iff
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
refine :
  ∀ (g : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0),
    ∃ (c : ℂ),
      HSMul.hSMul (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) c
          (const 1) =
        g
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) = 1

Tactic:
refine rank_eq_one (const 1) (by simp [DFunLike.ne_iff]) fun g ↦ ?_

Premises used: ModularForm.const, rank_eq_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
g : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
obtain :
  ∀ (c' : ℂ) (hc' : (⇑g : (a : ℍ) → ℂ) = Function.const ℍ c'),
    ∃ (c : ℂ),
      HSMul.hSMul (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) c
          (const 1) =
        g
⊢ ∃ (c : ℂ),
    HSMul.hSMul (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) c (const 1) =
      g

Tactic:
obtain ⟨c', hc'⟩ := levelOne_weight_zero_const g

Premises used: ModularFormClass.levelOne_weight_zero_const
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
g : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
c' : ℂ
hc' : (⇑g : (a : ℍ) → ℂ) = Function.const ℍ c'
⊢ ∃ (c : ℂ),
    HSMul.hSMul (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) c (const 1) =
      g

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
k : ℤ
hk : k < 0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) = 0

Tactic:
rank_eq_zero_iff.mpr fun f ↦ ⟨_, one_ne_zero, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, rank_eq_zero_iff, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
k : ℤ
hk : k < 0
refine :
  ∀ (f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k),
    HSMul.hSMul (α := ℂ) 1 f = 0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) = 0

Tactic:
refine rank_eq_zero_iff.mpr fun f ↦ ⟨_, one_ne_zero, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, rank_eq_zero_iff, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
k : ℤ
hk : k < 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ HSMul.hSMul (α := ℂ) 1 f = 0

Tactic:
simpa [← coe_eq_zero_iff] using levelOne_neg_weight_eq_zero hk f

Premises used: ModularFormClass.levelOne_neg_weight_eq_zero, ModularForm.coe_eq_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)
⊢ 12 + (k - 12) = k

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)
z : ℍ
⊢ (ofMulDiscriminant f : (a : ℍ) → ℂ) z = HMul.hMul (β := ℂ) (Δ z) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
γ : SL(2, ℤ)
⊢ Membership.mem (α := GL (Fin 2) ℝ) (γ := Subgroup (GL (Fin 2) ℝ))
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
      GL (Fin 2) ℝ)

Tactic:
have hγ : (γ : GL (Fin 2) ℝ) ∈ 𝒮ℒ := ⟨γ, rfl⟩
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
γ : SL(2, ℤ)
hγ :
  Membership.mem (α := GL (Fin 2) ℝ) (γ := Subgroup (GL (Fin 2) ℝ))
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
      GL (Fin 2) ℝ)
simp_rw :
  HDiv.hDiv (α := ℍ → ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
        (⇑f : (a : ℍ) → ℂ))
      (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ
        (⇑discriminant : (a : ℍ) → ℂ)) =
    HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)
simp_rw₁ :
  HDiv.hDiv (α := ℍ → ℂ)
      (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
          GL (Fin 2) ℝ)
        (⇑f : (a : ℍ) → ℂ))
      (@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
          GL (Fin 2) ℝ)
        (⇑discriminant : (a : ℍ) → ℂ)) =
    HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
      (HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)) =
    HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)

Tactic:
simp_rw [div_slash_SL2, SL_slash, slash_action_eqn _ _ hγ]

Premises used: ModularForm.SL_slash, ModularForm.div_slash_SL2, SlashInvariantForm.slash_action_eqn
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
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.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
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 →
      IsBoundedAtImInfty (α := ℂ)
        (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
          fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z))
⊢ c.IsBoundedAt (fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z)) (k - 12)

Tactic:
rw [isBoundedAt_iff_forall_SL2Z hc]

Premises used: OnePoint.isBoundedAt_iff_forall_SL2Z
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
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 →
    IsBoundedAtImInfty (α := ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
        fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z))
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
      c →
    IsBoundedAtImInfty (α := ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
        fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z))

Tactic:
_
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
rw : IsBigO (E := ℂ) (F := ℝ) atImInfty (fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z)) 1
⊢ IsBoundedAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
      fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z))

Tactic:
rw [divByDiscriminant_slash_eq f γ, IsBoundedAtImInfty, BoundedAtFilter]

Premises used: UpperHalfPlane.IsBoundedAtImInfty, Filter.BoundedAtFilter, CuspForm.divByDiscriminant_slash_eq
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
⊢ IsBigO (E := ℂ) (F := ℝ) atImInfty (fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z)) 1

Tactic:
(div_isBoundedUnder_of_isBigO (exp_decay_isBigO_discriminant f)).isBigO_one ℝ

Premises used: Real, Asymptotics.div_isBoundedUnder_of_isBigO, Filter.IsBoundedUnder.isBigO_one, CuspForm.exp_decay_isBigO_discriminant
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
⊢ IsBigO (E := ℂ) (F := ℝ) atImInfty (fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z)) 1

Tactic:
exact (div_isBoundedUnder_of_isBigO (exp_decay_isBigO_discriminant f)).isBigO_one ℝ

Premises used: Real, Asymptotics.div_isBoundedUnder_of_isBigO, Filter.IsBoundedUnder.isBigO_one, CuspForm.exp_decay_isBigO_discriminant
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
a b : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h :
  ∀ (z : ℍ),
    Eq (α := ℂ)
      (({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a + b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ } :
            (a : ℍ) → ℂ)
          z :
        ℂ)
      ((HAdd.hAdd (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
              { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                holo' := ⋯, bdd_at_cusps' := ⋯ :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }
              { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                holo' := ⋯, bdd_at_cusps' := ⋯ :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) } :
            (a : ℍ) → ℂ)
          z :
        ℂ)
⊢ { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a + b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
      bdd_at_cusps' := ⋯ } =
    HAdd.hAdd (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
      { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
        bdd_at_cusps' := ⋯ :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }
      { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
        bdd_at_cusps' := ⋯ :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
a b : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
h :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) / Δ z =
    HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z)
⊢ Eq (α := ℂ)
    (({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a + b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
            holo' := ⋯, bdd_at_cusps' := ⋯ } :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((HAdd.hAdd (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
            { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }
            { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) } :
          (a : ℍ) → ℂ)
        z :
      ℂ)

Tactic:
change (a z + b z) / Δ z = a z / Δ z + b z / Δ z

Premises used: HAdd.hAdd, ModularForm.discriminant, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
a b : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
h h₁ :
  HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z) =
    HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z)
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) / Δ z =
    HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z)

Tactic:
rw [add_div]

Premises used: add_div
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
c : ℂ
a : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h :
  ∀ (z : ℍ),
    Eq (α := ℂ)
      (({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((c • a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ } :
            (a : ℍ) → ℂ)
          z :
        ℂ)
      ((HSMul.hSMul (α := ℂ) (β :=
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
              ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
              { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                holo' := ⋯, bdd_at_cusps' := ⋯ :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) } :
            (a : ℍ) → ℂ)
          z :
        ℂ)
⊢ { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((c • a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
      bdd_at_cusps' := ⋯ } =
    HSMul.hSMul (α := ℂ) (β :=
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
      ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
      { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
        bdd_at_cusps' := ⋯ :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
c : ℂ
a : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
h : HMul.hMul (β := ℂ) c ((a : (a : ℍ) → ℂ) z : ℂ) / Δ z = c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z)
⊢ Eq (α := ℂ)
    (({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((c • a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
            holo' := ⋯, bdd_at_cusps' := ⋯ } :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((HSMul.hSMul (α := ℂ) (β :=
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
            ((RingHom.id ℂ : (a : ℂ) → ℂ) c : ℂ)
            { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) } :
          (a : ℍ) → ℂ)
        z :
      ℂ)

Tactic:
change (c * a z) / Δ z = c * (a z / Δ z)

Premises used: HMul.hMul, HDiv.hDiv, ModularForm.discriminant, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
c : ℂ
a : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
h h₁ : c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) = c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z)
⊢ HMul.hMul (β := ℂ) c ((a : (a : ℍ) → ℂ) z : ℂ) / Δ z = c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z)

Tactic:
rw [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h :
  ∀ (z : ℍ),
    Eq (α := ℂ)
      ((ofMulDiscriminant
              ((fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
                  ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                      holo' := ⋯, bdd_at_cusps' := ⋯ } :
                    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
                f) :
            (a : ℍ) → ℂ)
          z :
        ℂ)
      ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ ofMulDiscriminant
      ((fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
          ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ } :
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
        f) =
    f

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
⊢ Eq (α := ℂ)
    ((ofMulDiscriminant
            ((fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
                ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                    holo' := ⋯, bdd_at_cusps' := ⋯ } :
                  ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
              f) :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
mul_div_cancel₀ (f z) (discriminant_ne_zero z)

Premises used: ModularForm.discriminant_ne_zero, mul_div_cancel₀, ModularForm.discriminant, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
⊢ Eq (α := ℂ)
    ((ofMulDiscriminant
            ((fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
                ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                    holo' := ⋯, bdd_at_cusps' := ⋯ } :
                  ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
              f) :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
exact mul_div_cancel₀ (f z) (discriminant_ne_zero z)

Premises used: ModularForm.discriminant_ne_zero, mul_div_cancel₀, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)
h :
  ∀ (z : ℍ),
    Eq (α := ℂ)
      (((fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
                ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                    holo' := ⋯, bdd_at_cusps' := ⋯ } :
                  ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
              (ofMulDiscriminant f) :
            (a : ℍ) → ℂ)
          z :
        ℂ)
      ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ (fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
        ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
            bdd_at_cusps' := ⋯ } :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
      (ofMulDiscriminant f) =
    f

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)
z : ℍ
⊢ Eq (α := ℂ)
    (((fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
              ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                  holo' := ⋯, bdd_at_cusps' := ⋯ } :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
            (ofMulDiscriminant f) :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
mul_div_cancel_left₀ (f z) (discriminant_ne_zero z)

Premises used: mul_div_cancel_left₀, ModularForm.discriminant_ne_zero, ModularForm.discriminant, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)
z : ℍ
⊢ Eq (α := ℂ)
    (((fun (f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) ↦
              ({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
                  holo' := ⋯, bdd_at_cusps' := ⋯ } :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
            (ofMulDiscriminant f) :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
exact mul_div_cancel_left₀ (f z) (discriminant_ne_zero z)

Premises used: mul_div_cancel_left₀, ModularForm.discriminant_ne_zero, DFunLike.coe