English
The operation of adding an element to the end of a finite sequence, when evaluated at the reversed index, matches the operation of prepending the element to the reversed tail at the original index.
Русский
Операция добавления элемента в конец кортежа, взятая по обратному индексу, совпадает с операцией добавления этого элемента в начало развёрнутого хвоста по исходному индексу.
LaTeX
$$$$\mathrm{Fin.snoc}\ f\ a\ i.rev = \mathrm{Fin.cons}\ a\ (\mathrm{f} \circ \mathrm{Fin.rev})\ i$$$$
Lean4
theorem snoc_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
snoc (α := fun _ => α) f a i.rev = cons (α := fun _ => α) a (f ∘ Fin.rev : Fin _ → α) i := by
simpa using insertNth_rev (last n) a f i
