list.map versus list.filter_map

Stream: new members

[Martin Dvořák]

example {α β : Type*} {f : α → option β} {x : list α} {y : list β}
    (hmap : list.map f x = list.map some y) :
  list.filter_map f x = y :=
begin
  sorry,
end

[Eric Wieser]

I think it follows from docs#list.map_filter_map_of_inv with g = id

[Martin Dvořák]

I don't see how it should follow from it.

[Martin Dvořák]

Nevermind. I have proved it myself. Just tell me whether you want the lemma to be added to mathlib.