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

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