-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
Goal:
rw :
  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)
⊢ (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 ℝ))) 12 :
              (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
                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 ℝ))) 12 :
              (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
                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:
rw [← map_sub (DirectSum.of (ModularForm 𝒮ℒ) 12), ← DirectSum.of_smul]

Premises used: ModularForm, MonoidHom.range, DirectSum.of_smul, Real, map_sub, DirectSum.of, Matrix.SpecialLinearGroup.mapGL, OfNat.ofNat