no goals
α : Type u_2
β : Type u_1
γ : Type ?u.281796
p : α → Prop
inst✝ : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun b => decide (p b)) l) = List.filterMap (fun x => if p x then f x else none) l
simpa using List.filterMap_filter p f l