English
Updating the last element of a Fin-tuple does not change its beginning.
Русский
Обновление последнего элемента кортежа Fin не изменяет его префикс.
LaTeX
$$$\\\\operatorname{init}(\\\\operatorname{update} q(\\\\mathrm{last} \\\\; n) z) = \\\\operatorname{init} q$$$
Lean4
/-- Updating the last element of a tuple does not change the beginning. -/
@[simp]
theorem init_update_last : init (update q (last n) z) = init q :=
by
ext j
simp [init, Fin.ne_of_lt]