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

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ c4 (rst_iso r s t e) = c4 e
Tactic:
simp only [rst_iso, b2, b4, b6, b8, c4]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ ((e.a1 + 2 * s) * (e.a1 + 2 * s) + 4 * (e.a2 - s * e.a1 + 3 * r - s * s)) ^ 2 -
      24 *
        ((e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) +
          2 * (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t)) =
    (e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)

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