simp only [c4, c6, discr, mul_sub, mul_add]
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * discr e = c4 e ^ 3 - c6 e ^ 2
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * (-b2 e * b2 e * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) + 1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2