English
The initialization map on a last-n element matches the last component after applying the initialization to a tuple; init_def states this equality by rfl.
Русский
Инициализация для последнего элемента совпадает с последним компонентом после применения инициализации; init_def формулируется как равенство, тривиальное.
LaTeX
$$$\\mathrm{init}\\ (\lambda k. q\\ k) = \\lambda k. q\\ k.castSucc$$$
Lean4
@[simp]
theorem snoc_comp_natAdd {n m : ℕ} {α : Sort*} (f : Fin (m + n) → α) (a : α) :
(snoc f a : Fin _ → α) ∘ (natAdd m : Fin (n + 1) → Fin (m + n + 1)) = snoc (f ∘ natAdd m) a :=
by
ext i
refine Fin.lastCases ?_ (fun i ↦ ?_) i
· simp only [Function.comp_apply]
rw [snoc_last, natAdd_last, snoc_last]
· simp only [comp_apply, snoc_castSucc]
rw [natAdd_castSucc, snoc_castSucc]
