Basic properties of List.eraseIdx

List.eraseIdx l k erases k-th element of l : List α. If k ≥ length l, then it returns l.

@[deprecated List.mem_eraseIdx_iff_getElem (since := "2024-06-12")]

theorem List.mem_eraseIdx_iff_get {α : Type u} {x : α} {l : List α} {k : Nat} : x ∈ l.eraseIdx k ↔ ∃ (i : Fin l.length), ↑i ≠ k ∧ l.get i = x

@[deprecated List.mem_eraseIdx_iff_getElem? (since := "2024-06-12")]

theorem List.mem_eraseIdx_iff_get? {α : Type u} {x : α} {l : List α} {k : Nat} : x ∈ l.eraseIdx k ↔ ∃ (i : Nat), i ≠ k ∧ l.get? i = some x