Theorem: Model.dweierstrass_dx_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_dx (rst_iso r s t e) P =
    dweierstrass_dx e (var_change r s t P) + s * dweierstrass_dy e (var_change r s t P)
Tactic:
simp only [dweierstrass_dx, dweierstrass_dy, rst_iso, var_change]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
P : R × R
⊢ (e.a1 + 2 * s) * P.snd -
      (3 * P.fst ^ 2 + 2 * (e.a2 - s * e.a1 + 3 * r - s * s) * P.fst +
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    e.a1 * (P.snd + s * P.fst + t) - (3 * (P.fst + r) ^ 2 + 2 * e.a2 * (P.fst + r) + e.a4) +
      s * (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
⊢ (e.a1 + 2 * s) * P.snd -
      (3 * P.fst ^ 2 + 2 * (e.a2 - s * e.a1 + 3 * r - s * s) * P.fst +
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    e.a1 * (P.snd + s * P.fst + t) - (3 * (P.fst + r) ^ 2 + 2 * e.a2 * (P.fst + r) + e.a4) +
      s * (2 * (P.snd + s * P.fst + t) + e.a1 * (P.fst + r) + e.a3)
Tactic:
ring
State after:
no goals