insertIdx

Proves various lemmas about List.insertIdx.

theorem List.get_insertIdx_of_lt {α : Type u} (l : List α) (x : α) (n k : ℕ) (hn : k < n) (hk : k < l.length) (hk' : k < (insertIdx n x l).length := ⋯) : (insertIdx n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩

theorem List.get_insertIdx_self {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length) (hn' : n < (insertIdx n x l).length := ⋯) : (insertIdx n x l).get ⟨n, hn'⟩ = x

theorem List.getElem_insertIdx_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (insertIdx n x l).length := ⋯) : (insertIdx n x l)[n + k + 1] = l[n + k]

theorem List.get_insertIdx_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (insertIdx n x l).length := ⋯) : (insertIdx n x l).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

theorem List.insertIdx_injective {α : Type u} (n : ℕ) (x : α) : Function.Injective (insertIdx n x)

@[deprecated List.insertIdx_zero (since := "2024-10-21")]

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

Alias of List.insertIdx_zero.

@[deprecated List.insertIdx_succ_nil (since := "2024-10-21")]

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

Alias of List.insertIdx_succ_nil.

@[deprecated List.insertIdx_succ_cons (since := "2024-10-21")]

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

Alias of List.insertIdx_succ_cons.

@[deprecated List.length_insertIdx (since := "2024-10-21")]

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

Alias of List.length_insertIdx.

@[deprecated List.eraseIdx_insertIdx (since := "2024-10-21")]

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

Alias of List.eraseIdx_insertIdx.

@[deprecated List.insertIdx_eraseIdx_of_ge (since := "2024-10-21")]

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

Alias of List.insertIdx_eraseIdx_of_ge.

@[deprecated List.insertIdx_eraseIdx_of_le (since := "2024-10-21")]

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

Alias of List.insertIdx_eraseIdx_of_le.

@[deprecated List.insertIdx_comm (since := "2024-10-21")]

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

Alias of List.insertIdx_comm.

@[deprecated List.mem_insertIdx (since := "2024-10-21")]

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

Alias of List.mem_insertIdx.

@[deprecated List.insertIdx_of_length_lt (since := "2024-10-21")]

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

Alias of List.insertIdx_of_length_lt.

@[deprecated List.insertIdx_length_self (since := "2024-10-21")]

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

Alias of List.insertIdx_length_self.

@[deprecated List.length_le_length_insertIdx (since := "2024-10-21")]

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

Alias of List.length_le_length_insertIdx.

@[deprecated List.length_insertIdx_le_succ (since := "2024-10-21")]

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

Alias of List.length_insertIdx_le_succ.

@[deprecated List.getElem_insertIdx_of_lt (since := "2024-10-21")]

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

Alias of List.getElem_insertIdx_of_lt.

@[deprecated List.get_insertIdx_of_lt (since := "2024-10-21")]

theorem List.get_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n k : ℕ) (hn : k < n) (hk : k < l.length) (hk' : k < (insertIdx n x l).length := ⋯) : (insertIdx n x l).get ⟨k, hk'⟩ = l.get ⟨k, hk⟩

Alias of List.get_insertIdx_of_lt.

@[deprecated List.getElem_insertIdx_self (since := "2024-10-21")]

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

Alias of List.getElem_insertIdx_self.

@[deprecated List.get_insertIdx_self (since := "2024-10-21")]

theorem List.get_insertNth_self {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length) (hn' : n < (insertIdx n x l).length := ⋯) : (insertIdx n x l).get ⟨n, hn'⟩ = x

Alias of List.get_insertIdx_self.

@[deprecated List.getElem_insertIdx_add_succ (since := "2024-10-21")]

theorem List.getElem_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (insertIdx n x l).length := ⋯) : (insertIdx n x l)[n + k + 1] = l[n + k]

Alias of List.getElem_insertIdx_add_succ.

@[deprecated List.get_insertIdx_add_succ (since := "2024-10-21")]

theorem List.get_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length) (hk : n + k + 1 < (insertIdx n x l).length := ⋯) : (insertIdx n x l).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

Alias of List.get_insertIdx_add_succ.

@[deprecated List.insertIdx_injective (since := "2024-10-21")]

theorem List.insertNth_injective {α : Type u} (n : ℕ) (x : α) : Function.Injective (insertIdx n x)

Alias of List.insertIdx_injective.