induction L <;> simp [find?]
β : Type u_1
α : Type u_2
p : β → Bool
f : α → β
L : List α
⊢ find? p (map f L) = Option.map f (find? (p ∘ f) L)
case cons
β : Type u_1
α : Type u_2
p : β → Bool
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : find? p (map f tail✝) = Option.map f (find? (p ∘ f) tail✝)
⊢ (match p (f head✝) with
    | true => some (f head✝)
    | false => find? p (map f tail✝)) =
    Option.map f
      (match p (f head✝) with
      | true => some head✝
      | false => find? (p ∘ f) tail✝)