English
Let M be a commutative monoid. For natural numbers n,m with h : n = m, and a,b ∈ Fin n, and f : Fin m → M, the product of f over the interval from a.cast h to b.cast h equals the product of f composed with cast h over the interval from a to b:
Русский
Пусть M — коммутативный моноид. Для произвольных n,m и равенства h : n = m, а и b ∈ Fin n и f : Fin m → M выполняется: произведение по интервалу uIcc(a.cast h, b.cast h) от f равно произведению по интервалу uIcc(a, b) от f(i.cast h).
LaTeX
$$$\\displaystyle \\prod_{i \\in \\mathrm{uIcc}(a^{\\mathrm{cast}(h)},\, b^{\\mathrm{cast}(h)})} f(i) = \\prod_{i \\in \\mathrm{uIcc}(a, b)} f(i^{\\mathrm{cast}(h)})$$$
Lean4
@[to_additive]
theorem prod_uIcc_cast (h : n = m) (f : Fin m → M) (a b : Fin n) :
∏ i ∈ uIcc (a.cast h) (b.cast h), f i = ∏ i ∈ uIcc a b, f (i.cast h) := by simp [← map_finCongr_uIcc]
