English
Intercalating a single element x with a list of lists ls and then splitting on x recovers the original lists when x does not appear inside any elements of ls.
Русский
Вставка элемента x между списками ls и последующая разбивка по x восстанавливают исходные списки, если x не встречается внутри элементов ls.
LaTeX
$$$\\forall {\\alpha} (x: \\alpha) [DecidableEq\\alpha] (ls: \\mathrm{List}(\\mathrm{List}(\\alpha)))\\; (\\forall l \\in ls, x \\notin l) \\Rightarrow ([x].intercalate ls).splitOn x = ls$$$
Lean4
/-- `intercalate [x]` is the left inverse of `splitOn x` -/
theorem intercalate_splitOn (x : α) [DecidableEq α] : [x].intercalate (xs.splitOn x) = xs :=
by
simp only [intercalate, splitOn]
induction xs with
| nil => simp [flatten]
| cons hd tl ih => ?_
rcases h' : splitOnP (· == x) tl with - | ⟨hd', tl'⟩; · exact (splitOnP_ne_nil _ tl h').elim
rw [h'] at ih
rw [splitOnP_cons]
split_ifs with h
· rw [beq_iff_eq] at h
subst h
simp [ih, flatten, h']
cases tl' <;> simpa [flatten, h'] using ih
