English
Let l be a list of elements of α, and let x,y ∈ l. Then idxOf x l = idxOf y l if and only if x = y.
Русский
Пусть l — список элементов α, и x, y ∈ l. Тогда idxOf x l = idxOf y l эквивалентно x = y.
LaTeX
$$$\\\\forall l:\\\\, \\text{List }\\\\alpha, \\\\forall x,y \\\\in l, \\\\operatorname{idxOf}(x,l) = \\\\operatorname{idxOf}(y,l) \\\\iff x = y.$$$
Lean4
theorem idxOf_inj [DecidableEq α] {l : List α} {x y : α} (hx : x ∈ l) (hy : y ∈ l) : idxOf x l = idxOf y l ↔ x = y :=
⟨fun h =>
by
have x_eq_y : get l ⟨idxOf x l, idxOf_lt_length_iff.2 hx⟩ = get l ⟨idxOf y l, idxOf_lt_length_iff.2 hy⟩ := by
simp only [h]
simp only [idxOf_get] at x_eq_y; exact x_eq_y, fun h => by subst h; rfl⟩
