Theorem: factorize9 (ECTate/Algebra/EllipticCurve/AuxRingLemmas.lean)

State before:
R : Type u
inst✝ : CommRing R
a1 a2 a3 a4 a6 b8 p : R
⊢ p ^ 1 * a1 * (p ^ 1 * a1) * (p ^ 3 * a6) + p ^ 1 * a1 * (p ^ 2 * a3) * -a4 + 4 * a2 * (p ^ 3 * a6) +
        a2 * (p ^ 2 * a3) * (p ^ 2 * a3) +
      p ^ 3 * -b8 =
    p ^ 3 * (p ^ 1 * a1 * (p ^ 1 * a1) * a6 + a1 * a3 * -a4 + 4 * a2 * a6 + a2 * a3 * (p ^ 1 * a3) + -b8)
Tactic:
ring
State after:
no goals