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