insertIdx

Proves various lemmas about List.insertIdx.

@[simp]

theorem List.insertIdx_zero {α : Type u} (s : List α) (x : α) : insertIdx 0 x s = x :: s

@[simp]

theorem List.insertIdx_succ_nil {α : Type u} (n : Nat) (a : α) : insertIdx (n + 1) a [] = []

@[simp]

theorem List.insertIdx_succ_cons {α : Type u} (s : List α) (hd x : α) (n : Nat) : insertIdx (n + 1) x (hd :: s) = hd :: insertIdx n x s

theorem List.length_insertIdx {α : Type u} {a : α} (n : Nat) (as : List α) : (insertIdx n a as).length = if n ≤ as.length then as.length + 1 else as.length

theorem List.length_insertIdx_of_le_length {α : Type u} {a : α} {n : Nat} {as : List α} (h : n ≤ as.length) : (insertIdx n a as).length = as.length + 1

theorem List.length_insertIdx_of_length_lt {α : Type u} {a : α} {as : List α} {n : Nat} (h : as.length < n) : (insertIdx n a as).length = as.length

theorem List.eraseIdx_insertIdx {α : Type u} {a : α} (n : Nat) (l : List α) : (insertIdx n a l).eraseIdx n = l

theorem List.insertIdx_eraseIdx_of_ge {α : Type u} {a : α} (n m : Nat) (as : List α) : n < as.length → n ≤ m → insertIdx m a (as.eraseIdx n) = (insertIdx (m + 1) a as).eraseIdx n

theorem List.insertIdx_eraseIdx_of_le {α : Type u} {a : α} (n m : Nat) (as : List α) : n < as.length → m ≤ n → insertIdx m a (as.eraseIdx n) = (insertIdx m a as).eraseIdx (n + 1)

theorem List.insertIdx_comm {α : Type u} (a b : α) (i j : Nat) (l : List α) : i ≤ j → j ≤ l.length → insertIdx (j + 1) b (insertIdx i a l) = insertIdx i a (insertIdx j b l)

theorem List.mem_insertIdx {α : Type u} {a b : α} {n : Nat} {l : List α} : n ≤ l.length → (a ∈ insertIdx n b l ↔ a = b ∨ a ∈ l)

theorem List.insertIdx_of_length_lt {α : Type u} (l : List α) (x : α) (n : Nat) (h : l.length < n) : insertIdx n x l = l

@[simp]

theorem List.insertIdx_length_self {α : Type u} (l : List α) (x : α) : insertIdx l.length x l = l ++ [x]

theorem List.length_le_length_insertIdx {α : Type u} (l : List α) (x : α) (n : Nat) : l.length ≤ (insertIdx n x l).length

theorem List.length_insertIdx_le_succ {α : Type u} (l : List α) (x : α) (n : Nat) : (insertIdx n x l).length ≤ l.length + 1

theorem List.getElem_insertIdx_of_lt {α : Type u} {l : List α} {x : α} {n k : Nat} (hn : k < n) (hk : k < (insertIdx n x l).length) : (insertIdx n x l)[k] = l[k]

@[simp]

theorem List.getElem_insertIdx_self {α : Type u} {l : List α} {x : α} {n : Nat} (hn : n < (insertIdx n x l).length) : (insertIdx n x l)[n] = x

theorem List.getElem_insertIdx_of_ge {α : Type u} {l : List α} {x : α} {n k : Nat} (hn : n + 1 ≤ k) (hk : k < (insertIdx n x l).length) : (insertIdx n x l)[k] = l[k - 1]

theorem List.getElem_insertIdx {α : Type u} {l : List α} {x : α} {n k : Nat} (h : k < (insertIdx n x l).length) : (insertIdx n x l)[k] = if h₁ : k < n then l[k] else if h₂ : k = n then x else l[k - 1]

theorem List.getElem?_insertIdx {α : Type u} {l : List α} {x : α} {n k : Nat} : (insertIdx n x l)[k]? = if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

theorem List.getElem?_insertIdx_of_lt {α : Type u} {l : List α} {x : α} {n k : Nat} (h : k < n) : (insertIdx n x l)[k]? = l[k]?

theorem List.getElem?_insertIdx_self {α : Type u} {l : List α} {x : α} {n : Nat} : (insertIdx n x l)[n]? = if n ≤ l.length then some x else none

theorem List.getElem?_insertIdx_of_ge {α : Type u} {l : List α} {x : α} {n k : Nat} (h : n + 1 ≤ k) : (insertIdx n x l)[k]? = l[k - 1]?