ring
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ (e.a1 + 2 * s) * P.snd -
      (3 * P.fst ^ 2 + 2 * (e.a2 - s * e.a1 + 3 * r - s * s) * P.fst +
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    e.a1 * (P.snd + s * P.fst + t) - (3 * (P.fst + r) ^ 2 + 2 * e.a2 * (P.fst + r) + e.a4) +
      s * (2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3)
no goals