simp only [discr, rst_b2, rst_b4, rst_b6, rst_b8]
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ discr (rst_iso r s t e) = discr e
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e + 12 * r) * (b2 e + 12 * r) * (b8 e + 3 * r * b6 e + 3 * r * r * b4 e + r * r * r * b2 e + 3 * r * r * r * r) -
          8 * (b4 e + r * (b2 e + 6 * r)) ^ 3 -
        27 * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) *
          (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) +
      9 * (b2 e + 12 * r) * (b4 e + r * (b2 e + 6 * r)) * (b6 e + 2 * r * b4 e + r * r * b2 e + 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