English
Updating the tail and then cons-ing is the same as cons-ing and then updating the tail's successor: cons x (update p i y) = update (cons x p) i.succ y.
Русский
Обновление хвоста, затем добавление в голову эквивалентно добавлению и последующему обновлению хвоста: cons x (update p i y) = update (cons x p) i.succ y.
LaTeX
$$$\\\\mathrm{cons}(x,\\\\mathrm{update}(p,i,y)) = \\\\mathrm{update}(\\\\mathrm{cons}(x,p),\\\\mathrm{succ}(i),y)$$$
Lean4
/-- Updating a tuple and adding an element at the beginning commute. -/
@[simp]
theorem cons_update : cons x (update p i y) = update (cons x p) i.succ y :=
by
ext j
cases j using Fin.cases <;> simp [Ne.symm, update_apply_of_injective _ (succ_injective _)]
