modifyHead

@[simp]

theorem List.length_modifyHead {α : Type u_1} {f : α → α} {l : List α} : (modifyHead f l).length = l.length

theorem List.modifyHead_eq_set {α : Type u_1} [Inhabited α] (f : α → α) (l : List α) : modifyHead f l = l.set 0 (f (l[0]?.getD default))

@[simp]

theorem List.modifyHead_eq_nil_iff {α : Type u_1} {f : α → α} {l : List α} : modifyHead f l = [] ↔ l = []

@[simp]

theorem List.modifyHead_modifyHead {α : Type u_1} {l : List α} {f g : α → α} : modifyHead g (modifyHead f l) = modifyHead (g ∘ f) l

theorem List.getElem_modifyHead {α : Type u_1} {l : List α} {f : α → α} {i : Nat} (h : i < (modifyHead f l).length) : (modifyHead f l)[i] = if h' : i = 0 then f l[0] else l[i]

@[simp]

theorem List.getElem_modifyHead_zero {α : Type u_1} {l : List α} {f : α → α} {h : 0 < (modifyHead f l).length} : (modifyHead f l)[0] = f l[0]

@[simp]

theorem List.getElem_modifyHead_succ {α : Type u_1} {l : List α} {f : α → α} {n : Nat} (h : n + 1 < (modifyHead f l).length) : (modifyHead f l)[n + 1] = l[n + 1]

theorem List.getElem?_modifyHead {α : Type u_1} {l : List α} {f : α → α} {i : Nat} : (modifyHead f l)[i]? = if i = 0 then Option.map f l[i]? else l[i]?

@[simp]

theorem List.getElem?_modifyHead_zero {α : Type u_1} {l : List α} {f : α → α} : (modifyHead f l)[0]? = Option.map f l[0]?

@[simp]

theorem List.getElem?_modifyHead_succ {α : Type u_1} {l : List α} {f : α → α} {n : Nat} : (modifyHead f l)[n + 1]? = l[n + 1]?

@[simp]

theorem List.head_modifyHead {α : Type u_1} (f : α → α) (l : List α) (h : modifyHead f l ≠ []) : (modifyHead f l).head h = f (l.head ⋯)

@[simp]

theorem List.head?_modifyHead {α : Type u_1} {l : List α} {f : α → α} : (modifyHead f l).head? = Option.map f l.head?

@[simp]

theorem List.tail_modifyHead {α : Type u_1} {f : α → α} {l : List α} : (modifyHead f l).tail = l.tail

@[simp]

theorem List.take_modifyHead {α : Type u_1} {f : α → α} {l : List α} {i : Nat} : take i (modifyHead f l) = modifyHead f (take i l)

@[simp]

theorem List.drop_modifyHead_of_pos {α : Type u_1} {f : α → α} {l : List α} {i : Nat} (h : 0 < i) : drop i (modifyHead f l) = drop i l

theorem List.eraseIdx_modifyHead_zero {α : Type u_1} {f : α → α} {l : List α} : (modifyHead f l).eraseIdx 0 = l.eraseIdx 0

@[simp]

theorem List.eraseIdx_modifyHead_of_pos {α : Type u_1} {f : α → α} {l : List α} {i : Nat} (h : 0 < i) : (modifyHead f l).eraseIdx i = modifyHead f (l.eraseIdx i)

@[simp]

theorem List.modifyHead_id {α : Type u_1} : modifyHead id = id

@[simp]

theorem List.modifyHead_dropLast {α : Type u_1} {l : List α} {f : α → α} : modifyHead f l.dropLast = (modifyHead f l).dropLast

modifyTailIdx

@[simp]

theorem List.modifyTailIdx_id {α : Type u_1} (i : Nat) (l : List α) : l.modifyTailIdx i id = l

theorem List.eraseIdx_eq_modifyTailIdx {α : Type u_1} (i : Nat) (l : List α) : l.eraseIdx i = l.modifyTailIdx i tail

@[simp]

theorem List.length_modifyTailIdx {α : Type u_1} (f : List α → List α) (H : ∀ (l : List α), (f l).length = l.length) (l : List α) (i : Nat) : (l.modifyTailIdx i f).length = l.length

theorem List.modifyTailIdx_add {α : Type u_1} (f : List α → List α) (i : Nat) (l₁ l₂ : List α) : (l₁ ++ l₂).modifyTailIdx (l₁.length + i) f = l₁ ++ l₂.modifyTailIdx i f

theorem List.modifyTailIdx_eq_take_drop {α : Type u_1} (f : List α → List α) (H : f [] = []) (l : List α) (i : Nat) : l.modifyTailIdx i f = take i l ++ f (drop i l)

theorem List.exists_of_modifyTailIdx {α : Type u_1} (f : List α → List α) {i : Nat} {l : List α} (h : i ≤ l.length) : ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ l₁.length = i ∧ l.modifyTailIdx i f = l₁ ++ f l₂

theorem List.modifyTailIdx_modifyTailIdx {α : Type u_1} {f g : List α → List α} (i j : Nat) (l : List α) : (l.modifyTailIdx j f).modifyTailIdx (i + j) g = l.modifyTailIdx j fun (l : List α) => (f l).modifyTailIdx i g

theorem List.modifyTailIdx_modifyTailIdx_le {α : Type u_1} {f g : List α → List α} (i j : Nat) (l : List α) (h : j ≤ i) : (l.modifyTailIdx j f).modifyTailIdx i g = l.modifyTailIdx j fun (l : List α) => (f l).modifyTailIdx (i - j) g

theorem List.modifyTailIdx_modifyTailIdx_self {α : Type u_1} {f g : List α → List α} (i : Nat) (l : List α) : (l.modifyTailIdx i f).modifyTailIdx i g = l.modifyTailIdx i (g ∘ f)

modify

@[simp]

theorem List.modify_nil {α : Type u_1} (f : α → α) (i : Nat) : [].modify i f = []

@[simp]

theorem List.modify_zero_cons {α : Type u_1} (f : α → α) (a : α) (l : List α) : (a :: l).modify 0 f = f a :: l

@[simp]

theorem List.modify_succ_cons {α : Type u_1} (f : α → α) (a : α) (l : List α) (i : Nat) : (a :: l).modify (i + 1) f = a :: l.modify i f

theorem List.modify_cons {α : Type u_1} {f : α → α} {a : α} {l : List α} {i : Nat} : (a :: l).modify i f = if i = 0 then f a :: l else a :: l.modify (i - 1) f

theorem List.modifyHead_eq_modify_zero {α : Type u_1} (f : α → α) (l : List α) : modifyHead f l = l.modify 0 f

@[simp]

theorem List.modify_eq_nil_iff {α : Type u_1} {f : α → α} {i : Nat} {l : List α} : l.modify i f = [] ↔ l = []

theorem List.getElem?_modify {α : Type u_1} (f : α → α) (i : Nat) (l : List α) (j : Nat) : (l.modify i f)[j]? = (fun (a : α) => if i = j then f a else a) <$> l[j]?

@[simp]

theorem List.length_modify {α : Type u_1} (f : α → α) (l : List α) (i : Nat) : (l.modify i f).length = l.length

@[simp]

theorem List.getElem?_modify_eq {α : Type u_1} (f : α → α) (i : Nat) (l : List α) : (l.modify i f)[i]? = f <$> l[i]?

@[simp]

theorem List.getElem?_modify_ne {α : Type u_1} (f : α → α) {i j : Nat} (l : List α) (h : i ≠ j) : (l.modify i f)[j]? = l[j]?

theorem List.getElem_modify {α : Type u_1} (f : α → α) (i : Nat) (l : List α) (j : Nat) (h : j < (l.modify i f).length) : (l.modify i f)[j] = if i = j then f l[j] else l[j]

@[simp]

theorem List.getElem_modify_eq {α : Type u_1} (f : α → α) (i : Nat) (l : List α) (h : i < (l.modify i f).length) : (l.modify i f)[i] = f l[i]

@[simp]

theorem List.getElem_modify_ne {α : Type u_1} (f : α → α) {i j : Nat} (l : List α) (h : i ≠ j) (h' : j < (l.modify i f).length) : (l.modify i f)[j] = l[j]

theorem List.modify_eq_self {α : Type u_1} {f : α → α} {i : Nat} {l : List α} (h : l.length ≤ i) : l.modify i f = l

theorem List.modify_modify_eq {α : Type u_1} (f g : α → α) (i : Nat) (l : List α) : (l.modify i f).modify i g = l.modify i (g ∘ f)

theorem List.modify_modify_ne {α : Type u_1} (f g : α → α) {i j : Nat} (l : List α) (h : i ≠ j) : (l.modify i f).modify j g = (l.modify j g).modify i f

theorem List.modify_eq_set {α : Type u_1} [Inhabited α] (f : α → α) (i : Nat) (l : List α) : l.modify i f = l.set i (f (l[i]?.getD default))

theorem List.modify_eq_take_drop {α : Type u_1} (f : α → α) (l : List α) (i : Nat) : l.modify i f = take i l ++ modifyHead f (drop i l)

theorem List.modify_eq_take_cons_drop {α : Type u_1} {f : α → α} {i : Nat} {l : List α} (h : i < l.length) : l.modify i f = take i l ++ f l[i] :: drop (i + 1) l

theorem List.exists_of_modify {α : Type u_1} (f : α → α) {i : Nat} {l : List α} (h : i < l.length) : ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ l₁.length = i ∧ l.modify i f = l₁ ++ f a :: l₂

@[simp]

theorem List.modify_id {α : Type u_1} (i : Nat) (l : List α) : l.modify i id = l

theorem List.take_modify {α : Type u_1} (f : α → α) (i j : Nat) (l : List α) : take j (l.modify i f) = (take j l).modify i f

theorem List.drop_modify_of_lt {α : Type u_1} (f : α → α) (i j : Nat) (l : List α) (h : i < j) : drop j (l.modify i f) = drop j l

theorem List.drop_modify_of_ge {α : Type u_1} (f : α → α) (i j : Nat) (l : List α) (h : i ≥ j) : drop j (l.modify i f) = (drop j l).modify (i - j) f

theorem List.eraseIdx_modify_of_eq {α : Type u_1} (f : α → α) (i : Nat) (l : List α) : (l.modify i f).eraseIdx i = l.eraseIdx i

theorem List.eraseIdx_modify_of_lt {α : Type u_1} (f : α → α) (i j : Nat) (l : List α) (h : j < i) : (l.modify i f).eraseIdx j = (l.eraseIdx j).modify (i - 1) f

theorem List.eraseIdx_modify_of_gt {α : Type u_1} (f : α → α) (i j : Nat) (l : List α) (h : j > i) : (l.modify i f).eraseIdx j = (l.eraseIdx j).modify i f

theorem List.modify_eraseIdx_of_lt {α : Type u_1} (f : α → α) (i j : Nat) (l : List α) (h : j < i) : (l.eraseIdx i).modify j f = (l.modify j f).eraseIdx i

theorem List.modify_eraseIdx_of_ge {α : Type u_1} (f : α → α) (i j : Nat) (l : List α) (h : j ≥ i) : (l.eraseIdx i).modify j f = (l.modify (j + 1) f).eraseIdx i