English
Appending after snoc (left side) is equivalent to appending xs with cons x ys, up to a cast isomorphism.
Русский
Добавление слева после snoc эквивалентно добавлению xs с cons x ys с приведением к соответствующей размерности.
LaTeX
$$$\\\\operatorname{append}(\\\\operatorname{snoc} xs x) ys = (\\\\operatorname{append} xs (\\\\operatorname{cons} x ys)) \\\\circ \\\\operatorname{cast} (\\\\mathrm{Nat.succ\_add\_eq\_add\_succ} \\, \\, ..)$$$
Lean4
theorem append_left_snoc {n m} {α : Sort*} (xs : Fin n → α) (x : α) (ys : Fin m → α) :
Fin.append (Fin.snoc xs x) ys = Fin.append xs (Fin.cons x ys) ∘ Fin.cast (Nat.succ_add_eq_add_succ ..) := by
rw [snoc_eq_append, append_assoc, append_left_eq_cons, append_cast_right]; rfl
