insertNth

Proves various lemmas about List.insertNth.

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.length_insertNth {α : Type u} {a : α} (n : ℕ) (as : List α) : n ≤ List.length as → List.length (List.insertNth n a as) = List.length as + 1

theorem List.removeNth_insertNth {α : Type u} {a : α} (n : ℕ) (l : List α) : List.removeNth (List.insertNth n a l) n = l

theorem List.insertNth_removeNth_of_ge {α : Type u} {a : α} (n : ℕ) (m : ℕ) (as : List α) : n < List.length as → n ≤ m → List.insertNth m a (List.removeNth as n) = List.removeNth (List.insertNth (m + 1) a as) n

theorem List.insertNth_removeNth_of_le {α : Type u} {a : α} (n : ℕ) (m : ℕ) (as : List α) : n < List.length as → m ≤ n → List.insertNth m a (List.removeNth as n) = List.removeNth (List.insertNth m a as) (n + 1)

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

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

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

@[simp]

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

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

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

theorem List.get_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n : ℕ) (k : ℕ) (hn : k < n) (hk : k < List.length l) (hk' : optParam (k < List.length (List.insertNth n x l)) ⋯) : List.get (List.insertNth n x l) { val := k, isLt := hk' } = List.get l { val := k, isLt := hk }

@[deprecated List.get_insertNth_of_lt]

theorem List.nthLe_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n : ℕ) (k : ℕ) : k < n → ∀ (hk : k < List.length l) (hk' : optParam (k < List.length (List.insertNth n x l)) ⋯), List.nthLe (List.insertNth n x l) k hk' = List.nthLe l k hk

@[simp]

theorem List.get_insertNth_self {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ List.length l) (hn' : optParam (n < List.length (List.insertNth n x l)) ⋯) : List.get (List.insertNth n x l) { val := n, isLt := hn' } = x

@[simp, deprecated List.get_insertNth_self]

theorem List.nthLe_insertNth_self {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ List.length l) (hn' : optParam (n < List.length (List.insertNth n x l)) ⋯) : List.nthLe (List.insertNth n x l) n hn' = x

theorem List.get_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n : ℕ) (k : ℕ) (hk' : n + k < List.length l) (hk : optParam (n + k + 1 < List.length (List.insertNth n x l)) ⋯) : List.get (List.insertNth n x l) { val := n + k + 1, isLt := hk } = List.get l { val := n + k, isLt := hk' }

@[deprecated List.get_insertNth_add_succ]

theorem List.nthLe_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n : ℕ) (k : ℕ) (hk' : n + k < List.length l) (hk : optParam (n + k + 1 < List.length (List.insertNth n x l)) ⋯) : List.nthLe (List.insertNth n x l) (n + k + 1) hk = List.nthLe l (n + k) hk'

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