English
A variant formulation of insertIdx_comm with a more explicit match_1_1 pattern, stating the same commutation with explicit finite indices.
Русский
Упрощённая формулировка варианта insertIdx_comm через явное соответствие match_1_1, сохраняющая ту же самую коммутативность вставок.
LaTeX
$$$ insertIdx\\; comm \\; {\\text{...}} $$$
Lean4
theorem insertIdx_comm (a b : α) (i j : Fin (n + 1)) (h : i ≤ j) :
∀ v : Vector α n, (v.insertIdx a i).insertIdx b j.succ = (v.insertIdx b j).insertIdx a (Fin.castSucc i)
| ⟨l, hl⟩ => by
refine Subtype.eq ?_
simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.coe_castAdd]
apply List.insertIdx_comm
· assumption
· rw [hl]
exact Nat.le_of_succ_le_succ j.2
