English
Let h be a natural equality h: n = m and i ∈ Fin n. The image of the interval Iic(i) under Fin.cast h is Iic(i.cast h).
Русский
Пусть h : n = m и i ∈ Fin n. Образ Iic(i) при приведении Fin.cast h равен Iic(i.cast h).
LaTeX
$$$$ \operatorname{Finset.image}(\operatorname{Fin.cast} h)(\operatorname{Finset.Iic}(i)) = \operatorname{Finset.Iic}(\operatorname{Fin.cast} h\, i) $$$$
Lean4
@[simp]
theorem finsetImage_cast_Iic (h : n = m) (i : Fin n) : (Iic i).image (.cast h) = Iic (i.cast h) := by simp [← coe_inj]