Theorem: Model.var_change_comp (ECTate/Algebra/EllipticCurve/Model.lean)

State before:
R : Type u
inst✝ : CommRing R
r s t r' s' t' : R
P : R × R
⊢ var_change r s t (var_change r' s' t' P) = var_change (r + r') (s + s') (t + t' + s * r') P
Tactic:
simp only [var_change, Prod.mk.injEq]
State after:
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')

State before:
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')
Tactic:
apply And.intro <;>
ring
State after:
no goals