rw [show c4 e ^ 3 * (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
      e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
    e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
    (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
    e.a4 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) + e.a6)) =
  (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * ((b2 e * b5 e + 3 * b7 e)) ^ 2 +
    c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * ((18 * b6 e - b2 e * b4 e)) * ((b2 e * b5 e + 3 * b7 e)) +
  c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * ((b2 e * b5 e + 3 * b7 e)) -
  (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * ((18 * b6 e - b2 e * b4 e)) ^ 3 +
  c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * ((18 * b6 e - b2 e * b4 e)) ^ 2 +
    c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * ((18 * b6 e - b2 e * b4 e)) +
  c4 e * c4 e * c4 e * e.a6)) by ring]
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 *
      (((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) ^ 2 +
            e.a1 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) +
          e.a3 * ((b2 e * b5 e + 3 * b7 e) * (c4 e)⁻¹) -
        (((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 3 + e.a2 * ((18 * b6 e - b2 e * b4 e) * (c4 e)⁻¹) ^ 2 +
            e.a4 * ((18 * b6 e - b2 e * b4 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
⊢ c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (b2 e * b5 e + 3 * b7 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a1 * (18 * b6 e - b2 e * b4 e) * (b2 e * b5 e + 3 * b7 e) +
        c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a3 * (b2 e * b5 e + 3 * b7 e) -
      (c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * (18 * b6 e - b2 e * b4 e) ^ 3 +
            c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * c4 e * e.a2 * (18 * b6 e - b2 e * b4 e) ^ 2 +
          c4 e * (c4 e)⁻¹ * c4 e * c4 e * e.a4 * (18 * b6 e - b2 e * b4 e) +
        c4 e * c4 e * c4 e * e.a6) =
    0