no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
l : List α
⊢ map g (filterMap f l) = filterMap (fun x => Option.map g (f x)) l
simp only [← filterMap_eq_map, filterMap_filterMap, Option.map_eq_bind]