English
If xs is Nodup and xs ~ ys, then the function List.applyId(xs.zip ys) is injective on α.
Русский
Если xs без повторов и xs эквивалентно ys, то функция List.applyId(xs.zip ys) инъективна.
LaTeX
$$$\forall x,y,\; x \neq y \Rightarrow List.applyId(xs.zip ys) x \neq List.applyId(xs.zip ys) y$$$
Lean4
theorem applyId_injective [DecidableEq α] {xs ys : List α} (h₀ : List.Nodup xs) (h₁ : xs ~ ys) :
Injective.{u + 1, u + 1} (List.applyId (xs.zip ys)) :=
by
intro x y h
by_cases hx : x ∈ xs <;> by_cases hy : y ∈ xs
· rw [List.mem_iff_getElem?] at hx hy
obtain ⟨i, hx⟩ := hx
obtain ⟨j, hy⟩ := hy
suffices some x = some y by injection this
have h₂ := h₁.length_eq
rw [List.applyId_zip_eq h₀ h₂ _ _ _ hx] at h
rw [← hx, ← hy]; congr
apply List.getElem?_inj _ (h₁.nodup_iff.1 h₀)
· symm; rw [h]
rw [← List.applyId_zip_eq] <;> assumption
· rw [← h₁.length_eq]
rw [List.getElem?_eq_some_iff] at hx
obtain ⟨hx, hx'⟩ := hx
exact hx
· rw [← applyId_mem_iff h₀ h₁] at hx hy
rw [h] at hx
contradiction
· rw [← applyId_mem_iff h₀ h₁] at hx hy
rw [h] at hx
contradiction
· rwa [List.applyId_eq_self, List.applyId_eq_self] at h <;> assumption
