α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ length (filter (fun b => Option.isSome b) (map f l)) ≤ length (map f l)
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ length (filterMap f l) ≤ length l
rw [← length_map _ some, map_filterMap_some_eq_filter_map_is_some, ← length_map _ f]
no goals
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ length (filter (fun b => Option.isSome b) (map f l)) ≤ length (map f l)
apply length_filter_le