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

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ b2 (rst_iso r s t e) = b2 e + 12 * r
Tactic:
simp [rst_iso, b2]
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) = e.a1 * e.a1 + 4 * e.a2 + 12 * r

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) = e.a1 * e.a1 + 4 * e.a2 + 12 * r
Tactic:
ring
State after:
no goals