insertIdx

Proves various lemmas about Vector.insertIdx.

@[simp]

theorem Vector.insertIdx_zero {α : Type u} {n : Nat} {xs : Vector α n} {x : α} : xs.insertIdx 0 x ⋯ = Vector.cast ⋯ (#v[x] ++ xs)

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

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 ⋯)

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) ⋯)

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) ⋯)

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 ⋯

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

@[simp]

theorem Vector.insertIdx_size_self {α : Type u} {n : Nat} {xs : Vector α n} {x : α} : xs.insertIdx n x ⋯ = xs.push x

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]

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]

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

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]

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]?

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]?

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

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]?