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

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 4 * b8 e = b2 e * b6 e - b4 e ^ 2
Tactic:
simp only [b2, b4, b6, b8]
State after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 4 * (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) =
    (e.a1 * e.a1 + 4 * e.a2) * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a3 + 2 * e.a4) ^ 2

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 4 * (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) =
    (e.a1 * e.a1 + 4 * e.a2) * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a3 + 2 * e.a4) ^ 2
Tactic:
ring
State after:
no goals