English
Inserting into b :: v at index fs(i) yields b :: insert(a,v,i).
Русский
Вставка в позицию fs(i) внутри b :: v даёт b :: insert(a,v,i).
LaTeX
$$$ \mathrm{insert}(a,(b \:: v),\mathrm{fs}(i)) = b \:: \mathrm{insert}(a,v,i). $$$
Lean4
@[simp]
theorem insert_fs (a : α) (b : α) (v : Vector3 α n) (i : Fin2 (n + 1)) : insert a (b :: v) (fs i) = b :: insert a v i :=
funext fun j => by
refine j.cases' (by simp [insert, insertPerm]) fun j => ?_
simp only [insert, insertPerm, succ_eq_add_one, cons_fs]
refine Fin2.cases' ?_ ?_ (insertPerm i j) <;> simp