awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 = 1
have norm_cast : HAdd.hAdd (α := ℕ) 1 0 = 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (1 : ℂ)
hp6_0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (1 : ℂ)
hp4_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (240 : ℂ)
hp6_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (-504 : ℂ)
hqc4 : c4 • p4 = HPow.hPow (β := ℕ) p 2
hqc6 : c6 • p6 = HPow.hPow (β := ℕ) p 3
⊢ p = 0
have hp4_0₁ : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (1 : ℂ)
Tactic: simp_all only [PowerSeries.coeff_zero_eq_constantCoeff]
Cleared hypotheses: hp4_0, hp6_0, hp4_1, hp6_1, hqc4, hqc6
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (1 : ℂ)
hp6_0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (1 : ℂ)
hp4_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (240 : ℂ)
hp6_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (-504 : ℂ)
hqc4 : c4 • p4 = HPow.hPow (β := ℕ) p 2
hqc6 : c6 • p6 = HPow.hPow (β := ℕ) p 3
hp4_0₁ : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (1 : ℂ)
⊢ p = 0
have hp6_0₁ : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (1 : ℂ)
Tactic: simp_all only [PowerSeries.coeff_zero_eq_constantCoeff]
Cleared hypotheses: hp4_0, hp6_0, hp4_1, hp6_1, hqc4, hqc6
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (1 : ℂ)
hp6_0 : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (1 : ℂ)
hp4_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (240 : ℂ)
hp6_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (-504 : ℂ)
hqc4 : c4 • p4 = HPow.hPow (β := ℕ) p 2
hqc6 : c6 • p6 = HPow.hPow (β := ℕ) p 3
D : PowerSeries ℂ := HPow.hPow (β := ℕ) (c4 • p4) 3 - HPow.hPow (β := ℕ) (c6 • p6) 2
⊢ p = 0
have hD0 : (PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) D = HPow.hPow (β := ℕ) c4 3 - HPow.hPow (β := ℕ) c6 2
Tactic: have hD0 : D.coeff 0 = c4 ^ 3 - c6 ^ 2 := by simp [D, hp4_0, hp6_0]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (1 : ℂ)
hp6_0 : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (1 : ℂ)
hp4_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (240 : ℂ)
hp6_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (-504 : ℂ)
hqc4 : c4 • p4 = HPow.hPow (β := ℕ) p 2
hqc6 : c6 • p6 = HPow.hPow (β := ℕ) p 3
D : PowerSeries ℂ := HPow.hPow (β := ℕ) (c4 • p4) 3 - HPow.hPow (β := ℕ) (c6 • p6) 2
hD0 : (PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) D = HPow.hPow (β := ℕ) c4 3 - HPow.hPow (β := ℕ) c6 2
⊢ (PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) D = 720 * HPow.hPow (β := ℕ) c4 3 + 1008 * HPow.hPow (β := ℕ) c6 2
have simp : c4 *
      (c4 *
        (c4 *
          (HMul.hMul (β := ℂ)
              (HMul.hMul (α := ℂ) (β := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ)
                ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ))
              ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) +
            HMul.hMul (β := ℂ)
              (HMul.hMul (α := ℂ) (β := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ)
                  ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) +
                HMul.hMul (α := ℂ) (β := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ)
                  ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ))
              ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ)))) -
    c6 *
      (c6 *
        (HMul.hMul (α := ℂ) (β := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p6 : ℂ)
            ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) +
          HMul.hMul (α := ℂ) (β := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ)
            ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p6 : ℂ))) =
  720 * (c4 * c4 * c4) + 1008 * (c6 * c6)
Tactic: simp [D, pow_succ, PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (1 : ℂ)
hp6_0 : Eq (α := ℂ) ((PowerSeries.constantCoeff : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (1 : ℂ)
hp4_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p4 : ℂ) (240 : ℂ)
hp6_1 : Eq (α := ℂ) ((PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) p6 : ℂ) (-504 : ℂ)
hqc4 : c4 • p4 = HPow.hPow (β := ℕ) p 2
hqc6 : c6 • p6 = HPow.hPow (β := ℕ) p 3
D : PowerSeries ℂ := HPow.hPow (β := ℕ) (c4 • p4) 3 - HPow.hPow (β := ℕ) (c6 • p6) 2
hD0 : (PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) D = HPow.hPow (β := ℕ) c4 3 - HPow.hPow (β := ℕ) c6 2
⊢ p = 0
have hD1 : (PowerSeries.coeff 1 : (a : PowerSeries ℂ) → ℂ) D = 720 * HPow.hPow (β := ℕ) c4 3 + 1008 * HPow.hPow (β := ℕ) c6 2
Tactic: have hD1 : D.coeff 1 = 720 * c4 ^ 3 + 1008 * c6 ^ 2 := by
    simp [D, pow_succ, PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ]
    grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
⊢ qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0
have obtain : ∀ (c4 : ℂ) (hc4 : c4 • E₄ = f.mul f), qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0
Tactic: obtain ⟨c4, hc4⟩ : ∃ c4, c4 • E₄ = f.mul f :=
    (finrank_eq_one_iff_of_nonzero' E₄ (E_ne_zero _ ⟨2, rfl⟩)).mp
      (Module.rank_eq_one_iff_finrank_eq_one.mp levelOne_weight_four_rank_one) _
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
⊢ qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0
have obtain : ∀ (c6 : ℂ) (hc6 : c6 • E₆ = (f.mul f).mul f), qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0
Tactic: obtain ⟨c6, hc6⟩ : ∃ c6, c6 • E₆ = (f.mul f).mul f :=
    (finrank_eq_one_iff_of_nonzero' E₆ (E_ne_zero _ ⟨3, rfl⟩)).mp
      (Module.rank_eq_one_iff_finrank_eq_one.mp levelOne_weight_six_rank_one) _
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
⊢ c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
have rw : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
Tactic: rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
      show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
rw : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
⊢ c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
have rw₁ : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ)
Tactic: rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
      show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
rw : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₁ : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ)
⊢ c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
have rw₂ : qExpansion 1 (HSMul.hSMul (β := (a : ℍ) → ℂ) c4 (⇑E₄ : (a : ℍ) → ℂ)) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ)
Tactic: rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
      show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
rw : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₁ : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ)
rw₂ : qExpansion 1 (HSMul.hSMul (β := (a : ℍ) → ℂ) c4 (⇑E₄ : (a : ℍ) → ℂ)) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ)
⊢ c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
have rw₃ : qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ)
Tactic: rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
      show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
⊢ qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0
have hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
Tactic: have hqc4 : c4 • qExpansion 1 (E₄ : ℍ → ℂ) = qExpansion 1 (f : ℍ → ℂ) ^ 2 := by
    rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
      show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
⊢ c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
have rw : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
  HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2 * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
Tactic: rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
rw :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2 * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
⊢ c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
have rw₁ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
  qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
Tactic: rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
rw :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2 * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₁ :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
⊢ c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
have rw₂ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
Tactic: rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
rw :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2 * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₁ :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₂ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
⊢ c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
have rw₃ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = qExpansion 1 (⇑((f.mul f).mul f) : (a : ℍ) → ℂ)
Tactic: rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
rw :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2 * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₁ :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₂ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₃ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = qExpansion 1 (⇑((f.mul f).mul f) : (a : ℍ) → ℂ)
⊢ c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
have rw₄ : qExpansion 1 (HSMul.hSMul (β := (a : ℍ) → ℂ) c6 (⇑E₆ : (a : ℍ) → ℂ)) = qExpansion 1 (⇑((f.mul f).mul f) : (a : ℍ) → ℂ)
Tactic: rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
rw :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2 * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₁ :
  c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) =
    qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₂ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = qExpansion 1 (⇑(f.mul f) : (a : ℍ) → ℂ) * qExpansion 1 (⇑f : (a : ℍ) → ℂ)
rw₃ : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = qExpansion 1 (⇑((f.mul f).mul f) : (a : ℍ) → ℂ)
rw₄ :
  qExpansion 1 (HSMul.hSMul (β := (a : ℍ) → ℂ) c6 (⇑E₆ : (a : ℍ) → ℂ)) = qExpansion 1 (⇑((f.mul f).mul f) : (a : ℍ) → ℂ)
⊢ c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
have rw₅ : qExpansion 1 (⇑((f.mul f).mul f) : (a : ℍ) → ℂ) = qExpansion 1 (⇑((f.mul f).mul f) : (a : ℍ) → ℂ)
Tactic: rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
⊢ qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0
have hqc6 : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
Tactic: have hqc6 : c6 • qExpansion 1 E₆ = qExpansion 1 (f : ℍ → ℂ) ^ 3 := by
    rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
      ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
      show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have this : k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k
Tactic: have : k < 3 ∨ (3 ≤ k ∧ k < 12) ∨ 12 ≤ k := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
this : k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have h : ∀ (hk : k < 3),
  Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
Tactic: rcases this with hk | hk | hk
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
this : k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k
h :
  ∀ (hk : k < 3),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
      (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have h₁ : ∀ (hk : 3 ≤ k ∧ k < 12),
  Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
Tactic: rcases this with hk | hk | hk
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
this : k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k
h :
  ∀ (hk : k < 3),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
      (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
h₁ :
  ∀ (hk : 3 ≤ k ∧ k < 12),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
      (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have h₂ : ∀ (hk : 12 ≤ k),
  Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
Tactic: rcases this with hk | hk | hk
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : k < 3
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have h : ∀
  (ihn :
    ∀ m < 0,
      ∀ (hk2 : Even m),
        Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
          (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0}))
  (hk2 : Even (α := ℕ) 0) (hk : LT.lt (α := ℕ) 0 3),
  Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑0 : ℤ)) =
    (↑(if 0 ≡ 2 [MOD 12] then 0 / 12 else 0 / 12 + 1) : Cardinal.{0})
Tactic: interval_cases k
Cleared hypotheses: ihn, hk2, hk