-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
⊢ (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)
have 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)
Tactic: simp only [ModularForm.directSum_of_pow]