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

State before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
r : R
⊢ (rst_iso r 0 0 e).toModel.a6 = e.a6 + r * e.a4 + r ^ 2 * e.a2 + r ^ 3
Tactic:
simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero,
mul_zero, one_mul, add_zero, mul_assoc, pow_two r, pow_succ r, pow_zero, mul_one]
State after:
no goals