insert_fs — Mathlib

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

Похожие утверждения