theorem List.getElem?_eraseIdx {α : Type u_1} (l : List α) (i j : Nat) : (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]?

theorem List.getElem?_eraseIdx_of_lt {α : Type u_1} (l : List α) (i j : Nat) (h : j < i) : (l.eraseIdx i)[j]? = l[j]?

theorem List.getElem?_eraseIdx_of_ge {α : Type u_1} (l : List α) (i j : Nat) (h : i ≤ j) : (l.eraseIdx i)[j]? = l[j + 1]?

theorem List.getElem_eraseIdx {α : Type u_1} (l : List α) (i j : Nat) (h : j < (l.eraseIdx i).length) : (l.eraseIdx i)[j] = if h' : j < i then l[j] else l[j + 1]

theorem List.getElem_eraseIdx_of_lt {α : Type u_1} (l : List α) (i j : Nat) (h : j < (l.eraseIdx i).length) (h' : j < i) : (l.eraseIdx i)[j] = l[j]

theorem List.getElem_eraseIdx_of_ge {α : Type u_1} (l : List α) (i j : Nat) (h : j < (l.eraseIdx i).length) (h' : i ≤ j) : (l.eraseIdx i)[j] = l[j + 1]

theorem List.eraseIdx_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} : (l.set i a).eraseIdx i = l.eraseIdx i

theorem List.eraseIdx_set_lt {α : Type u_1} {l : List α} {i j : Nat} {a : α} (h : j < i) : (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a

theorem List.eraseIdx_set_gt {α : Type u_1} {l : List α} {i j : Nat} {a : α} (h : i < j) : (l.set i a).eraseIdx j = (l.eraseIdx j).set i a

@[simp]

theorem List.set_getElem_succ_eraseIdx_succ {α : Type u_1} {l : List α} {i : Nat} (h : i + 1 < l.length) : (l.eraseIdx (i + 1)).set i l[i + 1] = l.eraseIdx i

@[simp]

theorem List.eraseIdx_length_sub_one {α : Type u_1} (l : List α) : l.eraseIdx (l.length - 1) = l.dropLast