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