English
Let hr be that c is pairwise r-related and hc that c is a sublist of l. Then c is a sublist of insertionSort r l.
Русский
Пусть hr обозначает, что c попарно связано отношением r, и hc, что c является подпоследовательностью к l. Тогда c является подпоследовательностью к insertionSort r l.
LaTeX
$$$ c.Pairwise\\ r \\wedge c <+ l \\Rightarrow c <+ insertionSort r l $$$
Lean4
/-- If `c` is a sorted sublist of `l`, then `c` is still a sublist of `insertionSort r l`.
-/
theorem sublist_insertionSort {l c : List α} (hr : c.Pairwise r) (hc : c <+ l) : c <+ insertionSort r l := by
induction l generalizing c with
| nil => simp_all only [sublist_nil, insertionSort, Sublist.refl]
| cons _ _ ih =>
cases hc with
| cons _ h => exact ih hr h |>.trans (sublist_orderedInsert ..)
| cons₂ _ h =>
obtain ⟨hr, hp⟩ := pairwise_cons.mp hr
exact cons_sublist_orderedInsert (ih hp h) hr
