Theorem: List.find?_map (LeanSAT/Upstream/ToStd.lean)

State before:
β : Type u_1
α : Type u_2
p : β → Bool
f : α → β
L : List α
⊢ find? p (map f L) = Option.map f (find? (p ∘ f) L)
Tactic:
induction L <;> simp [find?]
State after:
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✝)

State before:
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✝)
Tactic:
split <;> simp [*]
State after:
no goals