simp only [rst_iso, Model.rst_iso, one_pow, zero_mul, sub_zero, mul_zero,
one_mul, add_zero, mul_add, ←pow_two t, sub_eq_add_neg, neg_add, ←add_assoc]
R : Type u
inst✝ : CommRing R
e : ValidModel R
t : R
⊢ (rst_iso 0 0 t e).toModel.a6 = e.a6 - t * e.a3 - t ^ 2
no goals