English
If a list is of the form [... xs, sep, ... as] where no element of xs satisfies p but sep does, then (xs ++ sep :: as).splitOnP p = xs :: as.splitOnP p.
Русский
Если список имеет вид [... xs, sep, ... as], где элементы xs не удовлетворяют p, но sep удовлетворяет p, то (xs ++ sep :: as).splitOnP p = xs :: as.splitOnP p.
LaTeX
$$$\\forall {\\alpha} (p: \\alpha \\to \\mathrm{Bool}) (xs: \\mathrm{List}(\\alpha)) (sep: \\alpha) (as: \\mathrm{List}(\\alpha))\\; (\\forall x \\in xs, \\neg p(x)) \\Rightarrow p(sep) \\Rightarrow (xs ++ sep :: as).splitOnP p = xs :: as.splitOnP p$$$
Lean4
/-- 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` -/
theorem splitOnP_first (h : ∀ x ∈ xs, ¬p x) (sep : α) (hsep : p sep) (as : List α) :
(xs ++ sep :: as).splitOnP p = xs :: as.splitOnP p := by
induction xs with
| nil => simp [hsep]
| cons hd tl ih => simp [h hd _, ih <| forall_mem_of_forall_mem_cons h]
