English
If there exists an x in l with p x, then find? p l equals some head of the list obtained by dropping elements not satisfying p: l.find? p = some ((l.dropWhile (¬ p)).head (proof of existence)).
Русский
Если существует элемент x в l such что p x, тогда l.find? p равно некоторому head (первому элементу) списка, полученного отбросив элементы, не удовлетворяющие p: l.find? p = some ((l.dropWhile (¬ p)).head доказательство существования)).
LaTeX
$$$$ \\forall l:\\, \\text{List}~\\alpha, \\forall p:\\, \\alpha \\rightarrow \\text{Bool},\\; (\\exists x \\in l, p\\,x) \\implies \\; l.find?\\,p = \\text{some}((l.dropWhile (\\lambda x.\\neg p x)).head (by \\simpa using \\exists.intro x (by assumption)) ). $$$$
Lean4
theorem find?_eq_head_dropWhile_not (h : ∃ x ∈ l, p x) :
l.find? p = some ((l.dropWhile (fun x ↦ !(p x))).head (by simpa using h)) := by
rw [l.find?_eq_head?_dropWhile_not p, ← head_eq_iff_head?_eq_some]
