English
If there exists an order-preserving embedding f: ℕ ↪o ℕ such that for every index the corresponding elements agree, then l is a sublist of l'.
Русский
Если существует невозрастающее отображение f: ℕ ↪o ℕ, сохраняющее порядок по элементах списка, и элементы списка l совпадают с элементами l' по этому отображению, то l является подсписком l'.
LaTeX
$$$ \\exists f:\\, \\mathbb{N} \\hookrightarrow_o \\mathbb{N},\\forall n, l[n]? = l'[f(n)]? \\Rightarrow l <+ l'. $$$
Lean4
/-- If there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`,
then `Sublist l l'`.
-/
theorem sublist_of_orderEmbedding_getElem?_eq {l l' : List α} (f : ℕ ↪o ℕ) (hf : ∀ ix : ℕ, l[ix]? = l'[f ix]?) :
l <+ l' :=
by
induction l generalizing l' f with
| nil => simp
| cons hd tl IH => ?_
have : some hd = l'[f 0]? := by simpa using hf 0
rw [eq_comm, List.getElem?_eq_some_iff] at this
obtain ⟨w, h⟩ := this
let f' : ℕ ↪o ℕ :=
OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b =>
by
dsimp only
rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
exact b.succ_pos
have : ∀ ix, tl[ix]? = (l'.drop (f 0 + 1))[f' ix]? := by
intro ix
rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
simp only [getElem?_cons_succ]
rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
exact ix.succ_pos
rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
apply List.Sublist.append _ (IH _ this)
rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]
exact List.getElem_mem _
