simp only [c4, c6, b2, b4, b6]
case pos.h_3.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ e.a1 * (-(-e.a1 * b2 e + 12 * e.a3) * 6) - (3 * (-b2 e) ^ 2 + 24 * e.a2 * -b2 e + 144 * e.a4) = 3 * c4 e
case pos.h_3.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
h12 : 12 ≠ 0
⊢ e.a1 * (-(-e.a1 * (e.a1 * e.a1 + 4 * e.a2) + 12 * e.a3) * 6) -
      (3 * (-(e.a1 * e.a1 + 4 * e.a2)) ^ 2 + 24 * e.a2 * -(e.a1 * e.a1 + 4 * e.a2) + 144 * e.a4) =
    3 * ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4))