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

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