Lemmas about Vector.eraseIdx.

eraseIdx

theorem Vector.eraseIdx_eq_take_drop_succ {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) : xs.eraseIdx i h = Vector.cast ⋯ (xs.take i ++ xs.drop (i + 1))

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

theorem Vector.getElem?_eraseIdx_of_lt {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) {j : Nat} (h' : j < i) : (xs.eraseIdx i h)[j]? = xs[j]?

theorem Vector.getElem?_eraseIdx_of_ge {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) {j : Nat} (h' : i ≤ j) : (xs.eraseIdx i h)[j]? = xs[j + 1]?

theorem Vector.getElem_eraseIdx {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i < n) {j : Nat} (h' : j < n - 1) : (xs.eraseIdx i h)[j] = if h'' : j < i then xs[j] else xs[j + 1]

theorem Vector.mem_of_mem_eraseIdx {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {h : i < n} {a : α} : a ∈ xs.eraseIdx i h → a ∈ xs

theorem Vector.eraseIdx_append_of_lt_size {α : Type u_1} {n : Nat} {xs : Vector α n} {k : Nat} (hk : k < n) (xs' : Vector α n) (h : k < n + n) : (xs ++ xs').eraseIdx k h = Vector.cast ⋯ (xs.eraseIdx k hk ++ xs')

theorem Vector.eraseIdx_append_of_length_le {α : Type u_1} {n : Nat} {xs : Vector α n} {k : Nat} (hk : n ≤ k) (xs' : Vector α n) (h : k < n + n) : (xs ++ xs').eraseIdx k h = Vector.cast ⋯ (xs ++ xs'.eraseIdx (k - n) ⋯)

theorem Vector.eraseIdx_append {α : Type u_1} {n m : Nat} {xs : Vector α n} {ys : Vector α m} {k : Nat} (h : k < n + m) : (xs ++ ys).eraseIdx k h = if h' : k < n then Vector.cast ⋯ (xs.eraseIdx k h' ++ ys) else Vector.cast ⋯ (xs ++ ys.eraseIdx (k - n) ⋯)

theorem Vector.eraseIdx_cast {α : Type u_1} {n m : Nat} {w : n = m} {xs : Vector α n} {k : Nat} (h : k < m) : (Vector.cast w xs).eraseIdx k h = Vector.cast ⋯ (xs.eraseIdx k ⋯)

theorem Vector.eraseIdx_replicate {α : Type u_1} {n : Nat} {a : α} {k : Nat} {h : k < n} : (replicate n a).eraseIdx k h = replicate (n - 1) a

theorem Vector.mem_eraseIdx_iff_getElem {α : Type u_1} {n : Nat} {x : α} {xs : Vector α n} {k : Nat} {h : k < n} : x ∈ xs.eraseIdx k h ↔ ∃ (i : Nat), ∃ (w : i < n), i ≠ k ∧ xs[i] = x

theorem Vector.mem_eraseIdx_iff_getElem? {α : Type u_1} {n : Nat} {x : α} {xs : Vector α n} {k : Nat} {h : k < n} : x ∈ xs.eraseIdx k h ↔ ∃ (i : Nat), i ≠ k ∧ xs[i]? = some x

theorem Vector.getElem_eraseIdx_of_lt {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (w : i < n) {j : Nat} (h : j < n - 1) (h' : j < i) : (xs.eraseIdx i w)[j] = xs[j]

theorem Vector.getElem_eraseIdx_of_ge {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (w : i < n) {j : Nat} (h : j < n - 1) (h' : i ≤ j) : (xs.eraseIdx i w)[j] = xs[j + 1]

theorem Vector.eraseIdx_set_eq {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {a : α} {h : i < n} : (xs.set i a h).eraseIdx i h = xs.eraseIdx i h

theorem Vector.eraseIdx_set_lt {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : j < i) : (xs.set i a w).eraseIdx j ⋯ = (xs.eraseIdx j ⋯).set (i - 1) a ⋯

theorem Vector.eraseIdx_set_gt {α : Type u_1} {n : Nat} {xs : Vector α n} {i j : Nat} {a : α} (h : i < j) {w : j < n} : (xs.set i a ⋯).eraseIdx j w = (xs.eraseIdx j w).set i a ⋯

theorem Vector.eraseIdx_set {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {a : α} {hi : i < n} {j : Nat} {hj : j < n} : (xs.set i a hi).eraseIdx j hj = if h' : j < i then (xs.eraseIdx j hj).set (i - 1) a ⋯ else if h'' : j = i then xs.eraseIdx i hi else (xs.eraseIdx j hj).set i a ⋯

theorem Vector.set_eraseIdx_le {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : i ≤ j) (hj : j < n - 1) : (xs.eraseIdx i w).set j a hj = (xs.set (j + 1) a ⋯).eraseIdx i w

theorem Vector.set_eraseIdx_gt {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : j < i) (hj : j < n - 1) : (xs.eraseIdx i w).set j a hj = (xs.set j a ⋯).eraseIdx i w

theorem Vector.set_eraseIdx {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (hj : j < n - 1) : (xs.eraseIdx i w).set j a hj = if h' : i ≤ j then (xs.set (j + 1) a ⋯).eraseIdx i w else (xs.set j a ⋯).eraseIdx i w

@[simp]

theorem Vector.set_getElem_succ_eraseIdx_succ {α : Type u_1} {n : Nat} {xs : Vector α n} {i : Nat} (h : i + 1 < n) : (xs.eraseIdx (i + 1) h).set i xs[i + 1] ⋯ = xs.eraseIdx i ⋯