rw [mul_zero]
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 ^ 3 *
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
              ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
              e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a6)) =
    c4 e ^ 3 * 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
⊢ c4 e ^ 3 *
      (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst *
              ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd +
          e.a3 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).snd -
        (((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 3 +
              e.a2 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e).fst +
          e.a6)) =
    0