-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
simp :
  (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) =
    (1 / 1728) •
      HSub.hSub (α :=
        DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
        (β :=
        DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
        ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
                (HMul.hMul (α := ℤ) (↑3 : ℤ) 4) :
              (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑3 : ℤ) * 4)) →
                DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
            (E₄.pow 3) :
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
        ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
                (HMul.hMul (α := ℤ) (↑2 : ℤ) 6) :
              (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑2 : ℤ) * 6)) →
                DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
            (E₆.pow 2) :
          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) =
    (1 / 1728) •
      (HPow.hPow (α :=
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
          (β := ℕ)
          ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 4 :
                (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 4) →
                  DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
              E₄ :
            DirectSum ℤ fun (i : ℤ) ↦
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
          3 -
        HPow.hPow (α :=
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
          (β := ℕ)
          ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 6 :
                (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 6) →
                  DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
              E₆ :
            DirectSum ℤ fun (i : ℤ) ↦
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
          2)

Tactic:
simp only [ModularForm.directSum_of_pow]

Premises used: ModularForm.directSum_of_pow