English
Let r be a transitive relation on α. If as is a sublist of bs and bs is sorted with respect to r, then the list obtained by inserting x into as is a sublist of the list obtained by inserting x into bs: orderedInsert r x as <+ orderedInsert r x bs.
Русский
Пусть r — транзитивное отношение на α. Если as является подпоследовательностью bs и bs упорядочено относительно r, то вставка x в as образует подпоследовательность к вставке x в bs: orderedInsert r x as <+ orderedInsert r x bs.
LaTeX
$$$ as <+ bs \\ \\wedge\\ bs.Sorted r \\Rightarrow orderedInsert r x as <+ orderedInsert r x bs $$$
Lean4
theorem orderedInsert_sublist [IsTrans α r] {as bs} (x) (hs : as <+ bs) (hb : bs.Sorted r) :
orderedInsert r x as <+ orderedInsert r x bs := by
cases as with
| nil => simp
| cons a as =>
cases bs with
| nil => contradiction
| cons b bs =>
unfold orderedInsert
cases hs <;> split_ifs with hr
· exact .cons₂ _ <| .cons _ ‹a :: as <+ bs›
· have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
simp only [hr, orderedInsert, ite_true] at ih
exact .trans ih <| .cons _ (.refl _)
· have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)
exact absurd (trans_of _ ‹r x b› hba) hr
· have ih := orderedInsert_sublist x ‹a :: as <+ bs› hb.of_cons
rw [orderedInsert, if_neg hr] at ih
exact .cons _ ih
· simp_all only [sorted_cons, cons_sublist_cons]
· exact .cons₂ _ <| orderedInsert_sublist x ‹as <+ bs› hb.of_cons
