English
If l1 and l2 are lists with l1[m] = l2[n] (when defined), then erasing the m-th element of l1 and the n-th element of l2 yields lists that are permutation-equivalent if and only if l1 and l2 were permutation-equivalent.
Русский
Если l1[m] и l2[n] определены и равны, то удаление соответствующих элементов по индексам m и n в l1 и l2 даёт списки перестановочно эквивалентные тогда и только тогда, когда сами l1 и l2 переставимы.
LaTeX
$$$\\mathrm{eraseIdx}(l_1,m) \\sim \\mathrm{eraseIdx}(l_2,n) \\;\\Longleftrightarrow\\; l_1 \\sim l_2$$$
Lean4
theorem perm_eraseIdx_of_getElem?_eq {l₁ l₂ : List α} {m n : ℕ} (h : l₁[m]? = l₂[n]?) :
eraseIdx l₁ m ~ eraseIdx l₂ n ↔ l₁ ~ l₂ := by
cases Nat.lt_or_ge m l₁.length with
| inl hm =>
rw [getElem?_eq_getElem hm, eq_comm, getElem?_eq_some_iff] at h
cases h with
| intro hn hnm =>
rw [← perm_cons l₁[m], rel_congr_left (getElem_cons_eraseIdx_perm ..), ← hnm,
rel_congr_right (getElem_cons_eraseIdx_perm ..)]
| inr hm =>
rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]
