ring
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 4 * (e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) =
    (e.a1 * e.a1 + 4 * e.a2) * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a3 + 2 * e.a4) ^ 2
no goals