English
If x ∉ l, then the map k ↦ l.insertIdx k x is injective on the domain {n | n ≤ length(l)}.
Русский
Если x не содержится в списке l, отображение k ↦ l.insertIdx k x инъективно на множестве {n | n ≤ length(l)}.
LaTeX
$$$\\forall {\\\\alpha} {l : List \\\\alpha} {x : \\\\alpha}, x ∉ l \\\\rightarrow \\mathrm{InjOn} (\\\\lambda k, l.insertIdx k x) {n \\\\mid n ≤ l.length}$$$
Lean4
theorem injOn_insertIdx_index_of_notMem (l : List α) (x : α) (hx : x ∉ l) :
Set.InjOn (fun k => l.insertIdx k x) {n | n ≤ l.length} :=
by
intro n hn m hm h
induction l generalizing n m with
| nil => simp_all [Set.mem_singleton_iff, Set.setOf_eq_eq_singleton, length]
| cons hd tl IH =>
simp only [length, Set.mem_setOf_eq] at hn hm
simp only [mem_cons, not_or] at hx
cases n <;> cases m
· rfl
· simp [hx.left] at h
· simp [Ne.symm hx.left] at h
· simp only [insertIdx_succ_cons, cons.injEq, true_and] at h
rw [Nat.succ_inj]
refine IH hx.right ?_ ?_ h
· simpa [Nat.succ_le_succ_iff] using hn
· simpa [Nat.succ_le_succ_iff] using hm
