English
For any i, a, f, and j, inserting at i and then reversing corresponds to inserting at i.rev with f composed with rev: i.insertNth a f j.rev = i.rev.insertNth a (f ∘ rev) j.
Русский
Для любых i, a, f и j вставка на i и разворот соответствует вставке на i.rev с f, композиции с rev: i.insertNth a f j.rev = i.rev.insertNth a (f ∘ rev) j.
LaTeX
$$∀ {i a f j}, i.insertNth a f j.rev = i.rev.insertNth a (Function.comp f Fin.rev) j$$
Lean4
theorem insertNth_rev {α : Sort*} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)) :
insertNth (α := fun _ ↦ α) i a f (rev j) = insertNth (α := fun _ ↦ α) i.rev a (f ∘ rev) j :=
by
induction j using Fin.succAboveCases
· exact rev i
· simp
· simp [rev_succAbove]
