β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ filterMap (fun x => Option.filter p ((some ∘ f) x)) l =
    filterMap (fun x => if (p ∘ f) x = true then (some ∘ f) x else none) l
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ filter p (map f l) = map f (filter (p ∘ f) l)
rw [← filterMap_eq_map, filter_filterMap, filterMap_filter]
no goals
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ filterMap (fun x => Option.filter p ((some ∘ f) x)) l =
    filterMap (fun x => if (p ∘ f) x = true then (some ∘ f) x else none) l
rfl