simp only [mul_inv_cancel hc4, one_mul]
case neg.refine_2
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 * (e.a1 * (b2 e * b5 e + 3 * b7 e) - 2 * e.a2 * (18 * b6 e - b2 e * b4 e)) -
        c4 e * (c4 e)⁻¹ * c4 e * (c4 e)⁻¹ * 3 * (18 * b6 e - b2 e * b4 e) ^ 2 -
      e.a4 * c4 e * c4 e =
    0
case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ c4 e * (e.a1 * (b2 e * b5 e + 3 * b7 e) - 2 * e.a2 * (18 * b6 e - b2 e * b4 e)) - 3 * (18 * b6 e - b2 e * b4 e) ^ 2 -
      e.a4 * c4 e * c4 e =
    0