theorem List.getElem?_eraseIdx {α : Type u_1} (l : List α) (i : Nat) (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 : Nat) (j : Nat) (h : j < i) : (l.eraseIdx i)[j]? = l[j]?

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

theorem List.getElem_eraseIdx {α : Type u_1} (l : List α) (i : Nat) (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 : Nat) (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 : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : i ≤ j) : (l.eraseIdx i)[j] = l[j + 1]