. rw [is_singular_point]
  have hchar : ringChar K = 2 := by assumption
  have hchar' : (ringChar K : K) = 2 := by simp [hchar]
  have hchar'' : (2 : K) = 0 := by simp [← hchar', ringChar.Nat.cast_ringChar]
  have hcharne : ringChar K ≠ 0 := by simp [hchar]
  have ha1 : e.a1 = 0 := by simpa [c4_zero_iff_a1_zero_of_char_two e hchar] using hc4
  have ha3 : e.a3 = 0 := a3_zero_of_a1_zero_of_disc_zero_of_char_two e hchar h ha1
  refine ⟨?_, ?_, ?_⟩
  . rw [weierstrass]
    simp only [ha1, ha3, mul_zero, zero_add, zero_mul, add_zero]
    rw [show 3 = 2 + 1 by norm_num]
    rw [pow_succ _ 2]
    rw [← hchar, pth_root_pow_char hcharne]
    rw [pth_root_pow_char hcharne]
    ring_nf
    simp [hchar'']
  . 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]
  . simp [dweierstrass_dy, ha1, ha3, hchar'']
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
⊢ is_singular_point e (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))

case pos.h_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 = 3
⊢ is_singular_point e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)

case pos.h_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✝² : ℕ
x✝¹ : ringChar K = 2 → False
x✝ : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
case pos.h_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 = 3
⊢ is_singular_point e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)

case pos.h_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✝² : ℕ
x✝¹ : ringChar K = 2 → False
x✝ : ringChar K = 3 → False
⊢ is_singular_point e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)