source
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]?
source
theorem List.getElem?_eraseIdx_of_lt {α : Type u_1} {l : List α} {i j : Nat} (h : j < i) :
(l.eraseIdx i)[j]? = l[j]?
source
theorem List.getElem?_eraseIdx_of_ge {α : Type u_1} {l : List α} {i j : Nat} (h : i ≤ j) :
(l.eraseIdx i)[j]? = l[j + 1]?
source
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]
source
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]
source
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]
source
theorem List.eraseIdx_eq_dropLast {α : Type u_1} {l : List α} {i : Nat} (h : i + 1 = l.length) :
l.eraseIdx i = l.dropLast
source
theorem List.eraseIdx_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} :
(l.set i a).eraseIdx i = l.eraseIdx i
source
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
source
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
source
theorem List.eraseIdx_set {α : Type u_1} {xs : List α} {i : Nat} {a : α} {j : Nat} :
(xs.set i a).eraseIdx j = if j < i then (xs.eraseIdx j).set (i - 1) a else if j = i then xs.eraseIdx i else (xs.eraseIdx j).set i a
source
theorem List.set_eraseIdx_le {α : Type u_1} {xs : List α} {i j : Nat} {a : α} (h : i ≤ j) :
(xs.eraseIdx i).set j a = (xs.set (j + 1) a).eraseIdx i
source
theorem List.set_eraseIdx_gt {α : Type u_1} {xs : List α} {i j : Nat} {a : α} (h : j < i) :
(xs.eraseIdx i).set j a = (xs.set j a).eraseIdx i
source
theorem List.set_eraseIdx {α : Type u_1} {xs : List α} {i j : Nat} {a : α} :
(xs.eraseIdx i).set j a = if i ≤ j then (xs.set (j + 1) a).eraseIdx i else (xs.set j a).eraseIdx i
source
@[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
source
@[simp]
theorem List.eraseIdx_length_sub_one {α : Type u_1} {l : List α} :
l.eraseIdx (l.length - 1) = l.dropLast