English
If two compositions have the same total n, the same blocks sequence, and identical index components, then their blocksFun values agree at corresponding indices: c1.blocksFun i1 = c2.blocksFun i2.
Русский
Если две композиции имеют одинаковую сумму n, одинаковую последовательность блоков и одинаковые индексы, то их значения blocksFun совпадают: c1.blocksFun i1 = c2.blocksFun i2.
LaTeX
$$$ c_1.blocksFun i_1 = c_2.blocksFun i_2 $ given equalities of n, blocks and index components$$
Lean4
theorem blocksFun_congr {n₁ n₂ : ℕ} (c₁ : Composition n₁) (c₂ : Composition n₂) (i₁ : Fin c₁.length)
(i₂ : Fin c₂.length) (hn : n₁ = n₂) (hc : c₁.blocks = c₂.blocks) (hi : (i₁ : ℕ) = i₂) :
c₁.blocksFun i₁ = c₂.blocksFun i₂ := by
cases hn
rw [← Composition.ext_iff] at hc
cases hc
congr
rwa [Fin.ext_iff]
