awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
⊢ Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0) :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    (0 :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
have h₁ : ∀ (hk12 : k < 12),
  Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0) :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    (0 :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
Tactic: rcases lt_or_ge k 12 with hk12 | hk12
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
h₁ :
  ∀ (hk12 : k < 12),
    Eq (α :=
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
      ((CuspForm.discriminantEquiv :
            (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
              ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
          (f.toCuspForm h0) :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
      (0 :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
⊢ Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0) :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    (0 :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
have h₂ : ∀ (hk12 : 12 ≤ k),
  Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0) :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    (0 :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
Tactic: rcases lt_or_ge k 12 with hk12 | hk12
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
hk12 : 12 ≤ k
⊢ Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0) :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
    (0 :
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
        (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
have h₁ : Eq (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑(k - 12) : ℤ))
  (mcast sorry
    ((CuspForm.discriminantEquiv :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
      (f.toCuspForm h0))
    sorry)
  0
Tactic: rw [← mcast_eq_zero_iff (b := ↑(k - 12)) (by lia) rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
hk12 : 12 ≤ k
⊢ Eq (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑(k - 12) : ℤ))
    (mcast ⋯
      ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0))
      ⋯)
    0
have h₁ : (↑((k - 12) / 12) : ℕ∞) <
  (qExpansion 1
      (⇑(mcast sorry
            ((CuspForm.discriminantEquiv :
                (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
                  ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
              (f.toCuspForm h0))
            sorry) :
        (a : ℍ) → ℂ)).order
Tactic: refine ih (k - 12) (by lia) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
hk12 : 12 ≤ k
⊢ (↑((k - 12) / 12) : ℕ∞) <
    (qExpansion 1
        (⇑(mcast ⋯
              ((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
                (f.toCuspForm h0))
              ⋯) :
          (a : ℍ) → ℂ)).order
have hsucc : k / 12 = (k - 12) / 12 + 1
Tactic: have hsucc : k / 12 = (k - 12) / 12 + 1 := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ (↑((k - 12) / 12) : ℕ∞) <
    (qExpansion 1
        (⇑(mcast ⋯
              ((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
                (f.toCuspForm h0))
              ⋯) :
          (a : ℍ) → ℂ)).order
have h₁ : HAdd.hAdd (α := ℕ∞) (↑((k - 12) / 12) : ℕ∞) 1 <
  (qExpansion 1
        (⇑((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
                (f.toCuspForm h0) :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                (HSub.hSub (α := ℤ) (↑k : ℤ) 12)) :
          (a : ℍ) → ℂ)).order +
    1
Tactic: rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h
Cleared hypotheses: h, hk12, hsucc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
⊢ f = 0
have h₁ : ∀ (k : ℕ)
  (ih :
    ∀ m < k,
      ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
        (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0)
  {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)}
  (h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
Tactic: induction k using Nat.strong_induction_on with | _ k ih =>
  have h0 : (qExpansion 1 f).coeff 0 = 0 :=
    PowerSeries.coeff_of_lt_order _ ((Nat.cast_nonneg _).trans_lt h)
  suffices CuspForm.discriminantEquiv (toCuspForm f h0) = 0 by
    simpa [CuspForm.discriminantEquiv.map_eq_zero_iff, DFunLike.ext_iff]
  rcases lt_or_ge k 12 with hk12 | hk12
  · apply rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero (by lia))
  · rw [← mcast_eq_zero_iff (b := ↑(k - 12)) (by lia) rfl]
    refine ih (k - 12) (by lia) ?_
    have hsucc : k / 12 = (k - 12) / 12 + 1 := by lia
    rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h
    exact (ENat.add_lt_add_iff_right (ENat.coe_ne_top 1)).mp h
Cleared hypotheses: k, f, h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : (↑(k.toNat / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
⊢ f = 0
have inl : ∀ (hk : k < 0), f = 0
Tactic: rcases lt_or_ge k 0 with hk | hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : (↑(k.toNat / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
inl : ∀ (hk : k < 0), f = 0
⊢ f = 0
have inr : ∀ (hk : 0 ≤ k), f = 0
Tactic: rcases lt_or_ge k 0 with hk | hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : (↑(k.toNat / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
hk : 0 ≤ k
⊢ f = 0
have inr : ∀ (k : ℕ) {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)}
  (h : (↑(Int.toNat (↑k : ℤ) / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
Tactic: lift k to ℕ using hk
Cleared hypotheses: k, f, h, hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
⊢ qExpansion 1 (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) =
    qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) -
      qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ)
have simp : HPow.hPow (β := ℕ) (qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ)) 3 - HPow.hPow (β := ℕ) (qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ)) 2 =
  qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) -
    qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ)
Tactic: simp only [E₄CubeSubE₆SqForm, coe_sub, coe_mcast,
    ModularForm.qExpansion_sub one_pos one_mem_strictPeriods_SL,
    ModularForm.qExpansion_pow one_pos one_mem_strictPeriods_SL]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
⊢ Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)) : ℂ)
    (1728 : ℂ)
have rw : Eq (α := ℂ)
  ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ)
      (qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) -
        qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) * qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ)) :
    ℂ)
  (1728 : ℂ)
Tactic: rw [E₄CubeSubE₆SqForm_qExpansion_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
z : ℍ
⊢ discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728
have obtain : ∀ (g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
  (hg :
    (CuspForm.toModularFormₗ :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
        g =
      E₄CubeSubE₆SqForm),
  discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728
Tactic: obtain ⟨g, hg⟩ := E₄CubeSubE₆SqForm_isCuspForm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
⊢ discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728
have obtain : ∀ (c : ℂ) (hc : c • CuspForm.discriminant = g),
  discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728
Tactic: obtain ⟨c, hc⟩ := CuspForm.exists_smul_discriminant_of_weight_eq_twelve g
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (hypothesis)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
⊢ discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728
have hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
Tactic: have hgE : (g : ℍ → ℂ) = E₄CubeSubE₆SqForm := congrArg DFunLike.coe hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (hypothesis)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
⊢ c = 1728
have hcΔ : HSMul.hSMul (β := (a : ℍ) → ℂ) c (⇑CuspForm.discriminant : (a : ℍ) → ℂ) = (⇑g : (a : ℍ) → ℂ)
Tactic: have hcΔ : (c • CuspForm.discriminant : ℍ → ℂ) = g := congrArg DFunLike.coe hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (hypothesis)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hcΔ : HSMul.hSMul (β := (a : ℍ) → ℂ) c (⇑CuspForm.discriminant : (a : ℍ) → ℂ) = (⇑g : (a : ℍ) → ℂ)
⊢ c = 1728
have hgΔ : qExpansion 1 (HSMul.hSMul (β := (a : ℍ) → ℂ) c (⇑CuspForm.discriminant : (a : ℍ) → ℂ)) =
  c • qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ)
Tactic: have hgΔ := ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c
      CuspForm.discriminant
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (hypothesis)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hcΔ : HSMul.hSMul (β := (a : ℍ) → ℂ) c (⇑CuspForm.discriminant : (a : ℍ) → ℂ) = (⇑g : (a : ℍ) → ℂ)
hgΔ :
  qExpansion 1 (HSMul.hSMul (β := (a : ℍ) → ℂ) c (⇑CuspForm.discriminant : (a : ℍ) → ℂ)) =
    c • qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ)
⊢ c = 1728
have hgΔ₁ : qExpansion 1 (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) = c • qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ)
Tactic: rw [hcΔ, hgE] at hgΔ
Cleared hypotheses: hgΔ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (hypothesis)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
⊢ discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728
have hc_eq : c = 1728
Tactic: have hc_eq : c = 1728 := by
    have hcΔ : (c • CuspForm.discriminant : ℍ → ℂ) = g := congrArg DFunLike.coe hc
    have hgΔ := ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c
      CuspForm.discriminant
    rw [hcΔ, hgE] at hgΔ
    simpa [PowerSeries.coeff_smul, discriminant_qExpansion_coeff_one,
      E₄CubeSubE₆SqForm_qExpansion_coeff_one] using (congr_arg (·.coeff 1) hgΔ).symm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hc_eq : c = 1728
⊢ 1728 * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
have rw : c * discriminant z =
  HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
Tactic: rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hc_eq : c = 1728
rw :
  c * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
⊢ 1728 * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
have rw₁ : (c • CuspForm.discriminant : (a : ℍ) → ℂ) z =
  HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
Tactic: rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hc_eq : c = 1728
rw :
  c * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₁ :
  (c • CuspForm.discriminant : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
⊢ 1728 * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
have rw₂ : (g : (a : ℍ) → ℂ) z =
  HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
Tactic: rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]