English
For a nodup list l and any index i with hi < l.length, idxOf (get l i) l = i.
Русский
Для нодуп списка l и любого индекса i с hi < l.length, idxOf (get l i) l = i.
LaTeX
$$$ [DecidableEq \alpha] \Rightarrow \forall \{l: List\,\alpha\}, Nodup\ l \rightarrow \forall i \ (h: i < l.length), \operatorname{idxOf}(l[i], l) = i $$$
Lean4
theorem idxOf_getElem [DecidableEq α] {l : List α} (H : Nodup l) (i : Nat) (h : i < l.length) : idxOf l[i] l = i :=
suffices (⟨idxOf l[i] l, idxOf_lt_length_iff.2 (getElem_mem _)⟩ : Fin l.length) = ⟨i, h⟩ from Fin.val_eq_of_eq this
nodup_iff_injective_get.1 H
(by simp)
-- This is incorrectly named and should be `idxOf_get`;
-- this already exists, so will require a deprecation dance.
