English
If a predicate p on Fin n is such that any two witnesses for p must be equal, then any witness i with p i holds is contained in Fin.find p; i.e., a unique witness is picked by the minimality inherent in the find operator.
Русский
Если на Fin n предикат p удовлетворяет условию уникальности свидетелей, то любой i с p i принадлежит Fin.find p; то есть минимальный свидетель выбирается через find.
LaTeX
$$$(\\forall i j, p i \\to p j \\to i = j) \\Rightarrow (p i) \\Rightarrow i \\in Fin.find p$$$
Lean4
theorem mem_find_of_unique {p : Fin n → Prop} [DecidablePred p] (h : ∀ i j, p i → p j → i = j) {i : Fin n} (hi : p i) :
i ∈ Fin.find p :=
mem_find_iff.2 ⟨hi, fun j hj ↦ Fin.le_of_eq <| h i j hi hj⟩
