n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ sum (take i c.blocks) = n
n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ sizeUpTo c i = n
dsimp [sizeUpTo]
case h.e'_2.h.e'_4
n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ take i c.blocks = c.blocks
n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ sum (take i c.blocks) = n
convert c.blocks_sum
no goals
case h.e'_2.h.e'_4
n : ℕ
c : Composition n
i : ℕ
h : length c ≤ i
⊢ take i c.blocks = c.blocks
exact take_all_of_le h