Theorem: Model.rst_b8 (ECTate/Algebra/EllipticCurve/Model.lean)

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ b8 (rst_iso r s t e) = b8 e + 3 * r * b6 e + 3 * r * r * b4 e + r * r * r * b2 e + 3 * r * r * r * r
Tactic:
simp only [rst_iso, b2, b4, b6, b8]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a1 + 2 * s) * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) -
            (e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) *
              (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) +
          4 * (e.a2 - s * e.a1 + 3 * r - s * s) *
            (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) +
        (e.a2 - s * e.a1 + 3 * r - s * s) * (e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) -
      (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) *
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) =
    e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4 +
            3 * r * (e.a3 * e.a3 + 4 * e.a6) +
          3 * r * r * (e.a1 * e.a3 + 2 * e.a4) +
        r * r * r * (e.a1 * e.a1 + 4 * e.a2) +
      3 * r * r * r * r

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (e.a1 + 2 * s) * (e.a1 + 2 * s) * (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) -
            (e.a1 + 2 * s) * (e.a3 + r * e.a1 + 2 * t) *
              (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) +
          4 * (e.a2 - s * e.a1 + 3 * r - s * s) *
            (e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)) +
        (e.a2 - s * e.a1 + 3 * r - s * s) * (e.a3 + r * e.a1 + 2 * t) * (e.a3 + r * e.a1 + 2 * t) -
      (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) *
        (e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t) =
    e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4 +
            3 * r * (e.a3 * e.a3 + 4 * e.a6) +
          3 * r * r * (e.a1 * e.a3 + 2 * e.a4) +
        r * r * r * (e.a1 * e.a1 + 4 * e.a2) +
      3 * r * r * r * r
Tactic:
ring
State after:
no goals