awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
c : ℂ
a : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ { 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) }
have h : ∀ (z : ℍ),
  Eq (α := ℂ)
    (({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((c • a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := sorry,
            holo' := sorry, bdd_at_cusps' := sorry } :
          (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' := sorry,
              holo' := sorry, bdd_at_cusps' := sorry :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) } :
          (a : ℍ) → ℂ)
        z :
      ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
c : ℂ
a : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
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 :
      ℂ)
have h : HMul.hMul (β := ℂ) c ((a : (a : ℍ) → ℂ) z : ℂ) / Δ z = c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z)
Tactic: change (c * a z) / Δ z = c * (a z / Δ z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
c : ℂ
a : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
⊢ HMul.hMul (β := ℂ) c ((a : (a : ℍ) → ℂ) z : ℂ) / Δ z = c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z)
have h : c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) = c * HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z)
Tactic: rw [mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ 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
have 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' := sorry,
                    holo' := sorry, bdd_at_cusps' := sorry } :
                  ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
              f) :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)
⊢ (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
have 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' := sorry,
                  holo' := sorry, bdd_at_cusps' := sorry } :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12)))
            (ofMulDiscriminant f) :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
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
have rw : Δ z * HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z) = (f : (a : ℍ) → ℂ) z
Tactic: rw [CuspForm.discriminantEquiv_apply, mul_div_cancel₀ _ (discriminant_ne_zero z)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ 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
have rw₁ : Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: rw [CuspForm.discriminantEquiv_apply, mul_div_cancel₀ _ (discriminant_ne_zero z)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
⊢ (qExpansion 1 Δ).order = 1
have refine : ∀ (i : ℕ) (hi : i < 1), Eq (α := ℂ) ((PowerSeries.coeff i : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (0 : ℂ)
Tactic: refine PowerSeries.order_eq_nat.mpr
    ⟨discriminant_qExpansion_coeff_one ▸ one_ne_zero, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
i : ℕ
hi : i < 1
⊢ Eq (α := ℂ) ((PowerSeries.coeff i : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (0 : ℂ)
have obtain : ∀ (hi : LT.lt (α := ℕ) 0 1), Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 Δ) : ℂ) (0 : ℂ)
Tactic: obtain rfl : i = 0 := by lia
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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 (⇑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 : ℍ) → ℂ)
have 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 : ℍ) → ℂ)
Tactic: rw [show (f : ℍ → ℂ) = discriminant * (toCuspForm f hcusp).discriminantEquiv from
      (discriminant_mul_discriminantEquiv (toCuspForm f hcusp)).symm, ← CuspForm.coe_discriminant]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
hk : Odd k
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ Eq (α := GL (Fin 2) ℝ) ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (-1)) (-1)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ 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 : ℤ))
have 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 : ℤ))
Tactic: rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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 : ℤ))
⊢ 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 : ℤ))
have 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 : ℤ))
Tactic: rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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 : ℤ))
⊢ 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 : ℤ))
have 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 : ℤ))
Tactic: rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even 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 : ℤ))
have 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
Tactic: suffices Module.rank ℂ (ModularForm 𝒮ℒ k ⧸ cuspFormSubmodule 𝒮ℒ k) = 1 by
    rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ 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
have 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
Tactic: apply rank_eq_one (Submodule.Quotient.mk (E hk))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ 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
have 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
Tactic: apply rank_eq_one (Submodule.Quotient.mk (E hk))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
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
⊢ False
have hE : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) : ℂ) (1 : ℂ)
Tactic: have hE := E_qExpansion_coeff_zero hk hk2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
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 : ℂ)
⊢ False
have 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)
Tactic: rw [Submodule.Quotient.mk_eq_zero] at h
Cleared hypotheses: h, hE
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
have 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
Tactic: refine (Submodule.Quotient.forall _).mpr fun f ↦ ⟨(qExpansion 1 f).coeff 0, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
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
have h : LT.lt (α := ℝ) 0 1
Tactic: rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.eq, mem_cuspFormSubmodule_iff,
      isCuspForm_iff_coeffZero_eq_zero, ModularForm.coe_sub, ModularForm.qExpansion_sub,
      IsGLPos.coe_smul, ModularForm.qExpansion_smul, map_sub,
      PowerSeries.coeff_smul, E_qExpansion_coeff_zero hk hk2, smul_eq_mul, mul_one, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : LT.lt (α := ℝ) 0 1
⊢ 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
have h₁ : 1 ∈ Subgroup.strictPeriods (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
Tactic: rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.eq, mem_cuspFormSubmodule_iff,
      isCuspForm_iff_coeffZero_eq_zero, ModularForm.coe_sub, ModularForm.qExpansion_sub,
      IsGLPos.coe_smul, ModularForm.qExpansion_smul, map_sub,
      PowerSeries.coeff_smul, E_qExpansion_coeff_zero hk hk2, smul_eq_mul, mul_one, sub_self]