insertIdx

Proves various lemmas about Array.insertIdx.

@[simp]

theorem Array.toList_insertIdx {α : Type u} {xs : Array α} {i : Nat} {x : α} (h : i ≤ xs.size) : (xs.insertIdx i x h).toList = xs.toList.insertIdx i x

@[simp]

theorem Array.insertIdx_zero {α : Type u} {xs : Array α} {x : α} : xs.insertIdx 0 x ⋯ = #[x] ++ xs

@[simp]

theorem Array.size_insertIdx {α : Type u} {a : α} {i : Nat} {xs : Array α} (h : i ≤ xs.size) : (xs.insertIdx i a h).size = xs.size + 1

theorem Array.eraseIdx_insertIdx_self {α : Type u} {a : α} {i : Nat} {xs : Array α} (h : i ≤ xs.size) : (xs.insertIdx i a h).eraseIdx i ⋯ = xs

theorem Array.insertIdx_eraseIdx_of_ge {α : Type u} {a : α} {i j : Nat} {as : Array α} (w₁ : i < as.size) (w₂ : j ≤ (as.eraseIdx i w₁).size) (h : i ≤ j) : (as.eraseIdx i w₁).insertIdx j a w₂ = (as.insertIdx (j + 1) a ⋯).eraseIdx i ⋯

theorem Array.insertIdx_eraseIdx_of_le {α : Type u} {a : α} {i j : Nat} {as : Array α} (w₁ : i < as.size) (w₂ : j ≤ (as.eraseIdx i w₁).size) (h : j ≤ i) : (as.eraseIdx i w₁).insertIdx j a w₂ = (as.insertIdx j a ⋯).eraseIdx (i + 1) ⋯

theorem Array.insertIdx_eraseIdx {α : Type u} {a : α} {i j : Nat} {as : Array α} (h₁ : i < as.size) (h₂ : j ≤ (as.eraseIdx i h₁).size) : (as.eraseIdx i h₁).insertIdx j a h₂ = if h : i ≤ j then (as.insertIdx (j + 1) a ⋯).eraseIdx i ⋯ else (as.insertIdx j a ⋯).eraseIdx (i + 1) ⋯

theorem Array.insertIdx_comm {α : Type u} (a b : α) {i j : Nat} {xs : Array α} (x✝ : i ≤ j) (x✝¹ : j ≤ xs.size) : (xs.insertIdx i a ⋯).insertIdx (j + 1) b ⋯ = (xs.insertIdx j b x✝¹).insertIdx i a ⋯

theorem Array.mem_insertIdx {α : Type u} {a : α} {i : Nat} {b : α} {xs : Array α} {h : i ≤ xs.size} : a ∈ xs.insertIdx i b h ↔ a = b ∨ a ∈ xs

@[simp]

theorem Array.insertIdx_size_self {α : Type u} {xs : Array α} {x : α} : xs.insertIdx xs.size x ⋯ = xs.push x

theorem Array.getElem_insertIdx {α : Type u} {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < (xs.insertIdx i x w).size) : (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 Array.getElem_insertIdx_of_lt {α : Type u} {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < i) : (xs.insertIdx i x w)[k] = xs[k]

theorem Array.getElem_insertIdx_self {α : Type u} {xs : Array α} {x : α} {i : Nat} (w : i ≤ xs.size) : (xs.insertIdx i x w)[i] = x

theorem Array.getElem_insertIdx_of_gt {α : Type u} {xs : Array α} {x : α} {i k : Nat} (w : k ≤ xs.size) (h : k > i) : (xs.insertIdx i x ⋯)[k] = xs[k - 1]

theorem Array.getElem?_insertIdx {α : Type u} {xs : Array α} {x : α} {i k : Nat} (h : i ≤ xs.size) : (xs.insertIdx i x h)[k]? = if k < i then xs[k]? else if k = i then if k ≤ xs.size then some x else none else xs[k - 1]?

theorem Array.getElem?_insertIdx_of_lt {α : Type u} {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < i) : (xs.insertIdx i x w)[k]? = xs[k]?

theorem Array.getElem?_insertIdx_self {α : Type u} {xs : Array α} {x : α} {i : Nat} (w : i ≤ xs.size) : (xs.insertIdx i x w)[i]? = some x

theorem Array.getElem?_insertIdx_of_ge {α : Type u} {xs : Array α} {x : α} {i k : Nat} (w : i < k) (h : k ≤ xs.size) : (xs.insertIdx i x ⋯)[k]? = xs[k - 1]?