n : ℕ
c : Composition n
⊢ ∀ (x : Fin (length c + 1)), ↑(boundary c) x ∈ boundaries c
n : ℕ
c : Composition n
⊢ Finset.orderEmbOfFin (boundaries c) (_ : Finset.card (boundaries c) = length c + 1) = boundary c
refine' (Finset.orderEmbOfFin_unique' _ _).symm
no goals
n : ℕ
c : Composition n
⊢ ∀ (x : Fin (length c + 1)), ↑(boundary c) x ∈ boundaries c
exact fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)