# insertIdx #

Proves various lemmas about `Vector.insertIdx`.

source
@[simp]
theorem Vector.insertIdx_zero {α : Type u} {n : Nat} {xs : Vector α n} {x : α} :
xs.insertIdx 0 x ⋯ = Vector.cast ⋯ (#v[x] ++ xs)
source
theorem Vector.eraseIdx_insertIdx_self {α : Type u} {a : α} {n i : Nat} {xs : Vector α n} {h : i ≤ n} :
(xs.insertIdx i a h).eraseIdx i ⋯ = xs
source
@[deprecated Vector.eraseIdx_insertIdx_self (since := "2025-06-15")]
theorem Vector.eraseIdx_insertIdx {α : Type u} {a : α} {n i : Nat} {xs : Vector α n} {h : i ≤ n} :
(xs.insertIdx i a h).eraseIdx i ⋯ = xs
source
theorem Vector.insertIdx_eraseIdx_of_ge {α : Type u} {a : α} {n i j : Nat} {xs : Vector α n} (w₁ : i < n) (w₂ : j ≤ n - 1) (h : i ≤ j) :
(xs.eraseIdx i w₁).insertIdx j a w₂ = Vector.cast ⋯ ((xs.insertIdx (j + 1) a ⋯).eraseIdx i ⋯)
source
theorem Vector.insertIdx_eraseIdx_of_le {α : Type u} {a : α} {n i j : Nat} {xs : Vector α n} (w₁ : i < n) (w₂ : j ≤ n - 1) (h : j ≤ i) :
(xs.eraseIdx i w₁).insertIdx j a w₂ = Vector.cast ⋯ ((xs.insertIdx j a ⋯).eraseIdx (i + 1) ⋯)
source
theorem Vector.insertIdx_eraseIdx {α : Type u} {a : α} {n i j : Nat} {as : Vector α n} (h₁ : i < n) (h₂ : j ≤ n - 1) :
(as.eraseIdx i h₁).insertIdx j a h₂ = if h : i ≤ j then Vector.cast ⋯ ((as.insertIdx (j + 1) a ⋯).eraseIdx i ⋯) else Vector.cast ⋯ ((as.insertIdx j a ⋯).eraseIdx (i + 1) ⋯)
source
theorem Vector.insertIdx_comm {α : Type u} {n : Nat} (a b : α) {i j : Nat} {xs : Vector α n} (x✝ : i ≤ j) (x✝¹ : j ≤ n) :
(xs.insertIdx i a ⋯).insertIdx (j + 1) b ⋯ = (xs.insertIdx j b x✝¹).insertIdx i a ⋯
source
theorem Vector.mem_insertIdx {α : Type u} {a : α} {n i : Nat} {b : α} {xs : Vector α n} {h : i ≤ n} :
a ∈ xs.insertIdx i b h ↔ a = b ∨ a ∈ xs
source
@[simp]
theorem Vector.insertIdx_size_self {α : Type u} {n : Nat} {xs : Vector α n} {x : α} :
xs.insertIdx n x ⋯ = xs.push x
source
theorem Vector.getElem_insertIdx {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < n + 1) :
(xs.insertIdx i x w)[k] = if h₁ : k < i then xs[k] else if h₂ : k = i then x else xs[k - 1]
source
theorem Vector.getElem_insertIdx_of_lt {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
(xs.insertIdx i x w)[k] = xs[k]
source
theorem Vector.getElem_insertIdx_self {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
(xs.insertIdx i x w)[i] = x
source
theorem Vector.getElem_insertIdx_of_gt {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i k : Nat} (w : k ≤ n) (h : k > i) :
(xs.insertIdx i x ⋯)[k] = xs[k - 1]
source
theorem Vector.getElem?_insertIdx {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i k : Nat} (h : i ≤ n) :
(xs.insertIdx i x h)[k]? = if k < i then xs[k]? else if k = i then if k ≤ n then some x else none else xs[k - 1]?
source
theorem Vector.getElem?_insertIdx_of_lt {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i k : Nat} (w : i ≤ n) (h : k < i) :
(xs.insertIdx i x w)[k]? = xs[k]?
source
theorem Vector.getElem?_insertIdx_self {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i : Nat} (w : i ≤ n) :
(xs.insertIdx i x w)[i]? = some x
source
theorem Vector.getElem?_insertIdx_of_ge {α : Type u} {n : Nat} {xs : Vector α n} {x : α} {i k : Nat} (w : i < k) (h : k ≤ n) :
(xs.insertIdx i x ⋯)[k]? = xs[k - 1]?