apply And.intro <;>
ring
R : Type u
inst✝ : CommRing R
r s t r' s' t' : R
P : R × R
⊢ P.fst + r' + r = P.fst + (r + r') ∧
    P.snd + s' * P.fst + t' + s * (P.fst + r') + t = P.snd + (s + s') * P.fst + (t + t' + s * r')
no goals