. rw [dweierstrass_dx]
  simp only [ha1, zero_mul, hchar'', add_zero, zero_sub, neg_add_rev]
  rw [← hchar, pth_root_pow_char hcharne, ← sub_eq_add_neg]
  simp only [add_sub_add_right_eq_sub, sub_eq_iff_eq_add, zero_add]
  rw [show (3 : K) = 2 * 2 - 1 by norm_num]
  rw [hchar'']
  simp [← neg_mul_eq_neg_mul]
case pos.h_1.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✝ : ℕ
heq✝ : ringChar K = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0

case pos.h_1.refine_3
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✝ : ℕ
heq✝ : ringChar K = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
case pos.h_1.refine_3
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✝ : ℕ
heq✝ : ringChar K = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0