induction xs with
| nil => contradiction
| cons y ys ih =>
  simp [List.filterMap] at h
  split at h
  . cases hx with
    | head => assumption
    | tail _ hmem => exact ih h hmem
  . contradiction
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
xs : List α✝¹
h : List.filterMap f xs = []
x : α✝¹
hx : x ∈ xs
⊢ f x = none
no goals