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

State before:
R : Type u
inst✝ : CommRing R
a b r p : R
⊢ p ^ 2 * a + 2 * (p * r) * (p ^ 1 * b) + 3 * (p * r) ^ 2 = p ^ 2 * (a + 2 * r * b + 3 * r ^ 2)
Tactic:
ring
State after:
no goals