English
When inserting at the last position, the result equals a Snoc with a cast: (last n).insertNth x p = snoc (cast ... (p j)) x.
Русский
При вставке в последнюю позицию результат равен snoc с приведением: (last n).insertNth x p = snoc (cast ... (p j)) x.
LaTeX
$$$(Fin.last\ n).insertNth x p = snoc (\lambda j. cast\;⋯\; (p\ j))\ x$$
Lean4
theorem insertNth_last (x : α (last n)) (p : ∀ j : Fin n, α ((last n).succAbove j)) :
insertNth (last n) x p = snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x :=
by
refine insertNth_eq_iff.2 ⟨by simp, ?_⟩
ext j
apply eq_of_heq
trans snoc (fun j ↦ _root_.cast (congr_arg α (succAbove_last_apply j)) (p j)) x j.castSucc
· rw [snoc_castSucc]
exact (cast_heq _ _).symm
· apply congr_arg_heq
rw [succAbove_last]
