English
For any a and b, the length of a.gather b equals the length of b.
Русский
Для любых a и b, длина a.gather b равна длине b.
LaTeX
$$$\\mathrm{length}(a \\text{ gather } b) = b.\\mathrm{length}$$$
Lean4
/-- When `a` is a composition of `n` and `b` is a composition of `a.length`, `a.gather b` is the
composition of `n` obtained by gathering all the blocks of `a` corresponding to a block of `b`.
For instance, if `a = [6, 5, 3, 5, 2]` and `b = [2, 3]`, one should gather together
the first two blocks of `a` and its last three blocks, giving `a.gather b = [11, 10]`. -/
def gather (a : Composition n) (b : Composition a.length) : Composition n
where
blocks := (a.blocks.splitWrtComposition b).map sum
blocks_pos := by
rw [forall_mem_map]
intro j hj
suffices H : ∀ i ∈ j, 1 ≤ i from
calc
0 < j.length := length_pos_of_mem_splitWrtComposition hj
_ ≤ j.sum := length_le_sum_of_one_le _ H
intro i hi
apply a.one_le_blocks
rw [← a.blocks.flatten_splitWrtComposition b]
exact mem_flatten_of_mem hj hi
blocks_sum := by rw [← sum_flatten, flatten_splitWrtComposition, a.blocks_sum]
