English
Let p be a predicate on Fin n with decidable truth. If there exists an element i in Fin n such that p i holds, then the finite index corresponding to the least such i (as produced by the natural-number minimization) is a member of Fin.find p. In particular, the witness ⟨Nat.find h, (Nat.find_spec h).fst⟩ satisfies p and lies in the set of indices found by Fin.find.
Русский
Пусть p — предикат на Fin n с разрешимостью. Если существует элемент i из Fin n, такой что p i истинно, тогда наименьшее такое i (получаемое через Nat.find) образует элемент ⟨Nat.find h, (Nat.find_spec h).fst⟩, который принадлежит Fin.find p и удовлетворяет p.
LaTeX
$$$\\text{If } h : \\exists i : Fin n, p i, \\text{ then } \\big( \\langle Nat.find h, (Nat.find_spec h).fst \\rangle : Fin n \\big) \\in Fin.find p.$$$
Lean4
theorem nat_find_mem_find {p : Fin n → Prop} [DecidablePred p] (h : ∃ i, ∃ hin : i < n, p ⟨i, hin⟩) :
(⟨Nat.find h, (Nat.find_spec h).fst⟩ : Fin n) ∈ find p :=
by
let ⟨i, hin, hi⟩ := h
rcases hf : find p with - | f
· rw [find_eq_none_iff] at hf
exact (hf ⟨i, hin⟩ hi).elim
· refine Option.some_inj.2 (Fin.le_antisymm ?_ ?_)
· exact find_min' hf (Nat.find_spec h).snd
· exact Nat.find_min' _ ⟨f.2, by convert find_spec p hf⟩
