English
For any TypeVec α of length n, composing subtypeVal applied to repeatEq α with diagSub yields the diagonal map prod.diag.
Русский
Для любого α типа TypeVec длины n композиция subtypeVal (repeatEq α) с diagSub даёт диагональное отображение prod.diag.
LaTeX
$$\operatorname{subtypeVal}(\operatorname{repeatEq}(\alpha)) \circ \operatorname{diagSub} = \operatorname{prod.diag}$$
Lean4
@[simp]
theorem diag_sub_val {n} {α : TypeVec.{u} n} : subtypeVal (repeatEq α) ⊚ diagSub = prod.diag :=
by
ext i x
induction i with
| fz => simp only [comp, subtypeVal, repeatEq.eq_2, diagSub, prod.diag]
| fs _ i_ih => apply @i_ih (drop α)