have ha1 : e.a1 = 0 := by simpa [c4_zero_iff_a1_zero_of_char_two e hchar] using hc4
case pos.h_1
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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0
case pos.h_1
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
⊢ weierstrass e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
    dweierstrass_dx e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0 ∧
      dweierstrass_dy e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6)) = 0