English
gives a compact encoding for locating a predicate across a finite index set.
Русский
дает компактное кодирование поиска предиката по конечному индексу.
LaTeX
$$$$ \text{find} : \forall n, (\mathrm{Fin}\ n \to \mathrm{Prop}) \to \mathrm{Option}\ (\mathrm{Fin}\ n) $$$$
Lean4
/-- If `find p = some i`, then `p i` holds -/
theorem find_spec : ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p] {i : Fin n} (_ : i ∈ Fin.find p), p i
| 0, _, _, _, hi => Option.noConfusion hi
| n + 1, p, I, i, hi => by
rw [find] at hi
rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | j
· rw [h] at hi
dsimp at hi
split_ifs at hi with hl
· simp only [Option.mem_def, Option.some.injEq] at hi
exact hi ▸ hl
· exact (Option.not_mem_none _ hi).elim
· rw [h] at hi
dsimp at hi
rw [← Option.some_inj.1 hi]
exact @find_spec n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _ _ h
