assumption
case cons.h_1.head
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
x : α✝¹
ys : List α✝¹
ih : List.filterMap f ys = [] → x ∈ ys → f x = none
x✝ : Option α✝
h : List.filterMap f ys = []
heq✝ : f x = none
⊢ f x = none
no goals