English
Appending a one-tuple to the left is the same as Fin.cons: Fin.append x0 x = Fin.cons (x0 0) x ∘ Fin.cast (Nat.add_comm ..).
Русский
Добавление однодительного к началу равно Fin.cons: Fin.append x0 x = Fin.cons (x0 0) x ∘ Fin.cast (Nat.add_comm ..).
LaTeX
$$$\\mathrm{Fin.append}\\;x_0\\;x = \\mathrm{Fin.cons}(x_0(0),x) \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.add\\_comm}()).$$$
Lean4
/-- Appending a one-tuple to the left is the same as `Fin.cons`. -/
theorem append_left_eq_cons {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α) :
Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.cast (Nat.add_comm ..) :=
by
ext i
refine Fin.addCases ?_ ?_ i <;> clear i
· intro i
rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
exact Fin.cons_zero _ _
· intro i
rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
exact Fin.cons_succ _ _ _
