English
Let i be an index in Fin(n+1) and x be an element of the fiber α(i). Then inserting x at position i with the value 1 in all other coordinates yields the function that is x at i and 1 at every other coordinate.
Русский
Пусть i ∈ Fin(n+1) и x ∈ α(i). Тогда вставка x в позицию i при значении 1 на всех остальных координатах даёт функцию, которая принимает значение x в координате i и единицу на остальных координатах.
LaTeX
$$$ i.insertNth x 1 = \lambda j. \begin{cases} x, & j = i\\ 1, & j \neq i \end{cases} $$$
Lean4
@[to_additive (attr := simp)]
theorem insertNth_one_right [∀ j, One (α j)] (i : Fin (n + 1)) (x : α i) : i.insertNth x 1 = Pi.mulSingle i x :=
insertNth_eq_iff.2 <| by unfold removeNth; simp [succAbove_ne, Pi.one_def]
