Theorem: ValidModel.st_of_a4 (ECTate/Algebra/EllipticCurve/Model.lean)

State before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ (rst_iso 0 s t e).toModel.a4 = e.a4 - s * e.a3 - t * e.a1 - 2 * s * t
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, mul_zero, one_mul, add_zero, mul_assoc, zero_mul]
State after:
no goals