Theorem: List.map_join (Moncalc/Data/List/Misc.lean)

State before:
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (join (as :: ass)) = join (map (map f) (as :: ass))
Tactic:
dsimp [join]
State after:
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (as ++ join ass) = map f as ++ join (map (map f) ass)

State before:
α : Type u
β : Type v
f : α → β
as : List α
ass : List (List α)
⊢ map f (as ++ join ass) = map f as ++ join (map (map f) ass)
Tactic:
rw [map_append, map_join f (ass:=ass)]
State after:
no goals