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

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ dweierstrass_dy (rst_iso r s t e) P = dweierstrass_dy e (var_change r s t P)
Tactic:
simp only [dweierstrass_dy, rst_iso, var_change]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ 2 * P.snd + (e.a1 + 2 * s) * P.fst + (e.a3 + r * e.a1 + 2 * t) =
    2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ 2 * P.snd + (e.a1 + 2 * s) * P.fst + (e.a3 + r * e.a1 + 2 * t) =
    2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3
Tactic:
ring
State after:
no goals