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