no goals
n : ℕ
α : Type u_1
L : List (List α)
c : Composition (length (join L))
h : map length L = c.blocks
⊢ splitWrtComposition (join L) c = L
simp only [eq_self_iff_true, and_self_iff, eq_iff_join_eq, join_splitWrtComposition,
  map_length_splitWrtComposition, h]