m n✝ n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ¬Option.isSome (find fun x => p x) = true
m n✝ n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ∀ (i : Fin n), ¬p i
rw [← not_exists, ← isSome_find_iff]
no goals
m n✝ n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ find p = none ↔ ¬Option.isSome (find fun x => p x) = true
cases find p <;> simp