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

State before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
r t : R
⊢ (rst_iso r 0 t e).toModel.a1 = e.a1
Tactic:
simp only [rst_iso, Model.rst_iso, mul_zero, add_zero, one_mul]
State after:
no goals