English
If n is a valid index, then erasing the nth element and inserting a at n yields setting the nth element to a.
Русский
Если n допустим, удаление n-го элемента и вставка a на позицию n эквивалентны замене n-го элемента на a.
LaTeX
$$$(l.eraseIdx n).insertIdx n a = l.set n a$$$
Lean4
/-- Erasing `n`th element of a list, then inserting `a` at the same place
is the same as setting `n`th element to `a`.
We assume that `n ≠ length l`, because otherwise LHS equals `l ++ [a]` while RHS equals `l`. -/
@[simp]
theorem insertIdx_eraseIdx_self {l : List α} {n : ℕ} (hn : n ≠ length l) (a : α) :
(l.eraseIdx n).insertIdx n a = l.set n a := by induction n generalizing l <;> cases l <;> simp_all