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

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

State before:
α : Type u
as : List α
ass bss : List (List α)
⊢ as ++ join (ass ++ bss) = as ++ join ass ++ join bss
Tactic:
rw [List.append_assoc, join_append ass bss]
State after:
no goals