n : ℕ
c : CompositionAsSet n
this : take (length c) (blocks c) = blocks c
⊢ sum (blocks c) = n
n : ℕ
c : CompositionAsSet n
⊢ sum (blocks c) = n
have : c.blocks.take c.length = c.blocks := take_all_of_le (by simp [blocks])
n : ℕ
c : CompositionAsSet n
this : take (length c) (blocks c) = blocks c
⊢ ↑(Fin.last n) = n
n : ℕ
c : CompositionAsSet n
this : take (length c) (blocks c) = blocks c
⊢ sum (blocks c) = n
rw [← this, c.blocks_partial_sum c.length_lt_card_boundaries, c.boundary_length]
no goals
n : ℕ
c : CompositionAsSet n
this : take (length c) (blocks c) = blocks c
⊢ ↑(Fin.last n) = n
rfl
no goals
n : ℕ
c : CompositionAsSet n
⊢ List.length (blocks c) ≤ length c
simp [blocks]