simp only [dweierstrass_dy, rst_iso, var_change]
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)
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