Theorem: Model.rst_discr
Proof state before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (4 * b8 e) +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Tactic:
rw [b8_identity]
Proof state after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (b2 e * b6 e - b4 e ^ 2) +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e