English
The left projection composed with the diagonal equals the identity: fst ∘ diag = id.
Русский
Левая проекция, составленная с диагонализацией, равна тождественному отображению: fst ∘ diag = id.
LaTeX
$$$\\mathrm{fst} \\circ \\mathrm{diag} = \\mathrm{id}$$$
Lean4
theorem fst_diag {α : TypeVec n} : TypeVec.prod.fst ⊚ (prod.diag : α ⟹ _) = id := by funext i;
induction i with
| fz => rfl
| fs _ i_ih => apply i_ih