Documentation

Batteries.Data.List.Lemmas

toArray #

@[simp]
theorem List.getElem_mk {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.length) :
{ toList := xs }[i] = xs[i]

== #

@[simp]
theorem List.beq_nil_iff {α : Type u_1} [BEq α] {l : List α} :
(l == []) = l.isEmpty
@[simp]
theorem List.nil_beq_iff {α : Type u_1} [BEq α] {l : List α} :
([] == l) = l.isEmpty
@[simp]
theorem List.cons_beq_cons {α : Type u_1} [BEq α] {a b : α} {l₁ l₂ : List α} :
(a :: l₁ == b :: l₂) = (a == b && l₁ == l₂)
theorem List.length_eq_of_beq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : (l₁ == l₂) = true) :
l₁.length = l₂.length

next? #

@[simp]
theorem List.next?_nil {α : Type u_1} :
[].next? = none
@[simp]
theorem List.next?_cons {α : Type u_1} (a : α) (l : List α) :
(a :: l).next? = some (a, l)

dropLast #

theorem List.dropLast_eq_eraseIdx {α : Type u_1} {xs : List α} {i : Nat} (last_idx : i + 1 = xs.length) :
xs.dropLast = xs.eraseIdx i

set #

theorem List.set_eq_modify {α : Type u_1} (a : α) (n : Nat) (l : List α) :
l.set n a = List.modify (fun (x : α) => a) n l
theorem List.set_eq_take_cons_drop {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) :
l.set n a = List.take n l ++ a :: List.drop (n + 1) l
theorem List.modify_eq_set_get? {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
List.modify f n l = ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l
theorem List.modify_eq_set_get {α : Type u_1} (f : αα) {n : Nat} {l : List α} (h : n < l.length) :
List.modify f n l = l.set n (f (l.get n, h))
theorem List.getElem?_set_eq_of_lt {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) :
(l.set n a)[n]? = some a
theorem List.get?_set_of_lt {α : Type u_1} (a : α) {m n : Nat} (l : List α) (h : n < l.length) :
(l.set m a).get? n = if m = n then some a else l.get? n
theorem List.get?_set_of_lt' {α : Type u_1} (a : α) {m n : Nat} (l : List α) (h : m < l.length) :
(l.set m a).get? n = if m = n then some a else l.get? n

tail #

theorem List.length_tail_add_one {α : Type u_1} (l : List α) (h : 0 < l.length) :
l.tail.length + 1 = l.length

eraseP #

@[simp]
theorem List.extractP_eq_find?_eraseP {α : Type u_1} {p : αBool} (l : List α) :
theorem List.extractP_eq_find?_eraseP.go {α : Type u_1} {p : αBool} (l : List α) (acc : Array α) (xs : List α) :
l = acc.toList ++ xsList.extractP.go p l xs acc = (List.find? p xs, acc.toList ++ List.eraseP p xs)

erase #

theorem List.erase_eq_self_iff_forall_bne {α : Type u_1} [BEq α] (a : α) (xs : List α) :
xs.erase a = xs ∀ (x : α), x xs¬(x == a) = true

findIdx? #

theorem List.findIdx_eq_findIdx? {α : Type u_1} (p : αBool) (l : List α) :
List.findIdx p l = match List.findIdx? p l with | some i => i | none => l.length

replaceF #

theorem List.replaceF_nil {α✝ : Type u_1} {p : α✝Option α✝} :
theorem List.replaceF_cons {α : Type u_1} {p : αOption α} (a : α) (l : List α) :
List.replaceF p (a :: l) = match p a with | none => a :: List.replaceF p l | some a' => a' :: l
theorem List.replaceF_cons_of_some {α : Type u_1} {a' a : α} {l : List α} (p : αOption α) (h : p a = some a') :
List.replaceF p (a :: l) = a' :: l
theorem List.replaceF_cons_of_none {α : Type u_1} {a : α} {l : List α} (p : αOption α) (h : p a = none) :
theorem List.replaceF_of_forall_none {α : Type u_1} {p : αOption α} {l : List α} (h : ∀ (a : α), a lp a = none) :
theorem List.exists_of_replaceF {α : Type u_1} {p : αOption α} {l : List α} {a a' : α} :
a lp a = some a'∃ (a : α), ∃ (a' : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁p b = none) p a = some a' l = l₁ ++ a :: l₂ List.replaceF p l = l₁ ++ a' :: l₂
theorem List.exists_or_eq_self_of_replaceF {α : Type u_1} (p : αOption α) (l : List α) :
List.replaceF p l = l ∃ (a : α), ∃ (a' : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁p b = none) p a = some a' l = l₁ ++ a :: l₂ List.replaceF p l = l₁ ++ a' :: l₂
@[simp]
theorem List.length_replaceF {α✝ : Type u_1} {f : α✝Option α✝} {l : List α✝} :
(List.replaceF f l).length = l.length

disjoint #

theorem List.disjoint_symm {α✝ : Type u_1} {l₁ l₂ : List α✝} (d : l₁.Disjoint l₂) :
l₂.Disjoint l₁
theorem List.disjoint_comm {α✝ : Type u_1} {l₁ l₂ : List α✝} :
l₁.Disjoint l₂ l₂.Disjoint l₁
theorem List.disjoint_left {α✝ : Type u_1} {l₁ l₂ : List α✝} :
l₁.Disjoint l₂ ∀ ⦃a : α✝⦄, a l₁¬a l₂
theorem List.disjoint_right {α✝ : Type u_1} {l₁ l₂ : List α✝} :
l₁.Disjoint l₂ ∀ ⦃a : α✝⦄, a l₂¬a l₁
theorem List.disjoint_iff_ne {α✝ : Type u_1} {l₁ l₂ : List α✝} :
l₁.Disjoint l₂ ∀ (a : α✝), a l₁∀ (b : α✝), b l₂a b
theorem List.disjoint_of_subset_left {α✝ : Type u_1} {l₁ l l₂ : List α✝} (ss : l₁ l) (d : l.Disjoint l₂) :
l₁.Disjoint l₂
theorem List.disjoint_of_subset_right {α✝ : Type u_1} {l₂ l l₁ : List α✝} (ss : l₂ l) (d : l₁.Disjoint l) :
l₁.Disjoint l₂
theorem List.disjoint_of_disjoint_cons_left {α✝ : Type u_1} {a : α✝} {l₁ l₂ : List α✝} :
(a :: l₁).Disjoint l₂l₁.Disjoint l₂
theorem List.disjoint_of_disjoint_cons_right {α✝ : Type u_1} {a : α✝} {l₁ l₂ : List α✝} :
l₁.Disjoint (a :: l₂)l₁.Disjoint l₂
@[simp]
theorem List.disjoint_nil_left {α : Type u_1} (l : List α) :
[].Disjoint l
@[simp]
theorem List.disjoint_nil_right {α : Type u_1} (l : List α) :
l.Disjoint []
@[simp]
theorem List.singleton_disjoint {α✝ : Type u_1} {a : α✝} {l : List α✝} :
[a].Disjoint l ¬a l
@[simp]
theorem List.disjoint_singleton {α✝ : Type u_1} {l : List α✝} {a : α✝} :
l.Disjoint [a] ¬a l
@[simp]
theorem List.disjoint_append_left {α✝ : Type u_1} {l₁ l₂ l : List α✝} :
(l₁ ++ l₂).Disjoint l l₁.Disjoint l l₂.Disjoint l
@[simp]
theorem List.disjoint_append_right {α✝ : Type u_1} {l l₁ l₂ : List α✝} :
l.Disjoint (l₁ ++ l₂) l.Disjoint l₁ l.Disjoint l₂
@[simp]
theorem List.disjoint_cons_left {α✝ : Type u_1} {a : α✝} {l₁ l₂ : List α✝} :
(a :: l₁).Disjoint l₂ ¬a l₂ l₁.Disjoint l₂
@[simp]
theorem List.disjoint_cons_right {α✝ : Type u_1} {l₁ : List α✝} {a : α✝} {l₂ : List α✝} :
l₁.Disjoint (a :: l₂) ¬a l₁ l₁.Disjoint l₂
theorem List.disjoint_of_disjoint_append_left_left {α✝ : Type u_1} {l₁ l₂ l : List α✝} (d : (l₁ ++ l₂).Disjoint l) :
l₁.Disjoint l
theorem List.disjoint_of_disjoint_append_left_right {α✝ : Type u_1} {l₁ l₂ l : List α✝} (d : (l₁ ++ l₂).Disjoint l) :
l₂.Disjoint l
theorem List.disjoint_of_disjoint_append_right_left {α✝ : Type u_1} {l l₁ l₂ : List α✝} (d : l.Disjoint (l₁ ++ l₂)) :
l.Disjoint l₁
theorem List.disjoint_of_disjoint_append_right_right {α✝ : Type u_1} {l l₁ l₂ : List α✝} (d : l.Disjoint (l₁ ++ l₂)) :
l.Disjoint l₂

union #

theorem List.union_def {α : Type u_1} [BEq α] (l₁ l₂ : List α) :
l₁ l₂ = List.foldr List.insert l₂ l₁
@[simp]
theorem List.nil_union {α : Type u_1} [BEq α] (l : List α) :
[] l = l
@[simp]
theorem List.cons_union {α : Type u_1} [BEq α] (a : α) (l₁ l₂ : List α) :
a :: l₁ l₂ = List.insert a (l₁ l₂)
@[simp]
theorem List.mem_union_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α} :
x l₁ l₂ x l₁ x l₂

inter #

theorem List.inter_def {α : Type u_1} [BEq α] (l₁ l₂ : List α) :
l₁ l₂ = List.filter (fun (x : α) => List.elem x l₂) l₁
@[simp]
theorem List.mem_inter_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α} :
x l₁ l₂ x l₁ x l₂

product #

@[simp]
theorem List.pair_mem_product {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {x : α} {y : β} :
(x, y) xs.product ys x xs y ys

List.prod satisfies a specification of cartesian product on lists.

monadic operations #

theorem List.forIn_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αβm (ForInStep β)) (l : List α) (init : β) :
forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)

diff #

@[simp]
theorem List.diff_nil {α : Type u_1} [BEq α] (l : List α) :
l.diff [] = l
@[simp]
theorem List.diff_cons {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ l₂ : List α) (a : α) :
l₁.diff (a :: l₂) = (l₁.erase a).diff l₂
theorem List.diff_cons_right {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ l₂ : List α) (a : α) :
l₁.diff (a :: l₂) = (l₁.diff l₂).erase a
theorem List.diff_erase {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ l₂ : List α) (a : α) :
(l₁.diff l₂).erase a = (l₁.erase a).diff l₂
@[simp]
theorem List.nil_diff {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) :
[].diff l = []
theorem List.cons_diff {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l₁ l₂ : List α) :
(a :: l₁).diff l₂ = if a l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂
theorem List.cons_diff_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₂ : List α} (h : a l₂) (l₁ : List α) :
(a :: l₁).diff l₂ = l₁.diff (l₂.erase a)
theorem List.cons_diff_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₂ : List α} (h : ¬a l₂) (l₁ : List α) :
(a :: l₁).diff l₂ = a :: l₁.diff l₂
theorem List.diff_eq_foldl {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ l₂ : List α) :
l₁.diff l₂ = List.foldl List.erase l₁ l₂
@[simp]
theorem List.diff_append {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ l₂ l₃ : List α) :
l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃
theorem List.diff_sublist {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ l₂ : List α) :
(l₁.diff l₂).Sublist l₁
theorem List.diff_subset {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ l₂ : List α) :
l₁.diff l₂ l₁
theorem List.mem_diff_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
a l₁¬a l₂a l₁.diff l₂
theorem List.Sublist.diff_right {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ l₃ : List α} :
l₁.Sublist l₂(l₁.diff l₃).Sublist (l₂.diff l₃)
theorem List.Sublist.erase_diff_erase_sublist {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
l₁.Sublist l₂((l₂.erase a).diff (l₁.erase a)).Sublist (l₂.diff l₁)

drop #

theorem List.disjoint_take_drop {α : Type u_1} {m n : Nat} {l : List α} :
l.Nodupm n(List.take m l).Disjoint (List.drop n l)

Chain #

@[simp]
theorem List.chain_cons {α : Type u_1} {R : ααProp} {a b : α} {l : List α} :
List.Chain R a (b :: l) R a b List.Chain R b l
theorem List.rel_of_chain_cons {α : Type u_1} {R : ααProp} {a b : α} {l : List α} (p : List.Chain R a (b :: l)) :
R a b
theorem List.chain_of_chain_cons {α : Type u_1} {R : ααProp} {a b : α} {l : List α} (p : List.Chain R a (b :: l)) :
theorem List.Chain.imp' {α : Type u_1} {R S : ααProp} (HRS : ∀ ⦃a b : α⦄, R a bS a b) {a b : α} (Hab : ∀ ⦃c : α⦄, R a cS b c) {l : List α} (p : List.Chain R a l) :
theorem List.Chain.imp {α : Type u_1} {R S : ααProp} (H : ∀ (a b : α), R a bS a b) {a : α} {l : List α} (p : List.Chain R a l) :
theorem List.Pairwise.chain {α✝ : Type u_1} {R : α✝α✝Prop} {a : α✝} {l : List α✝} (p : List.Pairwise R (a :: l)) :

range', range #

theorem List.chain_succ_range' (s n step : Nat) :
List.Chain (fun (a b : Nat) => b = a + step) s (List.range' (s + step) n step)
theorem List.chain_lt_range' (s n : Nat) {step : Nat} (h : 0 < step) :
List.Chain (fun (x1 x2 : Nat) => x1 < x2) s (List.range' (s + step) n step)
@[deprecated List.getElem?_range']
theorem List.get?_range' (s step : Nat) {m n : Nat} (h : m < n) :
(List.range' s n step).get? m = some (s + step * m)
@[deprecated List.getElem_range']
theorem List.get_range' {n m step : Nat} (i : Nat) (H : i < (List.range' n m step).length) :
(List.range' n m step).get i, H = n + step * i
@[deprecated List.getElem?_range]
theorem List.get?_range {m n : Nat} (h : m < n) :
(List.range n).get? m = some m
@[deprecated List.getElem_range]
theorem List.get_range {n : Nat} (i : Nat) (H : i < (List.range n).length) :
(List.range n).get i, H = i

indexOf and indexesOf #

theorem List.foldrIdx_start {α : Type u_1} {xs : List α} {α✝ : Sort u_2} {f : Natαα✝α✝} {i : α✝} {s : Nat} :
List.foldrIdx f i xs s = List.foldrIdx (fun (i : Nat) => f (i + s)) i xs
@[simp]
theorem List.foldrIdx_cons {α : Type u_1} {x : α} {xs : List α} {α✝ : Sort u_2} {f : Natαα✝α✝} {i : α✝} {s : Nat} :
List.foldrIdx f i (x :: xs) s = f s x (List.foldrIdx f i xs (s + 1))
theorem List.findIdxs_cons_aux {α : Type u_1} {xs : List α} {s : Nat} (p : αBool) :
List.foldrIdx (fun (i : Nat) (a : α) (is : List Nat) => if p a = true then (i + 1) :: is else is) [] xs s = List.map (fun (x : Nat) => x + 1) (List.foldrIdx (fun (i : Nat) (a : α) (is : List Nat) => if p a = true then i :: is else is) [] xs s)
theorem List.findIdxs_cons {α : Type u_1} {x : α} {xs : List α} {p : αBool} :
List.findIdxs p (x :: xs) = bif p x then 0 :: List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs) else List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs)
@[simp]
theorem List.indexesOf_nil {α : Type u_1} {x : α} [BEq α] :
theorem List.indexesOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] :
List.indexesOf y (x :: xs) = bif x == y then 0 :: List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs) else List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs)
@[simp]
theorem List.eraseIdx_indexOf_eq_erase {α : Type u_1} [BEq α] (a : α) (l : List α) :
l.eraseIdx (List.indexOf a l) = l.erase a
theorem List.indexOf_mem_indexesOf {α : Type u_1} {x : α} [BEq α] [LawfulBEq α] {xs : List α} (m : x xs) :
@[simp]
theorem List.indexOf?_nil {α : Type u_1} {x : α} [BEq α] :
List.indexOf? x [] = none
theorem List.indexOf?_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] :
List.indexOf? y (x :: xs) = if (x == y) = true then some 0 else Option.map Nat.succ (List.indexOf? y xs)
theorem List.indexOf?_eq_none_iff {α : Type u_1} [BEq α] {a : α} {l : List α} :
List.indexOf? a l = none ∀ (x : α), x l¬(x == a) = true
theorem List.indexOf_eq_indexOf? {α : Type u_1} [BEq α] (a : α) (l : List α) :
List.indexOf a l = match List.indexOf? a l with | some i => i | none => l.length

insertP #

theorem List.insertP_loop {α : Type u_1} {p : αBool} (a : α) (l r : List α) :
List.insertP.loop p a l r = r.reverseAux (List.insertP p a l)
@[simp]
theorem List.insertP_nil {α : Type u_1} (p : αBool) (a : α) :
List.insertP p a [] = [a]
@[simp]
theorem List.insertP_cons_pos {α : Type u_1} (p : αBool) (a b : α) (l : List α) (h : p b = true) :
List.insertP p a (b :: l) = a :: b :: l
@[simp]
theorem List.insertP_cons_neg {α : Type u_1} (p : αBool) (a b : α) (l : List α) (h : ¬p b = true) :
List.insertP p a (b :: l) = b :: List.insertP p a l
@[simp]
theorem List.length_insertP {α : Type u_1} (p : αBool) (a : α) (l : List α) :
(List.insertP p a l).length = l.length + 1
@[simp]
theorem List.mem_insertP {α : Type u_1} (p : αBool) (a : α) (l : List α) :

dropPrefix?, dropSuffix?, dropInfix? #

@[simp]
theorem List.dropPrefix?_nil {α : Type u_1} [BEq α] {p : List α} :
p.dropPrefix? [] = some p
@[irreducible]
theorem List.dropPrefix?_eq_some_iff {α : Type u_1} [BEq α] {l p s : List α} :
l.dropPrefix? p = some s ∃ (p' : List α), l = p' ++ s (p' == p) = true
theorem List.dropPrefix?_append_of_beq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (p : List α) (h : (l₁ == l₂) = true) :
(l₁ ++ p).dropPrefix? l₂ = some p
theorem List.dropSuffix?_eq_some_iff {α : Type u_1} [BEq α] {l p s : List α} :
l.dropSuffix? s = some p ∃ (s' : List α), l = p ++ s' (s' == s) = true
@[simp]
theorem List.dropSuffix?_nil {α : Type u_1} [BEq α] {s : List α} :
s.dropSuffix? [] = some s
@[irreducible]
theorem List.dropInfix?_go_eq_some_iff {α : Type u_1} [BEq α] {i l acc p s : List α} :
List.dropInfix?.go i l acc = some (p, s) ∃ (p' : List α), p = acc.reverse ++ p' (∃ (i' : List α), l = p' ++ i' ++ s (i' == i) = true) ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s''(i'' == i) = truep''.length p'.length
theorem List.dropInfix?_eq_some_iff {α : Type u_1} [BEq α] {l i p s : List α} :
l.dropInfix? i = some (p, s) (∃ (i' : List α), l = p ++ i' ++ s (i' == i) = true) ∀ (p' i' s' : List α), l = p' ++ i' ++ s'(i' == i) = truep'.length p.length
@[simp]
theorem List.dropInfix?_nil {α : Type u_1} [BEq α] {s : List α} :
s.dropInfix? [] = some ([], s)

deprecations #

@[deprecated List.isEmpty_iff]
theorem List.isEmpty_iff_eq_nil {α : Type u_1} {l : List α} :
l.isEmpty = true l = []

Alias of List.isEmpty_iff.

@[deprecated List.getElem_eq_iff]
theorem List.get_eq_iff {α✝ : Type u_1} {l : List α✝} {n : Fin l.length} {x : α✝} :
l.get n = x l.get? n = some x
@[deprecated List.getElem?_inj]
theorem List.get?_inj {i : Nat} {α✝ : Type u_1} {xs : List α✝} {j : Nat} (h₀ : i < xs.length) (h₁ : xs.Nodup) (h₂ : xs.get? i = xs.get? j) :
i = j
@[deprecated List.modify_nil]
theorem List.modifyNth_nil {α : Type u_1} (f : αα) (n : Nat) :
List.modify f n [] = []

Alias of List.modify_nil.

@[deprecated List.modify_zero_cons]
theorem List.modifyNth_zero_cons {α : Type u_1} (f : αα) (a : α) (l : List α) :
List.modify f 0 (a :: l) = f a :: l

Alias of List.modify_zero_cons.

@[deprecated List.modify_succ_cons]
theorem List.modifyNth_succ_cons {α : Type u_1} (f : αα) (a : α) (l : List α) (n : Nat) :
List.modify f (n + 1) (a :: l) = a :: List.modify f n l

Alias of List.modify_succ_cons.

@[deprecated List.modifyTailIdx_id]
theorem List.modifyNthTail_id {α : Type u_1} (n : Nat) (l : List α) :

Alias of List.modifyTailIdx_id.

@[deprecated List.eraseIdx_eq_modifyTailIdx]
theorem List.eraseIdx_eq_modifyNthTail {α : Type u_1} (n : Nat) (l : List α) :
l.eraseIdx n = List.modifyTailIdx List.tail n l

Alias of List.eraseIdx_eq_modifyTailIdx.

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

Alias of List.getElem?_modify.

@[deprecated List.getElem?_modify]
theorem List.get?_modifyNth {α : Type u_1} (f : αα) (n : Nat) (l : List α) (m : Nat) :
(List.modify f n l).get? m = (fun (a : α) => if n = m then f a else a) <$> l.get? m
@[deprecated List.length_modifyTailIdx]
theorem List.length_modifyNthTail {α : Type u_1} (f : List αList α) (H : ∀ (l : List α), (f l).length = l.length) (n : Nat) (l : List α) :
(List.modifyTailIdx f n l).length = l.length

Alias of List.length_modifyTailIdx.

@[deprecated List.length_modifyTailIdx]
theorem List.modifyNthTail_length {α : Type u_1} (f : List αList α) (H : ∀ (l : List α), (f l).length = l.length) (n : Nat) (l : List α) :
(List.modifyTailIdx f n l).length = l.length

Alias of List.length_modifyTailIdx.

@[deprecated List.modifyTailIdx_add]
theorem List.modifyNthTail_add {α : Type u_1} (f : List αList α) (n : Nat) (l₁ l₂ : List α) :
List.modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ List.modifyTailIdx f n l₂

Alias of List.modifyTailIdx_add.

@[deprecated List.exists_of_modifyTailIdx]
theorem List.exists_of_modifyNthTail {α : Type u_1} (f : List αList α) {n : Nat} {l : List α} (h : n l.length) :
∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ l₁.length = n List.modifyTailIdx f n l = l₁ ++ f l₂

Alias of List.exists_of_modifyTailIdx.

@[deprecated List.length_modify]
theorem List.length_modifyNth {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
(List.modify f n l).length = l.length

Alias of List.length_modify.

@[deprecated List.length_modify]
theorem List.modifyNth_get?_length {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
(List.modify f n l).length = l.length

Alias of List.length_modify.

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

Alias of List.getElem?_modify_eq.

@[deprecated List.getElem?_modify_eq]
theorem List.get?_modifyNth_eq {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
(List.modify f n l).get? n = f <$> l.get? n
@[deprecated List.getElem?_modify_ne]
theorem List.getElem?_modifyNth_ne {α : Type u_1} (f : αα) {m n : Nat} (l : List α) (h : m n) :
(List.modify f m l)[n]? = l[n]?

Alias of List.getElem?_modify_ne.

@[deprecated List.getElem?_modify_ne]
theorem List.get?_modifyNth_ne {α : Type u_1} (f : αα) {m n : Nat} (l : List α) (h : m n) :
(List.modify f m l).get? n = l.get? n
@[deprecated List.exists_of_modify]
theorem List.exists_of_modifyNth {α : Type u_1} (f : αα) {n : Nat} {l : List α} (h : n < l.length) :
∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ l₁.length = n List.modify f n l = l₁ ++ f a :: l₂

Alias of List.exists_of_modify.

@[deprecated List.modifyTailIdx_eq_take_drop]
theorem List.modifyNthTail_eq_take_drop {α : Type u_1} (f : List αList α) (H : f [] = []) (n : Nat) (l : List α) :

Alias of List.modifyTailIdx_eq_take_drop.

@[deprecated List.modify_eq_take_drop]
theorem List.modifyNth_eq_take_drop {α : Type u_1} (f : αα) (n : Nat) (l : List α) :

Alias of List.modify_eq_take_drop.

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

Alias of List.modify_eq_take_cons_drop.

@[deprecated List.set_eq_modify]
theorem List.set_eq_modifyNth {α : Type u_1} (a : α) (n : Nat) (l : List α) :
l.set n a = List.modify (fun (x : α) => a) n l

Alias of List.set_eq_modify.

@[deprecated List.modify_eq_set_get?]
theorem List.modifyNth_eq_set_get? {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
List.modify f n l = ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l

Alias of List.modify_eq_set_get?.

@[deprecated List.modify_eq_set_get]
theorem List.modifyNth_eq_set_get {α : Type u_1} (f : αα) {n : Nat} {l : List α} (h : n < l.length) :
List.modify f n l = l.set n (f (l.get n, h))

Alias of List.modify_eq_set_get.

@[deprecated List.exists_of_set]
theorem List.exists_of_set' {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ l₁.length = n l.set n a' = l₁ ++ a' :: l₂
@[deprecated List.getElem?_set_self']
theorem List.get?_set_eq {α : Type u_1} (a : α) (n : Nat) (l : List α) :
(l.set n a).get? n = (fun (x : α) => a) <$> l.get? n
@[deprecated List.getElem?_set_eq_of_lt]
theorem List.get?_set_eq_of_lt {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) :
(l.set n a).get? n = some a
@[deprecated List.getElem?_set_ne]
theorem List.get?_set_ne {α : Type u_1} (a : α) {m n : Nat} (l : List α) (h : m n) :
(l.set m a).get? n = l.get? n
@[deprecated List.getElem?_set]
theorem List.get?_set {α : Type u_1} (a : α) {m n : Nat} (l : List α) :
(l.set m a).get? n = if m = n then (fun (x : α) => a) <$> l.get? n else l.get? n