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 : α → α} {n : Nat} (h : n < (modifyHead f l).length) : (modifyHead f l)[n] = if h' : n = 0 then f l[0] else l[n]

@[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 : α → α} {n : Nat} : (modifyHead f l)[n]? = if n = 0 then Option.map f l[n]? else l[n]?

@[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 α} {n : Nat} : take n (modifyHead f l) = modifyHead f (take n l)

@[simp]

theorem List.drop_modifyHead_of_pos {α : Type u_1} {f : α → α} {l : List α} {n : Nat} (h : 0 < n) : drop n (modifyHead f l) = drop n 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 α} {n : Nat} (h : 0 < n) : (modifyHead f l).eraseIdx n = modifyHead f (l.eraseIdx n)

@[simp]

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

modifyTailIdx

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

modify

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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