rw [b5, b7, c4, b2, b4, b6]
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e * (b2 e * b5 e + 3 * b7 e) ^ 2 + c4 e * e.a1 * (18 * b6 e - b2 e * b4 e) * (b2 e * b5 e + 3 * b7 e) +
        c4 e * c4 e * e.a3 * (b2 e * b5 e + 3 * b7 e) -
      ((18 * b6 e - b2 e * b4 e) ^ 3 + c4 e * e.a2 * (18 * b6 e - b2 e * b4 e) ^ 2 +
          c4 e * c4 e * e.a4 * (18 * b6 e - b2 e * b4 e) +
        c4 e * c4 e * c4 e * e.a6) =
    0
case neg.refine_1
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
            ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
                3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) ^
              2 +
          ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a1 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) *
            ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
              3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) +
        ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
              ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
            e.a3 *
          ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
            3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) -
      ((18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 3 +
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a2 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 2 +
          ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
                ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
              e.a4 *
            (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) +
        ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
              ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          e.a6) =
    0