English
An auxiliary lemma for associativity of composition of formal multilinear series, expressing how to split the size up to two nested blocks.
Русский
Вспомогенная лемма для ассоциативности композиции формальных многочленных рядов, выражающая разбиение размера до двух вложенных блоков.
LaTeX
$$$sizeUpTo a (sizeUpTo b i + j) = sizeUpTo (a.gather b) i + sizeUpTo (sigmaCompositionAux b) j$$$
Lean4
theorem blocksFun_sigmaCompositionAux (a : Composition n) (b : Composition a.length) (i : Fin b.length)
(j : Fin (blocksFun b i)) :
blocksFun (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ i.2⟩)
⟨j, (length_sigmaCompositionAux a b i).symm ▸ j.2⟩ =
blocksFun a (embedding b i j) :=
by
unfold sigmaCompositionAux
rw [blocksFun, get_eq_getElem, getElem_of_eq (getElem_splitWrtComposition _ _ _ _), getElem_drop, getElem_take]; rfl
