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

State before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ Model.b8 (rst_iso 0 s t e).toModel = Model.b8 e.toModel
Tactic:
rw [rst_iso, Model.rst_b8]
State after:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ Model.b8 e.toModel + 3 * 0 * Model.b6 e.toModel + 3 * 0 * 0 * Model.b4 e.toModel + 0 * 0 * 0 * Model.b2 e.toModel +
      3 * 0 * 0 * 0 * 0 =
    Model.b8 e.toModel

State before:
R : Type u
inst✝ : CommRing R
e : ValidModel R
s t : R
⊢ Model.b8 e.toModel + 3 * 0 * Model.b6 e.toModel + 3 * 0 * 0 * Model.b4 e.toModel + 0 * 0 * 0 * Model.b2 e.toModel +
      3 * 0 * 0 * 0 * 0 =
    Model.b8 e.toModel
Tactic:
simp only [mul_zero, add_zero, zero_mul]
State after:
no goals