@[simp]

theorem List.splitOn_nil {α : Type u_1} [BEq α] (a : α) : splitOn a [] = [[]]

@[simp]

theorem List.splitOnP_nil {α : Type u_1} {p : α → Bool} : splitOnP p [] = [[]]

@[simp]

theorem List.splitOnPPrepend_ne_nil {α : Type u_1} (p : α → Bool) (xs acc : List α) : splitOnPPrepend p xs acc ≠ []

@[deprecated List.splitOnPPrepend_ne_nil (since := "2026-02-26")]

theorem List.splitOnP.go_ne_nil {α : Type u_1} (p : α → Bool) (xs acc : List α) : splitOnPPrepend p xs acc ≠ []

@[simp]

theorem List.splitOnPPrepend_nil {α : Type u_1} {p : α → Bool} {acc : List α} : splitOnPPrepend p [] acc = [acc.reverse]

@[simp]

theorem List.splitOnPPrepend_nil_right {α : Type u_1} {p : α → Bool} {xs : List α} : splitOnPPrepend p xs [] = splitOnP p xs

theorem List.splitOnP_eq_splitOnPPrepend {α : Type u_1} {p : α → Bool} {xs : List α} : splitOnP p xs = splitOnPPrepend p xs []

theorem List.splitOnPPrepend_cons_eq_ite {α : Type u_1} {p : α → Bool} {x : α} {xs acc : List α} : splitOnPPrepend p (x :: xs) acc = if p x = true then acc.reverse :: splitOnP p xs else splitOnPPrepend p xs (x :: acc)

@[deprecated List.splitOnPPrepend_cons_eq_ite (since := "2026-07-21")]

theorem List.splitOnPPrepend_cons_eq_if {α : Type u_1} {p : α → Bool} {x : α} {xs acc : List α} : splitOnPPrepend p (x :: xs) acc = if p x = true then acc.reverse :: splitOnP p xs else splitOnPPrepend p xs (x :: acc)

theorem List.splitOnPPrepend_cons_pos {α : Type u_1} {p : α → Bool} {a : α} {l acc : List α} (h : p a = true) : splitOnPPrepend p (a :: l) acc = acc.reverse :: splitOnP p l

theorem List.splitOnPPrepend_cons_neg {α : Type u_1} {p : α → Bool} {a : α} {l acc : List α} (h : p a = false) : splitOnPPrepend p (a :: l) acc = splitOnPPrepend p l (a :: acc)

theorem List.splitOnP_cons_eq_ite_splitOnPPrepend {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else splitOnPPrepend p xs [x]

@[deprecated List.splitOnP_cons_eq_ite_splitOnPPrepend (since := "2026-07-21")]

theorem List.splitOnP_cons_eq_if_splitOnPPrepend {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else splitOnPPrepend p xs [x]

theorem List.splitOnPPrepend_eq_modifyHead {α : Type u_1} {p : α → Bool} {xs acc : List α} : splitOnPPrepend p xs acc = modifyHead (fun (x : List α) => acc.reverse ++ x) (splitOnP p xs)

@[deprecated List.splitOnPPrepend_eq_modifyHead (since := "2026-02-26")]

theorem List.splitOnP.go_acc {α : Type u_1} {p : α → Bool} {xs acc : List α} : splitOnPPrepend p xs acc = modifyHead (fun (x : List α) => acc.reverse ++ x) (splitOnP p xs)

@[simp]

theorem List.splitOnP_ne_nil {α : Type u_1} (p : α → Bool) (xs : List α) : splitOnP p xs ≠ []

theorem List.splitOnP_cons_eq_ite_modifyHead {α : Type u_1} {p : α → Bool} (x : α) (xs : List α) : splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)

@[deprecated List.splitOnP_cons_eq_ite_modifyHead (since := "2026-07-21")]

theorem List.splitOnP_cons_eq_if_modifyHead {α : Type u_1} {p : α → Bool} (x : α) (xs : List α) : splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)

@[deprecated List.splitOnP_cons_eq_ite_modifyHead (since := "2026-02-26")]

theorem List.splitOnP_cons {α : Type u_1} {p : α → Bool} (x : α) (xs : List α) : splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)

theorem List.splitOnP_spec {α : Type u_1} {p : α → Bool} (as : List α) : (zipWith (fun (x1 x2 : List α) => x1 ++ x2) (splitOnP p as) (map (fun (x : α) => [x]) (filter p as) ++ [[]])).flatten = as

The original list L can be recovered by flattening the lists produced by splitOnP p L, interspersed with the elements L.filter p.

theorem List.splitOnP_eq_singleton {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∀ (x : α), x ∈ xs → p x = false) : splitOnP p xs = [xs]

If no element satisfies p in the list xs, then xs.splitOnP p = [xs]

@[deprecated List.splitOnP_eq_singleton (since := "2026-02-26")]

theorem List.splitOnP_eq_single {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∀ (x : α), x ∈ xs → p x = false) : splitOnP p xs = [xs]

theorem List.splitOnP_append_cons {α : Type u_1} {p : α → Bool} (xs as : List α) {sep : α} (hsep : p sep = true) : splitOnP p (xs ++ sep :: as) = splitOnP p xs ++ splitOnP p as

When a list of the form [...xs, sep, ...as] is split at the sep element satisfying p, the result is the concatenation of splitOnP called on xs and as

theorem List.splitOnP_append_cons_of_forall_mem {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∀ (x : α), x ∈ xs → p x = false) (sep : α) (hsep : p sep = true) (as : List α) : splitOnP p (xs ++ sep :: as) = xs :: splitOnP p as

When a list of the form [...xs, sep, ...as] is split on p, the first element is xs, assuming no element in xs satisfies p but sep does satisfy p

@[deprecated List.splitOnP_append_cons_of_forall_mem (since := "2026-02-26")]

theorem List.splitOnP_first {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∀ (x : α), x ∈ xs → p x = false) (sep : α) (hsep : p sep = true) (as : List α) : splitOnP p (xs ++ sep :: as) = xs :: splitOnP p as

theorem List.splitOn_eq_splitOnP {α : Type u_1} [BEq α] {x : α} {xs : List α} : splitOn x xs = splitOnP (fun (x_1 : α) => x_1 == x) xs

@[simp]

theorem List.splitOn_ne_nil {α : Type u_1} [BEq α] (a : α) (xs : List α) : splitOn a xs ≠ []

theorem List.splitOn_cons_eq_ite_modifyHead {α : Type u_1} [BEq α] {a : α} (x : α) (xs : List α) : splitOn a (x :: xs) = if (x == a) = true then [] :: splitOn a xs else modifyHead (cons x) (splitOn a xs)

@[deprecated List.splitOn_cons_eq_ite_modifyHead (since := "2026-07-21")]

theorem List.splitOn_cons_eq_if_modifyHead {α : Type u_1} [BEq α] {a : α} (x : α) (xs : List α) : splitOn a (x :: xs) = if (x == a) = true then [] :: splitOn a xs else modifyHead (cons x) (splitOn a xs)

theorem List.splitOn_eq_singleton_of_beq_eq_false {α : Type u_1} {xs : List α} [BEq α] {a : α} (h : ∀ (x : α), x ∈ xs → (x == a) = false) : splitOn a xs = [xs]

If no element satisfies p in the list xs, then xs.splitOnP p = [xs]

theorem List.splitOn_eq_singleton {α : Type u_1} {xs : List α} [BEq α] [LawfulBEq α] {a : α} (h : ¬a ∈ xs) : splitOn a xs = [xs]

theorem List.splitOn_append_cons_of_beq {α : Type u_1} [BEq α] {a : α} (xs as : List α) {sep : α} (hsep : (sep == a) = true) : splitOn a (xs ++ sep :: as) = splitOn a xs ++ splitOn a as

When a list of the form [...xs, sep, ...as] is split at the sep element equal to a, the result is the concatenation of splitOnP called on xs and as

theorem List.splitOn_append_cons_self {α : Type u_1} [BEq α] [ReflBEq α] {a : α} (xs as : List α) : splitOn a (xs ++ a :: as) = splitOn a xs ++ splitOn a as

When a list of the form [...xs, sep, ...as] is split at a, the result is the concatenation of splitOnP called on xs and as

theorem List.splitOn_append_cons_of_forall_mem_beq_eq_false {α : Type u_1} {xs : List α} [BEq α] {a : α} (h : ∀ (x : α), x ∈ xs → (x == a) = false) (sep : α) (hsep : (sep == a) = true) (as : List α) : splitOn a (xs ++ sep :: as) = xs :: splitOn a as

When a list of the form [...xs, sep, ...as] is split at a, the first element is xs, assuming no element in xs is equal to a but sep is equal to a.

theorem List.splitOn_append_cons_self_of_not_mem {α : Type u_1} {xs : List α} [BEq α] [LawfulBEq α] {a : α} (h : ¬a ∈ xs) (as : List α) : splitOn a (xs ++ a :: as) = xs :: splitOn a as

When a list of the form [...xs, a, ...as] is split at a, the first element is xs, assuming no element in xs is equal to a.

@[simp]

theorem List.intercalate_splitOn {α : Type u_1} {xs : List α} [BEq α] [LawfulBEq α] (x : α) : [x].intercalate (splitOn x xs) = xs

intercalate [x] is the left inverse of splitOn x

theorem List.splitOn_intercalate {α : Type u_1} {ls : List (List α)} [BEq α] [LawfulBEq α] (x : α) (hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l) (hls : ls ≠ []) : splitOn x ([x].intercalate ls) = ls

splitOn x is the left inverse of intercalate [x], on the domain consisting of each nonempty list of lists ls whose elements do not contain x