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

State before:
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (join (as :: asss)) = join (map join (as :: asss))
Tactic:
dsimp [join]
State after:
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (as ++ join asss) = join as ++ join (map join asss)

State before:
α : Type u
as : List (List α)
asss : List (List (List α))
⊢ join (as ++ join asss) = join as ++ join (map join asss)
Tactic:
rw [join_append, join_join asss]
State after:
no goals