English
Snoc with rotation equals cons rotated: Fin.snoc(v,a) = Fin.cons(a,v,finRotate i).
Русский
Snoc с поворотом равен конструктору cons после поворота: Fin.snoc(v,a) = Fin.cons(a,v,finRotate i).
LaTeX
$$$ \\mathrm{Fin.snoc}\ v\ a = \\lambda i.\\ \\mathrm{Fin.cons}\\ a\\ v\\ (\\mathrm{finRotate}\\ i)$$$
Lean4
theorem snoc_eq_cons_rotate {α : Type*} (v : Fin n → α) (a : α) :
@Fin.snoc _ (fun _ => α) v a = fun i => @Fin.cons _ (fun _ => α) a v (finRotate _ i) :=
by
ext ⟨i, h⟩
by_cases h' : i < n
· rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
rfl
· have h'' : n = i := by
simp only [not_lt] at h'
exact (Nat.eq_of_le_of_lt_succ h' h).symm
subst h''
rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
rfl
