map filter_map join

Stream: new members

[Martin Dvořák]

I am confused. Does my example hold?

example (a : list (list ℤ)) (f : ℤ → option ℕ) :
  (list.map (list.filter_map f) a).join =
    list.filter_map f a.join :=
begin
  sorry
end

[Eric Rodriguez]

import data.list.join

example {α β} (l : list $ list α) (f : α → option β) :
  (l.map (list.filter_map f)).join = l.join.filter_map f :=
begin
  induction l with h tl ih,
  { simp },
  { simp [list.filter_map_append, ih] },
end

[Martin Dvořák]

Don't we want to add it to mathlib alongside with the following theorem?

@[simp] theorem map_join (f : α → β) (L : list (list α)) :
  map f (join L) = join (map (map f) L) :=
by induction L; [refl, simp only [*, join, map, map_append]]

[Notification Bot]

Martin Dvořák has marked this topic as unresolved.

[Eric Wieser]

I don't know if the direction of those lemmas is right or whether they should be simp, but we should certainly have them in some form

[Martin Dvořák]

I am sorry for using a wrong word. The theorem map_join already exists in mathlib. I would like to add only one new theorem.

[Martin Dvořák]

Lemme PR it.

[Martin Dvořák]

https://github.com/leanprover-community/mathlib/pull/14777

[Martin Dvořák]

Should I move it to data/list/join as suggested?