English
Inserting two elements a and b at positions i and j (i ≤ j) in a vector v commutes up to a cast: (v.insertIdx a i).insertIdx b j.succ = (v.insertIdx b j).insertIdx a (Fin.castSucc i).
Русский
Вставки двух элементов a и b по позициям i и j (i ≤ j) коммутируют с корректировкой индексов: (v.insertIdx a i).insertIdx b j.succ = (v.insertIdx b j).insertIdx a (Fin.castSucc i).
LaTeX
$$$ (v.insertIdx\\ a\\ i).insertIdx\\ b\\ j.\\succ = (v.insertIdx\\ b\\ j).insertIdx\\ a\\ (Fin.castSucc\\ i) $$$
Lean4
/-- Erasing an element after inserting an element, at different indices. -/
theorem eraseIdx_insertIdx' {v : Vector α (n + 1)} :
∀ {i : Fin (n + 1)} {j : Fin (n + 2)},
eraseIdx (j.succAbove i) (insertIdx a j v) = insertIdx a (i.predAbove j) (eraseIdx i v)
| ⟨i, hi⟩, ⟨j, hj⟩ => by
dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]
rw [Subtype.mk_eq_mk]
simp only [Fin.lt_iff_val_lt_val]
split_ifs with hij
· rcases Nat.exists_eq_succ_of_ne_zero (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
rw [← List.insertIdx_eraseIdx_of_ge]
· simp; rfl
· simpa
· simpa [Nat.lt_succ_iff] using hij
· dsimp
rw [← List.insertIdx_eraseIdx_of_le]
· rfl
· simpa
· simpa [not_lt] using hij
