insertIdx

Proves various lemmas about List.insertIdx.

@[simp]

theorem List.sublist_insertIdx {α : Type u} (l : List α) (n : ℕ) (a : α) : l.Sublist (l.insertIdx n a)

@[simp]

theorem List.subset_insertIdx {α : Type u} (l : List α) (n : ℕ) (a : α) : l ⊆ l.insertIdx n a

@[simp]

theorem List.insertIdx_eraseIdx_self {α : Type u} {l : List α} {n : ℕ} (hn : n ≠ l.length) (a : α) : (l.eraseIdx n).insertIdx n a = l.set n a

Erasing nth element of a list, then inserting a at the same place is the same as setting nth element to a.

We assume that n ≠ length l, because otherwise LHS equals l ++ [a] while RHS equals l.

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

theorem List.eq_or_mem_of_mem_insertIdx {α : Type u} {l : List α} {n : ℕ} {a b : α} (h : a ∈ l.insertIdx n b) : a = b ∨ a ∈ l

theorem List.insertIdx_subset_cons {α : Type u} (n : ℕ) (a : α) (l : List α) : l.insertIdx n a ⊆ a :: l

theorem List.insertIdx_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} {a : α} {n : ℕ} (hl : ∀ (x : α), x ∈ l → p x) (ha : p a) : (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯

theorem List.map_insertIdx {α : Type u} {β : Type v} (f : α → β) (l : List α) (n : ℕ) (a : α) : map f (l.insertIdx n a) = (map f l).insertIdx n (f a)

theorem List.eraseIdx_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (hl : ∀ (a : α), a ∈ l → p a) (n : ℕ) : (pmap f l hl).eraseIdx n = pmap f (l.eraseIdx n) ⋯

theorem List.eraseIdx_map {α : Type u} {β : Type v} (f : α → β) (l : List α) (n : ℕ) : (map f l).eraseIdx n = map f (l.eraseIdx n)

Erasing an index commutes with List.map.

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

theorem List.get_insertIdx_self {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length) (hn' : n < (l.insertIdx n x).length := ⋯) : (l.insertIdx n x).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 < (l.insertIdx n x).length := ⋯) : (l.insertIdx n x)[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 < (l.insertIdx n x).length := ⋯) : (l.insertIdx n x).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

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

theorem List.take_insertIdx_eq_take_of_le {α : Type u} (l : List α) (x : α) (i j : ℕ) (h : i ≤ j) : take i (l.insertIdx j x) = take i l

theorem List.take_eraseIdx_eq_take_of_le {α : Type u} (l : List α) (i j : ℕ) (h : i ≤ j) : take i (l.eraseIdx j) = take i l