split_ifs with hc4
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point e
    (if c4 e = 0 then
      match ringChar K with
      | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
      | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
      | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2)
    else ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e))
case pos
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
⊢ is_singular_point e
    (match ringChar K with
    | 2 => (pth_root e.a4, pth_root (e.a2 * e.a4 + e.a6))
    | 3 => (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3)
    | x => (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2))

case neg
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ is_singular_point e ((18 * b6 e - b2 e * b4 e) / c4 e, (b2 e * b5 e + 3 * b7 e) / c4 e)