English
Appending a one-tuple to the right is the same as snoc-ing the single element: append xs x₀ = snoc xs (x₀ 0).
Русский
Добавление единичного кортежа справа эквивалентно snoc: append xs x₀ = snoc xs (x₀ 0).
LaTeX
$$$\\\\operatorname{append} xs x_0 = \\\\operatorname{snoc} xs (x_0 0)$$$
Lean4
/-- Appending a one-tuple to the right is the same as `Fin.snoc`. -/
theorem append_right_eq_snoc {α : Sort*} {n : ℕ} (x : Fin n → α) (x₀ : Fin 1 → α) :
Fin.append x x₀ = Fin.snoc x (x₀ 0) := by
ext i
refine Fin.addCases ?_ ?_ i <;> clear i
· intro i
rw [Fin.append_left]
exact (@snoc_castSucc _ (fun _ => α) _ _ i).symm
· intro i
rw [Subsingleton.elim i 0, Fin.append_right]
exact (@snoc_last _ (fun _ => α) _ _).symm
