simp [-quot_mk_to_coe, find?]
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ find? f ⟦L⟧ h = some x ↔ x ∈ ⟦L⟧ ∧ f x = true
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ ⟦L⟧ ∧ f x = true