awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
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
⊢ 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

Premises used: rank_zero_iff_forall_zero, ModularForm.levelOne_neg_weight_rank_zero, ModularForm.discriminant_qExpansion_order, add_comm, Nat.cast_add, Iff.mp, ENat.coe_ne_top, ModularForm.mcast_eq_zero_iff, lt_or_ge, OfNat.ofNat, PowerSeries.order_mul, Nat.cast_one, ENat.add_lt_add_iff_right, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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
inr : ∀ (hk : 0 ≤ k), f = 0
⊢ f = 0

Tactic:
rcases lt_or_ge k 0 with hk | hk

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : (↑(k.toNat / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
hk : k < 0
⊢ f = 0

Tactic:
rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero hk) f

Premises used: rank_zero_iff_forall_zero, ModularForm.levelOne_neg_weight_rank_zero, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : (↑(k.toNat / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
hk : k < 0
⊢ f = 0

Tactic:
exact rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero hk) f

Premises used: rank_zero_iff_forall_zero, ModularForm.levelOne_neg_weight_rank_zero, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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
⊢ 0 ≤ k

Tactic:
hk
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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
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
⊢ f = 0

Tactic:
lift k to ℕ using hk
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
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:
sturm_bound_levelOne_nat (mod_cast h)

Premises used: UpperHalfPlane.qExpansion, congrArg, cast, HDiv.hDiv, Nat.cast, LT.lt, PowerSeries.order, ModularForm.sturm_bound_levelOne_nat, Int.toNat, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, DFunLike.coe, Eq.trans
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
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:
exact sturm_bound_levelOne_nat (mod_cast h)

Premises used: ModularForm.sturm_bound_levelOne_nat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
⊢ HMul.hMul (α := ℤ) (↑3 : ℤ) 4 = 12

Tactic:
decide
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
⊢ HMul.hMul (α := ℤ) (↑2 : ℤ) 6 = 12

Tactic:
decide
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
z : ℍ
⊢ (E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2

Tactic:
simp only [E₄CubeSubE₆SqForm, coe_mcast, coe_pow, sub_apply, Pi.pow_apply]

Premises used: ModularForm.sub_apply, ModularForm.coe_pow, Pi.pow_apply, ModularForm.coe_mcast, _private.0.ModularForm.E₄CubeSubE₆SqForm
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
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 : ℍ) → ℂ)
⊢ 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 : ℍ) → ℂ)

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]

Premises used: ModularForm.qExpansion_pow, one_mem_strictPeriods_SL, ModularForm.qExpansion_sub, ModularForm.coe_mcast, _private.0.ModularForm.E₄CubeSubE₆SqForm, ModularForm.coe_sub, one_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
⊢ 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:
ring
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
⊢ E₄CubeSubE₆SqForm.IsCuspForm

Tactic:
simp [isCuspForm_iff_coeffZero_eq_zero, E₄CubeSubE₆SqForm_qExpansion_eq,
    PowerSeries.coeff_mul, -PowerSeries.coeff_zero_eq_constantCoeff,
    E_qExpansion_coeff_zero _ ⟨2, rfl⟩, E_qExpansion_coeff_zero _ ⟨3, rfl⟩]

Premises used: ModularForm.isCuspForm_iff_coeffZero_eq_zero, PowerSeries.coeff_mul, _private.0.ModularForm.E₄CubeSubE₆SqForm_qExpansion_eq, PowerSeries.coeff_zero_eq_constantCoeff, Exists.intro, EisensteinSeries.E_qExpansion_coeff_zero, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
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 : ℂ)
⊢ Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)) : ℂ)
    (1728 : ℂ)

Tactic:
rw [E₄CubeSubE₆SqForm_qExpansion_eq]

Premises used: _private.0.ModularForm.E₄CubeSubE₆SqForm_qExpansion_eq
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
⊢ 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:
norm_num [PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ, E₄_qExpansion_coeff_one,
    E₆_qExpansion_coeff_one, E_qExpansion_coeff_zero _ ⟨2, rfl⟩,
    E_qExpansion_coeff_zero _ ⟨3, rfl⟩]

Premises used: ModularForm.E₆_qExpansion_coeff_one, Finset.Nat.antidiagonal_succ, ModularForm.E₄_qExpansion_coeff_one, PowerSeries.coeff_mul, Exists.intro, EisensteinSeries.E_qExpansion_coeff_zero, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
z : ℍ
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
⊢ discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728

Tactic:
obtain ⟨g, hg⟩ := E₄CubeSubE₆SqForm_isCuspForm

Premises used: _private.0.ModularForm.E₄CubeSubE₆SqForm_isCuspForm
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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
obtain :
  ∀ (c : ℂ) (hc : c • CuspForm.discriminant = g),
    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) /
      1728

Tactic:
obtain ⟨c, hc⟩ := CuspForm.exists_smul_discriminant_of_weight_eq_twelve g

Premises used: CuspForm.exists_smul_discriminant_of_weight_eq_twelve
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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
⊢ Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)

Tactic:
have hgE : (g : ℍ → ℂ) = E₄CubeSubE₆SqForm := congrArg DFunLike.coe hg
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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 : ℍ) → ℂ)
⊢ HSMul.hSMul (β := (a : ℍ) → ℂ) c (⇑CuspForm.discriminant : (a : ℍ) → ℂ) = (⇑g : (a : ℍ) → ℂ)

Tactic:
have hcΔ : (c • CuspForm.discriminant : ℍ → ℂ) = g := congrArg DFunLike.coe hc
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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 : ℍ) → ℂ)
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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 : ℍ) → ℂ)
⊢ qExpansion 1 (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) = c • qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ)

Tactic:
rw [hcΔ, hgE] at hgΔ
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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 (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) = c • qExpansion 1 (⇑CuspForm.discriminant : (a : ℍ) → ℂ)
⊢ c = 1728

Tactic:
simpa [PowerSeries.coeff_smul, discriminant_qExpansion_coeff_one,
      E₄CubeSubE₆SqForm_qExpansion_coeff_one] using (congr_arg (·.coeff 1) hgΔ).symm

Premises used: _private.0.ModularForm.E₄CubeSubE₆SqForm_qExpansion_coeff_one, ModularForm.discriminant_qExpansion_coeff_one, congr_arg, PowerSeries.coeff_smul, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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

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
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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
rw₂ :
  (g : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₃ :
  (E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₄ rw₅ :
  HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2 =
    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

Tactic:
rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]

Premises used: _private.0.ModularForm.E₄CubeSubE₆SqForm_apply, congr_fun, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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

Tactic:
have h1728 : (1728 : ℂ) * discriminant z = E₄ z ^ 3 - E₆ z ^ 2 := by
    rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
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
h1728 :
  1728 * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
⊢ discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728

Tactic:
linear_combination h1728 / 1728
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
h :
  modularForm CuspForm.discriminant =
    (1 / 1728) •
      HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
        (E₄.pow 3 :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
        (E₆.pow 2 :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (HMul.hMul (α := ℤ) (↑2 : ℤ) 6))
⊢ Eq (α :=
    DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
    ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
          (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
            DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
        (modularForm CuspForm.discriminant) :
      DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
    ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
          (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
            DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
        ((1 / 1728) •
          HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
            (E₄.pow 3 :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
            (E₆.pow 2 :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                (HMul.hMul (α := ℤ) (↑2 : ℤ) 6))) :
      DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
h :
  ∀ (z : ℍ),
    Eq (α := ℂ) ((modularForm CuspForm.discriminant : (a : ℍ) → ℂ) z : ℂ)
      (((1 / 1728) •
              HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
                (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
                (E₄.pow 3 :
                  ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                    (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
                (E₆.pow 2 :
                  ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                    (HMul.hMul (α := ℤ) (↑2 : ℤ) 6)) :
            (a : ℍ) → ℂ)
          z :
        ℂ)
⊢ modularForm CuspForm.discriminant =
    (1 / 1728) •
      HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
        (E₄.pow 3 :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
        (E₆.pow 2 :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (HMul.hMul (α := ℤ) (↑2 : ℤ) 6))

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
z : ℍ
⊢ discriminant z =
    1 / 1728 *
      (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2)

Tactic:
grind [discriminant_eq_E₄_cube_sub_E₆_sq z]

Premises used: ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h ≈ h'
⊢ h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ

Tactic:
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hhh'

Premises used: Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
⊢ ∃ g ∈ 𝒢, (↑h' : GL (Fin 2) ℝ) = (↑h : GL (Fin 2) ℝ) * g

Tactic:
⟨h⁻¹ * h', hhh', mod_cast (mul_inv_cancel_left h h').symm⟩

Premises used: HMul.hMul, cast, Inv.inv, And.intro, Exists.intro, SetLike.coe_eq_coe._simp_1, Eq.symm, mul_inv_cancel_left, Subtype.val
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
⊢ ∃ g ∈ 𝒢, (↑h' : GL (Fin 2) ℝ) = (↑h : GL (Fin 2) ℝ) * g

Tactic:
exact ⟨h⁻¹ * h', hhh', mod_cast (mul_inv_cancel_left h h').symm⟩