English
The result of List.find? on the list List.ofFn f with predicate p equals some b iff p b = true and there exists i with f i = b and no earlier element satisfies p.
Русский
Find? на List.ofFn f даёт some b тогда и только тогда, когда p b = true и существует i с f i = b и никакой предыдущий элемент не удовлетворяет p.
LaTeX
$$$ (\\operatorname{List.find}?\\ p\\ (\\operatorname{List.ofFn} f)) = \\text{some } b \\iff p(b) = \\text{true} \\land \\exists i: \\mathrm{Fin}\\ n, f i = b \\land \\forall j < i, \\neg (p (f j) = \\text{true}) $$$
Lean4
theorem find?_ofFn_eq_some {n} {f : Fin n → α} {p : α → Bool} {b : α} :
(ofFn f).find? p = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬(p (f j) = true) :=
by
rw [find?_eq_some_iff_getElem]
exact
⟨fun ⟨hpb, i, hi, hfb, h⟩ ↦
⟨hpb, ⟨⟨i, length_ofFn (f := f) ▸ hi⟩, by simpa using hfb, fun j hj ↦ by simpa using h j hj⟩⟩,
fun ⟨hpb, i, hfb, h⟩ ↦
⟨hpb,
⟨i, (length_ofFn (f := f)).symm ▸ i.isLt, by simpa using hfb, fun j hj ↦ by
simpa using h ⟨j, by cutsat⟩ (by simpa using hj)⟩⟩⟩
