English
The first true index exists exactly when some index satisfies p.
Русский
Первый истинный индекс существует тогда и только тогда, когда существует индекс, удовлетворяющий p.
LaTeX
$$$$ \text{find p isSome} \iff \exists i, p i $$$$
Lean4
/-- `find p` does not return `none` if and only if `p i` holds at some index `i`. -/
theorem isSome_find_iff : ∀ {n : ℕ} {p : Fin n → Prop} [DecidablePred p], (find p).isSome ↔ ∃ i, p i
| 0, _, _ => iff_of_false (fun h ↦ Bool.noConfusion h) fun ⟨i, _⟩ ↦ Fin.elim0 i
| n + 1, p, _ =>
⟨fun h ↦ by
rw [Option.isSome_iff_exists] at h
obtain ⟨i, hi⟩ := h
exact ⟨i, find_spec _ hi⟩, fun ⟨⟨i, hin⟩, hi⟩ ↦ by
dsimp [find]
rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | j
· split_ifs with hl
· exact Option.isSome_some
· have :=
(@isSome_find_iff n (fun x ↦ p (x.castLT (Nat.lt_succ_of_lt x.2))) _).2
⟨⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ hin) fun h ↦ by cases h; exact hl hi⟩, hi⟩
rw [h] at this
exact this
· simp⟩
