case h
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ filterMap (some ∘ f) l = map f l
α : Type u_1
β : Type u_2
f : α → β
⊢ filterMap (some ∘ f) = map f
funext l
no goals
case h
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ filterMap (some ∘ f) l = map f l
induction l <;> simp [*]