awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
⊢ (((discriminantEquiv :
              (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
            f :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
        (a : ℍ) → ℂ)
      z =
    HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ 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
z : ℍ
⊢ (f.divDiscriminant : (a : ℍ) → ℂ) z = HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ 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
z : ℍ
rw : Δ z * HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z) = (f : (a : ℍ) → ℂ) z
rw₁ rw₂ : Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ HMul.hMul (β := ℂ) (Δ z)
      ((((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                f :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
            (a : ℍ) → ℂ)
          z :
        ℂ) =
    (f : (a : ℍ) → ℂ) z

Tactic:
rw [CuspForm.discriminantEquiv_apply, mul_div_cancel₀ _ (discriminant_ne_zero z)]

Premises used: ModularForm.discriminant_ne_zero, mul_div_cancel₀, CuspForm.discriminantEquiv_apply
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ Δ *
      (⇑((CuspForm.discriminantEquiv :
                (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                  ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
              f :
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
        (a : ℍ) → ℂ) =
    (⇑f : (a : ℍ) → ℂ)

Tactic:
grind [Pi.mul_apply, discriminant_mul_discriminantEquiv_apply]

Premises used: Pi.mul_apply, ModularForm.discriminant_mul_discriminantEquiv_apply
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
⊢ (qExpansion 1 Δ).order = 1

Tactic:
PowerSeries.order_eq_nat.mpr
    ⟨discriminant_qExpansion_coeff_one ▸ one_ne_zero, fun i hi ↦ ?_⟩

Premises used: Iff.mpr, Eq.rec, ModularForm.discriminant_qExpansion_coeff_one, WithTop.some, And.intro, one_ne_zero, Eq.symm, PowerSeries.order_eq_nat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
refine :
  ∀ (i : ℕ) (hi : i < 1), Eq (α := ℂ) ((PowerSeries.coeff i : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (0 : ℂ)
⊢ (qExpansion 1 Δ).order = 1

Tactic:
refine PowerSeries.order_eq_nat.mpr
    ⟨discriminant_qExpansion_coeff_one ▸ one_ne_zero, fun i hi ↦ ?_⟩

Premises used: Iff.mpr, And.intro, PowerSeries.order_eq_nat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
i : ℕ
hi : i < 1
⊢ i = 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
i : ℕ
hi : i < 1
obtain :
  ∀ (hi : LT.lt (α := ℕ) 0 1),
    Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((PowerSeries.coeff i : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (0 : ℂ)

Tactic:
obtain rfl : i = 0 := by lia

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
hi : LT.lt (α := ℕ) 0 1
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (0 : ℂ)

Tactic:
simpa using CuspFormClass.qExpansion_coeff_zero CuspForm.discriminant one_pos
    one_mem_strictPeriods_SL

Premises used: CuspForm.discriminant, one_mem_strictPeriods_SL, CuspFormClass.qExpansion_coeff_zero, one_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hcusp : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
rw :
  qExpansion 1
      (HMul.hMul (α := (z : ℍ) → ℂ) (⇑CuspForm.discriminant : (a : ℍ) → ℂ)
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                (f.toCuspForm hcusp) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
          (a : ℍ) → ℂ)) =
    qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ) *
      qExpansion 1
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                (f.toCuspForm hcusp) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
          (a : ℍ) → ℂ)
⊢ qExpansion 1 (⇑f : (a : ℍ) → ℂ) =
    qExpansion 1 Δ *
      qExpansion 1
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                (f.toCuspForm hcusp) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
          (a : ℍ) → ℂ)

Tactic:
rw [show (f : ℍ → ℂ) = discriminant * (toCuspForm f hcusp).discriminantEquiv from
      (discriminant_mul_discriminantEquiv (toCuspForm f hcusp)).symm, ← CuspForm.coe_discriminant]

Premises used: ModularForm.discriminant_mul_discriminantEquiv, ModularForm.toCuspForm, Eq.symm, CuspForm.coe_discriminant
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hcusp : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
⊢ qExpansion 1
      (HMul.hMul (α := (z : ℍ) → ℂ) (⇑CuspForm.discriminant : (a : ℍ) → ℂ)
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                (f.toCuspForm hcusp) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
          (a : ℍ) → ℂ)) =
    qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ) *
      qExpansion 1
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                (f.toCuspForm hcusp) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
          (a : ℍ) → ℂ)

Tactic:
ModularForm.qExpansion_mul_coe one_pos one_mem_strictPeriods_SL _ _

Premises used: one_mem_strictPeriods_SL, ModularForm.qExpansion_mul_coe, one_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hcusp : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
⊢ qExpansion 1
      (HMul.hMul (α := (z : ℍ) → ℂ) (⇑CuspForm.discriminant : (a : ℍ) → ℂ)
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                (f.toCuspForm hcusp) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
          (a : ℍ) → ℂ)) =
    qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ) *
      qExpansion 1
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12))
                (f.toCuspForm hcusp) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)) :
          (a : ℍ) → ℂ)

Tactic:
exact ModularForm.qExpansion_mul_coe one_pos one_mem_strictPeriods_SL _ _

Premises used: one_mem_strictPeriods_SL, ModularForm.qExpansion_mul_coe, one_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk : Odd k
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
huv :
  ∀ (i j : Fin 2),
    Eq (α := ℝ)
      ((↑((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (-1)) : Matrix (Fin 2) (Fin 2) ℝ) i j)
      ((↑(-1) : Matrix (Fin 2) (Fin 2) ℝ) i j)
⊢ Eq (α := GL (Fin 2) ℝ) ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (-1)) (-1)

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk : Odd k
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
i j : Fin 2
⊢ Eq (α := ℝ)
    ((↑((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (-1)) : Matrix (Fin 2) (Fin 2) ℝ) i j)
    ((↑(-1) : Matrix (Fin 2) (Fin 2) ℝ) i j)

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

Tactic:
rank_zero_iff_forall_zero.mpr (levelOne_odd_weight_eq_zero hk)

Premises used: Iff.mpr, rank_zero_iff_forall_zero, ModularForm.levelOne_odd_weight_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk : k < 12
⊢ k - 12 < 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
⊢ Module.rank ℂ (CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) = 1

Tactic:
simpa [CuspForm.discriminantEquiv.rank_eq] using levelOne_weight_zero_rank_one

Premises used: ModularForm.levelOne_weight_zero_rank_one, LinearEquiv.rank_eq, CuspForm.discriminantEquiv
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
⊢ ∃ (c : ℂ), c • discriminant = f

Tactic:
(finrank_eq_one_iff_of_nonzero' _ (DFunLike.ne_iff.mpr ⟨I, discriminant_ne_zero _⟩)).mp
    (Module.rank_eq_one_iff_finrank_eq_one.mp CuspForm.rank_eq_one_of_weight_eq_twelve) f

Premises used: Iff.mpr, CuspForm.rank_eq_one_of_weight_eq_twelve, DFunLike.ne_iff, Module.rank_eq_one_iff_finrank_eq_one, Exists.intro, Iff.mp, UpperHalfPlane.I, finrank_eq_one_iff_of_nonzero'
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
this :
  Module.rank ℂ
      (HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
        (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
        (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))) =
    1
rw :
  Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    1 +
      Module.rank ℂ ↥(cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
rw₁ :
  Module.rank ℂ
        (HasQuotient.Quotient
          (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (B :=
          Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
          (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))) +
      Module.rank ℂ
        ↥(cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    1 +
      Module.rank ℂ ↥(cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
rw₂ rw₃ :
  1 +
      Module.rank ℂ
        ↥(cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    1 +
      Module.rank ℂ ↥(cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    1 + Module.rank ℂ (CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))

Tactic:
rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]

Premises used: MonoidHom.range, Real, Submodule.rank_quotient_add_rank, Nat.cast, ModularForm.cuspFormSubmodule, LinearEquiv.rank_eq, ModularForm.CuspForm.equivCuspFormSubmodule, Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
suffices :
  Module.rank ℂ
      (HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
        (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
        (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))) =
    1
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    1 + Module.rank ℂ (CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))

Tactic:
suffices Module.rank ℂ (ModularForm 𝒮ℒ k ⧸ cuspFormSubmodule 𝒮ℒ k) = 1 by
    rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
n :
  Ne (α :=
    HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
      (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
      (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (Submodule.Quotient.mk (E hk)) 0
h :
  ∀
    (w :
      HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
        (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
        (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))),
    ∃ (c : ℂ),
      HSMul.hSMul (β :=
          HasQuotient.Quotient
            (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (B :=
            Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
            (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
          c (Submodule.Quotient.mk (E hk)) =
        w
⊢ Module.rank ℂ
      (HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
        (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
        (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))) =
    1

Tactic:
apply rank_eq_one (Submodule.Quotient.mk (E hk))

Premises used: rank_eq_one, Submodule.Quotient.mk, ModularForm.E
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h :
  Eq (α :=
    HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
      (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
      (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (Submodule.Quotient.mk (E hk)) 0
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)

Tactic:
have hE := E_qExpansion_coeff_zero hk hk2
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h :
  Eq (α :=
    HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
      (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
      (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (Submodule.Quotient.mk (E hk)) 0
hE : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)
⊢ Membership.mem (γ :=
    Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (E hk)

Tactic:
rw [Submodule.Quotient.mk_eq_zero] at h

Premises used: Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h :
  Eq (α :=
    HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
      (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
      (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (Submodule.Quotient.mk (E hk)) 0
hE : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)
h₁ :
  Membership.mem (γ :=
    Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (E hk)
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)

Tactic:
rw [Submodule.Quotient.mk_eq_zero] at h

Premises used: Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h :
  Membership.mem (γ :=
    Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (E hk)
hE : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)
⊢ False

Tactic:
one_ne_zero <| hE.symm.trans <| (isCuspForm_iff_coeffZero_eq_zero _).mp h

Premises used: ModularForm.isCuspForm_iff_coeffZero_eq_zero, Iff.mp, one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h :
  Membership.mem (γ :=
    Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
    (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (E hk)
hE : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)
⊢ False

Tactic:
exact one_ne_zero <| hE.symm.trans <| (isCuspForm_iff_coeffZero_eq_zero _).mp h

Premises used: ModularForm.isCuspForm_iff_coeffZero_eq_zero, Iff.mp, one_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
        (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
        (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))),
    ∃ (c : ℂ),
      HSMul.hSMul (β :=
          HasQuotient.Quotient
            (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (B :=
            Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
            (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
          c (Submodule.Quotient.mk (E hk)) =
        w

Tactic:
(Submodule.Quotient.forall _).mpr fun f ↦ ⟨(qExpansion 1 f).coeff 0, ?_⟩

Premises used: Iff.mpr, UpperHalfPlane.qExpansion, Submodule.Quotient.forall, PowerSeries.coeff, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
h :
  ∀ (f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)),
    HSMul.hSMul (α := ℂ) (β :=
        HasQuotient.Quotient
          (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (B :=
          Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
          (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
        ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ)
        (Submodule.Quotient.mk (E hk)) =
      Submodule.Quotient.mk f
⊢ ∀
    (w :
      HasQuotient.Quotient (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))
        (B := Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
        (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ))),
    ∃ (c : ℂ),
      HSMul.hSMul (β :=
          HasQuotient.Quotient
            (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) (B :=
            Submodule ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
            (cuspFormSubmodule (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)))
          c (Submodule.Quotient.mk (E hk)) =
        w

Tactic:
refine (Submodule.Quotient.forall _).mpr fun f ↦ ⟨(qExpansion 1 f).coeff 0, ?_⟩

Premises used: Iff.mpr, Submodule.Quotient.forall