English
Let i be an index in Fin(n+1), an element x in α, and p a function Fin n → α. Then inserting x at position i into p and then reversing the index order is the same as first reversing i and applying the insertion to the reversed tail, i.e. (Fin.insertNth i x p) ∘ Fin.rev = Fin.insertNth (Fin.rev i) x (p ∘ Fin.rev).
Русский
Пусть i — индекс из Fin(n+1), x ∈ α, и p:Fin n → α. Тогда вставка x на позиции i в p, после чего развернуть порядок индексов, равна вставке x на позиции rev i в хвосте p после разворота: (Fin.insertNth i x p) ∘ Fin.rev = Fin.insertNth (Fin.rev i) x (p ∘ Fin.rev).
LaTeX
$$$$(\mathrm{Fin.insertNth}\, i\, x\, p) \circ \mathrm{Fin.rev} = \mathrm{Fin.insertNth}(\mathrm{Fin.rev}\, i)\, x\ (p \circ \mathrm{Fin.rev})$$$$
Lean4
theorem insertNth_comp_rev {α} (i : Fin (n + 1)) (x : α) (p : Fin n → α) :
(Fin.insertNth i x p) ∘ Fin.rev = Fin.insertNth (Fin.rev i) x (p ∘ Fin.rev) :=
by
funext x
apply insertNth_rev
