English
InsertNth(i, x, p) is the new tuple obtained by inserting x at position i into the tuple with tail p, where the value at i is x and the rest are given by p via succAbove.
Русский
InsertNth(i, x, p) — это новый кортеж, полученный путем вставки x на позицию i в кортеж с хвостом p; на позиции i стоит x, а остальные значения задаются через succAbove.
LaTeX
$$$insertNth(i, x, p) = j \mapsto succAboveCases(i, x, p)\, j.$$$
Lean4
/-- Insert an element into a tuple at a given position. For `i = 0` see `Fin.cons`,
for `i = Fin.last n` see `Fin.snoc`. See also `Fin.succAboveCases` for a version elaborated
as an eliminator. -/
def insertNth (i : Fin (n + 1)) (x : α i) (p : ∀ j : Fin n, α (i.succAbove j)) (j : Fin (n + 1)) : α j :=
succAboveCases i x p j
