English
For f: Fin (succ n) → α, the list of f equals the concatenation of the list formed from i.castSucc and the last element f(last n).
Русский
Для f: Fin(n+1) → α списку f соответствует конкатенация списка, полученного через i.castSucc, и последнего элемента f(last n).
LaTeX
$$$ \\operatorname{ofFn} f = (\\operatorname{ofFn} (\\lambda i : \\mathrm{Fin} n, f(i.castSucc))).\\text{concat} (f(\\mathrm{Fin.last} \\, n)) $$$
Lean4
theorem ofFn_succ' {n} (f : Fin (succ n) → α) : ofFn f = (ofFn fun i => f (Fin.castSucc i)).concat (f (Fin.last _)) :=
by
induction n with
| zero => rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero, Fin.last_zero]
| succ n IH =>
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero, Fin.succ_last]
simp only [succ_eq_add_one, Fin.castSucc_succ]
