Basic properties of lists

@[deprecated "No deprecation message was provided." (since := "2024-07-27")]

theorem List.le_eq_not_gt {α : Type u} [LT α] (l₁ l₂ : List α) : (l₁ ≤ l₂) = ¬l₂ < l₁

≤ implies not > for lists.

instance List.uniqueOfIsEmpty {α : Type u} [IsEmpty α] : Unique (List α)

There is only one list of an empty type

Equations

• List.uniqueOfIsEmpty = { toInhabited := instInhabitedList, uniq := ⋯ }

instance List.instLawfulIdentityAppendNil_mathlib {α : Type u} : Std.LawfulIdentity Append.append []

instance List.instAssociativeAppend_mathlib {α : Type u} : Std.Associative Append.append

@[simp]

theorem List.cons_injective {α : Type u} {a : α} : Function.Injective (cons a)

theorem List.singleton_injective {α : Type u} : Function.Injective fun (a : α) => [a]

theorem List.set_of_mem_cons {α : Type u} (l : List α) (a : α) : {x : α | x ∈ a :: l} = insert a {x : α | x ∈ l}

mem

theorem Decidable.List.eq_or_ne_mem_of_mem {α : Type u} [DecidableEq α] {a b : α} {l : List α} (h : a ∈ b :: l) : a = b ∨ a ≠ b ∧ a ∈ l

theorem List.mem_pair {α : Type u} {a b c : α} : a ∈ [b, c] ↔ a = b ∨ a = c

@[simp]

theorem List.mem_map_of_injective {α : Type u} {β : Type v} {f : α → β} (H : Function.Injective f) {a : α} {l : List α} : f a ∈ map f l ↔ a ∈ l

@[simp]

theorem Function.Involutive.exists_mem_and_apply_eq_iff {α : Type u} {f : α → α} (hf : Involutive f) (x : α) (l : List α) : (∃ (y : α), y ∈ l ∧ f y = x) ↔ f x ∈ l

theorem List.mem_map_of_involutive {α : Type u} {f : α → α} (hf : Function.Involutive f) {a : α} {l : List α} : a ∈ map f l ↔ f a ∈ l

length

theorem List.length_pos_of_ne_nil {α : Type u_1} {l : List α} : l ≠ [] → 0 < l.length

Alias of the reverse direction of List.length_pos.

theorem List.length_pos_iff_ne_nil {α : Type u} {l : List α} : 0 < l.length ↔ l ≠ []

theorem List.exists_of_length_succ {α : Type u} {n : ℕ} (l : List α) : l.length = n + 1 → ∃ (h : α), ∃ (t : List α), l = h :: t

@[simp]

theorem List.length_injective_iff {α : Type u} : Function.Injective length ↔ Subsingleton α

@[simp]

theorem List.length_injective {α : Type u} [Subsingleton α] : Function.Injective length

theorem List.length_eq_two {α : Type u} {l : List α} : l.length = 2 ↔ ∃ (a : α), ∃ (b : α), l = [a, b]

theorem List.length_eq_three {α : Type u} {l : List α} : l.length = 3 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), l = [a, b, c]

set-theoretic notation of lists

instance List.instSingletonList {α : Type u} : Singleton α (List α)

Equations

• List.instSingletonList = { singleton := fun (x : α) => [x] }

instance List.instInsertOfDecidableEq_mathlib {α : Type u} [DecidableEq α] : Insert α (List α)

Equations

• List.instInsertOfDecidableEq_mathlib = { insert := List.insert }

instance List.instLawfulSingleton_mathlib {α : Type u} [DecidableEq α] : LawfulSingleton α (List α)

theorem List.singleton_eq {α : Type u} (x : α) : {x} = [x]

theorem List.insert_neg {α : Type u} [DecidableEq α] {x : α} {l : List α} (h : ¬x ∈ l) : insert x l = x :: l

theorem List.insert_pos {α : Type u} [DecidableEq α] {x : α} {l : List α} (h : x ∈ l) : insert x l = l

theorem List.doubleton_eq {α : Type u} [DecidableEq α] {x y : α} (h : x ≠ y) : {x, y} = [x, y]

bounded quantifiers over lists

theorem List.forall_mem_of_forall_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : List α} (h : ∀ (x : α), x ∈ a :: l → p x) (x : α) : x ∈ l → p x

theorem List.exists_mem_cons_of {α : Type u} {p : α → Prop} {a : α} (l : List α) (h : p a) : ∃ (x : α), x ∈ a :: l ∧ p x

theorem List.exists_mem_cons_of_exists {α : Type u} {p : α → Prop} {a : α} {l : List α} : (∃ (x : α), x ∈ l ∧ p x) → ∃ (x : α), x ∈ a :: l ∧ p x

theorem List.or_exists_of_exists_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : List α} : (∃ (x : α), x ∈ a :: l ∧ p x) → p a ∨ ∃ (x : α), x ∈ l ∧ p x

theorem List.exists_mem_cons_iff {α : Type u} (p : α → Prop) (a : α) (l : List α) : (∃ (x : α), x ∈ a :: l ∧ p x) ↔ p a ∨ ∃ (x : α), x ∈ l ∧ p x

list subset

theorem List.cons_subset_of_subset_of_mem {α : Type u} {a : α} {l m : List α} (ainm : a ∈ m) (lsubm : l ⊆ m) : a :: l ⊆ m

theorem List.append_subset_of_subset_of_subset {α : Type u} {l₁ l₂ l : List α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) : l₁ ++ l₂ ⊆ l

theorem List.map_subset_iff {α : Type u} {β : Type v} {l₁ l₂ : List α} (f : α → β) (h : Function.Injective f) : map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂

append

theorem List.append_eq_has_append {α : Type u} {L₁ L₂ : List α} : L₁.append L₂ = L₁ ++ L₂

theorem List.append_right_injective {α : Type u} (s : List α) : Function.Injective fun (t : List α) => s ++ t

theorem List.append_left_injective {α : Type u} (t : List α) : Function.Injective fun (s : List α) => s ++ t

replicate

theorem List.eq_replicate_length {α : Type u} {a : α} {l : List α} : l = replicate l.length a ↔ ∀ (b : α), b ∈ l → b = a

theorem List.replicate_add {α : Type u} (m n : ℕ) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a

theorem List.replicate_subset_singleton {α : Type u} (n : ℕ) (a : α) : replicate n a ⊆ [a]

theorem List.subset_singleton_iff {α : Type u} {a : α} {L : List α} : L ⊆ [a] ↔ ∃ (n : ℕ), L = replicate n a

theorem List.replicate_right_injective {α : Type u} {n : ℕ} (hn : n ≠ 0) : Function.Injective (replicate n)

theorem List.replicate_right_inj {α : Type u} {a b : α} {n : ℕ} (hn : n ≠ 0) : replicate n a = replicate n b ↔ a = b

theorem List.replicate_right_inj' {α : Type u} {a b : α} {n : ℕ} : replicate n a = replicate n b ↔ n = 0 ∨ a = b

theorem List.replicate_left_injective {α : Type u} (a : α) : Function.Injective fun (x : ℕ) => replicate x a

theorem List.replicate_left_inj {α : Type u} {a : α} {n m : ℕ} : replicate n a = replicate m a ↔ n = m

pure

theorem List.mem_pure {α : Type u} (x y : α) : x ∈ pure y ↔ x = y

bind

@[simp]

theorem List.bind_eq_flatMap {α β : Type u_2} (f : α → List β) (l : List α) : l >>= f = l.flatMap f

@[deprecated List.bind_eq_flatMap (since := "2024-10-16")]

theorem List.bind_eq_bind {α β : Type u_2} (f : α → List β) (l : List α) : l >>= f = l.flatMap f

Alias of List.bind_eq_flatMap.

concat

reverse

theorem List.reverse_cons' {α : Type u} (a : α) (l : List α) : (a :: l).reverse = l.reverse.concat a

theorem List.reverse_concat' {α : Type u} (l : List α) (a : α) : (l ++ [a]).reverse = a :: l.reverse

@[simp]

theorem List.reverse_singleton {α : Type u} (a : α) : [a].reverse = [a]

@[simp]

theorem List.reverse_involutive {α : Type u} : Function.Involutive reverse

@[simp]

theorem List.reverse_injective {α : Type u} : Function.Injective reverse

theorem List.reverse_surjective {α : Type u} : Function.Surjective reverse

theorem List.reverse_bijective {α : Type u} : Function.Bijective reverse

theorem List.concat_eq_reverse_cons {α : Type u} (a : α) (l : List α) : l.concat a = (a :: l.reverse).reverse

theorem List.map_reverseAux {α : Type u} {β : Type v} (f : α → β) (l₁ l₂ : List α) : map f (l₁.reverseAux l₂) = (map f l₁).reverseAux (map f l₂)

getLast

theorem List.getLast_append_singleton {α : Type u} {a : α} (l : List α) : (l ++ [a]).getLast ⋯ = a

theorem List.getLast_append' {α : Type u} (l₁ l₂ : List α) (h : l₂ ≠ []) : (l₁ ++ l₂).getLast ⋯ = l₂.getLast h

theorem List.getLast_concat' {α : Type u} {a : α} (l : List α) : (l.concat a).getLast ⋯ = a

@[simp]

theorem List.getLast_singleton' {α : Type u} (a : α) : [a].getLast ⋯ = a

@[simp]

theorem List.getLast_cons_cons {α : Type u} (a₁ a₂ : α) (l : List α) : (a₁ :: a₂ :: l).getLast ⋯ = (a₂ :: l).getLast ⋯

theorem List.dropLast_append_getLast {α : Type u} {l : List α} (h : l ≠ []) : l.dropLast ++ [l.getLast h] = l

theorem List.getLast_congr {α : Type u} {l₁ l₂ : List α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) : l₁.getLast h₁ = l₂.getLast h₂

theorem List.getLast_replicate_succ {α : Type u} (m : ℕ) (a : α) : (replicate (m + 1) a).getLast ⋯ = a

theorem List.getLast_filter' {α : Type u} {p : α → Bool} (l : List α) (hlp : filter p l ≠ []) : p (l.getLast ⋯) = true → (filter p l).getLast hlp = l.getLast ⋯

If the last element of l does not satisfy p, then it is also the last element of l.filter p.

getLast?

@[deprecated List.getLast?_eq_none_iff (since := "2024-09-06")]

theorem List.getLast?_eq_none {α : Type u_1} {xs : List α} : xs.getLast? = none ↔ xs = []

Alias of List.getLast?_eq_none_iff.

@[deprecated List.getLast?_eq_none (since := "2024-06-20")]

theorem List.getLast?_isNone {α : Type u_1} {xs : List α} : xs.getLast? = none ↔ xs = []

Alias of List.getLast?_eq_none_iff.

---

Alias of List.getLast?_eq_none_iff.

theorem List.mem_getLast?_eq_getLast {α : Type u} {l : List α} {x : α} : x ∈ l.getLast? → ∃ (h : l ≠ []), x = l.getLast h

theorem List.getLast?_eq_getLast_of_ne_nil {α : Type u} {l : List α} (h : l ≠ []) : l.getLast? = some (l.getLast h)

theorem List.mem_getLast?_cons {α : Type u} {x y : α} {l : List α} : x ∈ l.getLast? → x ∈ (y :: l).getLast?

theorem List.dropLast_append_getLast? {α : Type u} {l : List α} (a : α) : a ∈ l.getLast? → l.dropLast ++ [a] = l

theorem List.getLastI_eq_getLast? {α : Type u} [Inhabited α] (l : List α) : l.getLastI = l.getLast?.iget

theorem List.getLast?_append_cons {α : Type u} (l₁ : List α) (a : α) (l₂ : List α) : (l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?

theorem List.getLast?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} : l₂ ≠ [] → (l₁ ++ l₂).getLast? = l₂.getLast?

theorem List.mem_getLast?_append_of_mem_getLast? {α : Type u} {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) : x ∈ (l₁ ++ l₂).getLast?

head(!?) and tail

@[simp]

theorem List.head!_nil {α : Type u} [Inhabited α] : [].head! = default

@[simp]

theorem List.head_cons_tail {α : Type u} (x : List α) (h : x ≠ []) : x.head h :: x.tail = x

theorem List.head_eq_getElem_zero {α : Type u} {l : List α} (hl : l ≠ []) : l.head hl = l[0]

theorem List.head!_eq_head? {α : Type u} [Inhabited α] (l : List α) : l.head! = l.head?.iget

theorem List.surjective_head! {α : Type u} [Inhabited α] : Function.Surjective head!

theorem List.surjective_head? {α : Type u} : Function.Surjective head?

theorem List.surjective_tail {α : Type u} : Function.Surjective tail

theorem List.eq_cons_of_mem_head? {α : Type u} {x : α} {l : List α} : x ∈ l.head? → l = x :: l.tail

@[simp]

theorem List.head!_cons {α : Type u} [Inhabited α] (a : α) (l : List α) : (a :: l).head! = a

@[simp]

theorem List.head!_append {α : Type u} [Inhabited α] (t : List α) {s : List α} (h : s ≠ []) : (s ++ t).head! = s.head!

theorem List.mem_head?_append_of_mem_head? {α : Type u} {s t : List α} {x : α} (h : x ∈ s.head?) : x ∈ (s ++ t).head?

theorem List.head?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} : l₁ ≠ [] → (l₁ ++ l₂).head? = l₁.head?

theorem List.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : List α} (h : l ≠ []) : (l ++ [a]).tail = l.tail ++ [a]

theorem List.cons_head?_tail {α : Type u} {l : List α} {a : α} : a ∈ l.head? → a :: l.tail = l

theorem List.head!_mem_head? {α : Type u} [Inhabited α] {l : List α} : l ≠ [] → l.head! ∈ l.head?

theorem List.cons_head!_tail {α : Type u} [Inhabited α] {l : List α} (h : l ≠ []) : l.head! :: l.tail = l

theorem List.head!_mem_self {α : Type u} [Inhabited α] {l : List α} (h : l ≠ []) : l.head! ∈ l

theorem List.get_eq_get? {α : Type u} (l : List α) (i : Fin l.length) : l.get i = (l.get? ↑i).get ⋯

theorem List.exists_mem_iff_getElem {α : Type u} {l : List α} {p : α → Prop} : (∃ (x : α), x ∈ l ∧ p x) ↔ ∃ (i : ℕ), ∃ (x : i < l.length), p l[i]

theorem List.forall_mem_iff_getElem {α : Type u} {l : List α} {p : α → Prop} : (∀ (x : α), x ∈ l → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p l[i]

theorem List.get_tail {α : Type u} (l : List α) (i : ℕ) (h : i < l.tail.length) (h' : i + 1 < l.length := ⋯) : l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩

@[deprecated "No deprecation message was provided." (since := "2024-08-22")]

theorem List.get_cons {α : Type u} {l : List α} {a : α} {n : ℕ} (hl : n < (a :: l).length) : (a :: l).get ⟨n, hl⟩ = if hn : n = 0 then a else l.get ⟨n - 1, ⋯⟩

Induction from the right

@[irreducible]

def List.reverseRecOn {α : Type u} {motive : List α → Sort u_2} (l : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : motive l

Induction principle from the right for lists: if a property holds for the empty list, and for l ++ [a] if it holds for l, then it holds for all lists. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem List.reverseRecOn_nil {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : reverseRecOn [] nil append_singleton = nil

@[simp]

theorem List.reverseRecOn_concat {α : Type u} {motive : List α → Sort u_2} (x : α) (xs : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (reverseRecOn xs nil append_singleton)

@[irreducible]

def List.bidirectionalRec {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (l : List α) : motive l

Bidirectional induction principle for lists: if a property holds for the empty list, the singleton list, and a :: (l ++ [b]) from l, then it holds for all lists. This can be used to prove statements about palindromes. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

• One or more equations did not get rendered due to their size.
• List.bidirectionalRec nil singleton cons_append [] = nil
• List.bidirectionalRec nil singleton cons_append [a] = singleton a

@[simp]

theorem List.bidirectionalRec_nil {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) : bidirectionalRec nil singleton cons_append [] = nil

@[simp]

theorem List.bidirectionalRec_singleton {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a : α) : bidirectionalRec nil singleton cons_append [a] = singleton a

@[simp]

theorem List.bidirectionalRec_cons_append {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a : α) (l : List α) (b : α) : bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) = cons_append a l b (bidirectionalRec nil singleton cons_append l)

@[reducible, inline]

abbrev List.bidirectionalRecOn {α : Type u} {C : List α → Sort u_2} (l : List α) (H0 : C []) (H1 : (a : α) → C [a]) (Hn : (a : α) → (l : List α) → (b : α) → C l → C (a :: (l ++ [b]))) : C l

Like bidirectionalRec, but with the list parameter placed first.

Equations

• l.bidirectionalRecOn H0 H1 Hn = List.bidirectionalRec H0 H1 Hn l

sublists

theorem List.Sublist.cons_cons {α : Type u} {l₁ l₂ : List α} (a : α) (s : l₁.Sublist l₂) : (a :: l₁).Sublist (a :: l₂)

theorem List.cons_sublist_cons' {α : Type u} {l₁ l₂ : List α} {a b : α} : (a :: l₁).Sublist (b :: l₂) ↔ (a :: l₁).Sublist l₂ ∨ a = b ∧ l₁.Sublist l₂

theorem List.sublist_cons_of_sublist {α : Type u} {l₁ l₂ : List α} (a : α) (h : l₁.Sublist l₂) : l₁.Sublist (a :: l₂)

@[deprecated "No deprecation message was provided." (since := "2024-04-07")]

theorem List.sublist_of_cons_sublist_cons {α : Type u} {l₁ l₂ : List α} {a : α} (h : (a :: l₁).Sublist (a :: l₂)) : l₁.Sublist l₂

@[deprecated List.cons_sublist_cons (since := "2024-04-07")]

theorem List.cons_sublist_cons_iff {α✝ : Type u_1} {a : α✝} {l₁ l₂ : List α✝} : (a :: l₁).Sublist (a :: l₂) ↔ l₁.Sublist l₂

Alias of List.cons_sublist_cons.

theorem List.sublist_nil_iff_eq_nil {α : Type u_1} {l : List α} : l.Sublist [] ↔ l = []

Alias of List.sublist_nil.

@[simp]

theorem List.sublist_singleton {α : Type u} {l : List α} {a : α} : l.Sublist [a] ↔ l = [] ∨ l = [a]

theorem List.Sublist.antisymm {α : Type u} {l₁ l₂ : List α} (s₁ : l₁.Sublist l₂) (s₂ : l₂.Sublist l₁) : l₁ = l₂

instance List.decidableSublist {α : Type u} [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁.Sublist l₂)

Equations

• [].decidableSublist x✝ = isTrue ⋯
• (head :: tail).decidableSublist [] = isFalse ⋯
• (a :: l₁).decidableSublist (b :: l₂) = if h : a = b then decidable_of_decidable_of_iff ⋯ else decidable_of_decidable_of_iff ⋯

theorem List.Sublist.of_cons_of_ne {α : Type u} {l₁ l₂ : List α} {a b : α} (h₁ : a ≠ b) (h₂ : (a :: l₁).Sublist (b :: l₂)) : (a :: l₁).Sublist l₂

If the first element of two lists are different, then a sublist relation can be reduced.

indexOf

@[simp]

theorem List.indexOf_cons_self {α : Type u} [DecidableEq α] (a : α) (l : List α) : indexOf a (a :: l) = 0

theorem List.indexOf_cons_eq {α : Type u} [DecidableEq α] {a b : α} (l : List α) : b = a → indexOf a (b :: l) = 0

@[simp]

theorem List.indexOf_cons_ne {α : Type u} [DecidableEq α] {a b : α} (l : List α) : b ≠ a → indexOf a (b :: l) = (indexOf a l).succ

theorem List.indexOf_eq_length {α : Type u} [DecidableEq α] {a : α} {l : List α} : indexOf a l = l.length ↔ ¬a ∈ l

@[simp]

theorem List.indexOf_of_not_mem {α : Type u} [DecidableEq α] {l : List α} {a : α} : ¬a ∈ l → indexOf a l = l.length

theorem List.indexOf_le_length {α : Type u} [DecidableEq α] {a : α} {l : List α} : indexOf a l ≤ l.length

theorem List.indexOf_lt_length_iff {α : Type u} [DecidableEq α] {a : α} {l : List α} : indexOf a l < l.length ↔ a ∈ l

@[deprecated List.indexOf_lt_length_iff (since := "2025-01-22")]

theorem List.indexOf_lt_length {α : Type u} [DecidableEq α] {a : α} {l : List α} : indexOf a l < l.length ↔ a ∈ l

Alias of List.indexOf_lt_length_iff.

theorem List.indexOf_append_of_mem {α : Type u} {l₁ l₂ : List α} [DecidableEq α] {a : α} (h : a ∈ l₁) : indexOf a (l₁ ++ l₂) = indexOf a l₁

theorem List.indexOf_append_of_not_mem {α : Type u} {l₁ l₂ : List α} [DecidableEq α] {a : α} (h : ¬a ∈ l₁) : indexOf a (l₁ ++ l₂) = l₁.length + indexOf a l₂

nth element

@[simp]

theorem List.getElem?_length {α : Type u} (l : List α) : l[l.length]? = none

@[deprecated List.getElem?_length (since := "2024-06-12")]

theorem List.get?_length {α : Type u} (l : List α) : l.get? l.length = none

@[deprecated List.get?_inj (since := "2024-05-03")]

theorem List.get?_injective {i : ℕ} {α✝ : Type u_1} {xs : List α✝} {j : ℕ} (h₀ : i < xs.length) (h₁ : xs.Nodup) (h₂ : xs.get? i = xs.get? j) : i = j

Alias of List.get?_inj.

theorem List.getElem_map_rev {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : ℕ} {h : n < l.length} : f l[n] = (map f l)[n]

A version of getElem_map that can be used for rewriting.

@[deprecated List.getElem_map_rev (since := "2024-06-12")]

theorem List.get_map_rev {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : Fin l.length} : f (l.get n) = (map f l).get ⟨↑n, ⋯⟩

A version of get_map that can be used for rewriting.

theorem List.get_length_sub_one {α : Type u} {l : List α} (h : l.length - 1 < l.length) : l.get ⟨l.length - 1, h⟩ = l.getLast ⋯

theorem List.take_one_drop_eq_of_lt_length {α : Type u} {l : List α} {n : ℕ} (h : n < l.length) : take 1 (drop n l) = [l.get ⟨n, h⟩]

theorem List.ext_get?' {α : Type u} {l₁ l₂ : List α} (h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁.get? n = l₂.get? n) : l₁ = l₂

theorem List.ext_get?_iff {α : Type u} {l₁ l₂ : List α} : l₁ = l₂ ↔ ∀ (n : ℕ), l₁.get? n = l₂.get? n

theorem List.ext_get_iff {α : Type u} {l₁ l₂ : List α} : l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

theorem List.ext_get?_iff' {α : Type u} {l₁ l₂ : List α} : l₁ = l₂ ↔ ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁.get? n = l₂.get? n

theorem List.ext_getElem! {α : Type u} {l₁ l₂ : List α} [Inhabited α] (hl : l₁.length = l₂.length) (h : ∀ (n : ℕ), l₁[n]! = l₂[n]!) : l₁ = l₂

If two lists l₁ and l₂ are the same length and l₁[n]! = l₂[n]! for all n, then the lists are equal.

@[simp]

theorem List.getElem_indexOf {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : indexOf a l < l.length) : l[indexOf a l] = a

theorem List.indexOf_get {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : indexOf a l < l.length) : l.get ⟨indexOf a l, h⟩ = a

@[simp]

theorem List.getElem?_indexOf {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l[indexOf a l]? = some a

theorem List.indexOf_get? {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l.get? (indexOf a l) = some a

theorem List.indexOf_inj {α : Type u} [DecidableEq α] {l : List α} {x y : α} (hx : x ∈ l) (hy : y ∈ l) : indexOf x l = indexOf y l ↔ x = y

@[deprecated List.getElem_reverse (since := "2024-06-12")]

theorem List.get_reverse {α : Type u} (l : List α) (i : ℕ) (h1 : l.length - 1 - i < l.reverse.length) (h2 : i < l.length) : l.reverse.get ⟨l.length - 1 - i, h1⟩ = l.get ⟨i, h2⟩

theorem List.get_reverse' {α : Type u} (l : List α) (n : Fin l.reverse.length) (hn' : l.length - 1 - ↑n < l.length) : l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩

theorem List.eq_cons_of_length_one {α : Type u} {l : List α} (h : l.length = 1) : l = [l.get ⟨0, ⋯⟩]

@[deprecated List.modifyTailIdx_modifyTailIdx_le (since := "2024-10-21")]

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

Alias of List.modifyTailIdx_modifyTailIdx_le.

@[deprecated List.modifyTailIdx_modifyTailIdx_self (since := "2024-10-21")]

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

Alias of List.modifyTailIdx_modifyTailIdx_self.

@[deprecated List.eraseIdx_eq_modifyTailIdx (since := "2024-05-04")]

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

Alias of List.eraseIdx_eq_modifyTailIdx.

@[deprecated List.modify_eq_set (since := "2024-10-21")]

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

Alias of List.modify_eq_set.

@[simp]

theorem List.getElem_set_of_ne {α : Type u} {l : List α} {i j : ℕ} (h : i ≠ j) (a : α) (hj : j < (l.set i a).length) : (l.set i a)[j] = l[j]

@[deprecated List.getElem_set_of_ne (since := "2024-06-12")]

theorem List.get_set_of_ne {α : Type u} {l : List α} {i j : ℕ} (h : i ≠ j) (a : α) (hj : j < (l.set i a).length) : (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, ⋯⟩

map

@[deprecated List.map_congr_left (since := "2024-06-21")]

theorem List.map_congr {α✝ : Type u_1} {l : List α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} (h : ∀ (a : α✝), a ∈ l → f a = g a) : map f l = map g l

Alias of List.map_congr_left.

theorem List.flatMap_pure_eq_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : l.flatMap (pure ∘ f) = map f l

@[deprecated List.flatMap_pure_eq_map (since := "2024-10-16")]

theorem List.bind_pure_eq_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : l.flatMap (pure ∘ f) = map f l

Alias of List.flatMap_pure_eq_map.

theorem List.flatMap_congr {α : Type u} {β : Type v} {l : List α} {f g : α → List β} (h : ∀ (x : α), x ∈ l → f x = g x) : l.flatMap f = l.flatMap g

@[deprecated List.flatMap_congr (since := "2024-10-16")]

theorem List.bind_congr {α : Type u} {β : Type v} {l : List α} {f g : α → List β} (h : ∀ (x : α), x ∈ l → f x = g x) : l.flatMap f = l.flatMap g

Alias of List.flatMap_congr.

theorem List.infix_flatMap_of_mem {α : Type u} {a : α} {as : List α} (h : a ∈ as) (f : α → List α) : f a <:+: as.flatMap f

@[deprecated List.infix_flatMap_of_mem (since := "2024-10-16")]

theorem List.infix_bind_of_mem {α : Type u} {a : α} {as : List α} (h : a ∈ as) (f : α → List α) : f a <:+: as.flatMap f

Alias of List.infix_flatMap_of_mem.

@[simp]

theorem List.map_eq_map {α β : Type u_2} (f : α → β) (l : List α) : f <$> l = map f l

theorem List.comp_map {α : Type u} {β : Type v} {γ : Type w} (h : β → γ) (g : α → β) (l : List α) : map (h ∘ g) l = map h (map g l)

A single List.map of a composition of functions is equal to composing a List.map with another List.map, fully applied. This is the reverse direction of List.map_map.

@[simp]

theorem List.map_comp_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) : map g ∘ map f = map (g ∘ f)

Composing a List.map with another List.map is equal to a single List.map of composed functions.

theorem Function.LeftInverse.list_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : LeftInverse f g) : LeftInverse (List.map f) (List.map g)

theorem Function.RightInverse.list_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : RightInverse f g) : RightInverse (List.map f) (List.map g)

theorem Function.Involutive.list_map {α : Type u} {f : α → α} (h : Involutive f) : Involutive (List.map f)

@[simp]

theorem List.map_leftInverse_iff {α : Type u} {β : Type v} {f : α → β} {g : β → α} : Function.LeftInverse (map f) (map g) ↔ Function.LeftInverse f g

@[simp]

theorem List.map_rightInverse_iff {α : Type u} {β : Type v} {f : α → β} {g : β → α} : Function.RightInverse (map f) (map g) ↔ Function.RightInverse f g

@[simp]

theorem List.map_involutive_iff {α : Type u} {f : α → α} : Function.Involutive (map f) ↔ Function.Involutive f

theorem Function.Injective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Injective f) : Injective (List.map f)

@[simp]

theorem List.map_injective_iff {α : Type u} {β : Type v} {f : α → β} : Function.Injective (map f) ↔ Function.Injective f

theorem Function.Surjective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Surjective f) : Surjective (List.map f)

@[simp]

theorem List.map_surjective_iff {α : Type u} {β : Type v} {f : α → β} : Function.Surjective (map f) ↔ Function.Surjective f

theorem Function.Bijective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Bijective f) : Bijective (List.map f)

@[simp]

theorem List.map_bijective_iff {α : Type u} {β : Type v} {f : α → β} : Function.Bijective (map f) ↔ Function.Bijective f

theorem List.eq_of_mem_map_const {α : Type u} {β : Type v} {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (Function.const α b₂) l) : b₁ = b₂

take, drop

@[simp]

theorem List.take_eq_self_iff {α : Type u} (x : List α) {n : ℕ} : take n x = x ↔ x.length ≤ n

@[simp]

theorem List.take_self_eq_iff {α : Type u} (x : List α) {n : ℕ} : x = take n x ↔ x.length ≤ n

@[simp]

theorem List.take_eq_left_iff {α : Type u} {x y : List α} {n : ℕ} : take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

@[simp]

theorem List.left_eq_take_iff {α : Type u} {x y : List α} {n : ℕ} : take n x = take n (x ++ y) ↔ y = [] ∨ n ≤ x.length

@[simp]

theorem List.drop_take_append_drop {α : Type u} (x : List α) (m n : ℕ) : take n (drop m x) ++ drop (m + n) x = drop m x

@[simp]

theorem List.drop_take_append_drop' {α : Type u} (x : List α) (m n : ℕ) : take n (drop m x) ++ drop (n + m) x = drop m x

Compared to drop_take_append_drop, the order of summands is swapped.

theorem List.take_concat_get' {α : Type u} (l : List α) (i : ℕ) (h : i < l.length) : take i l ++ [l[i]] = take (i + 1) l

take_concat_get in simp normal form

theorem List.eq_nil_or_concat' {α : Type u} (l : List α) : l = [] ∨ ∃ (L : List α), ∃ (b : α), l = L ++ [b]

eq_nil_or_concat in simp normal form

theorem List.cons_getElem_drop_succ {α : Type u} {l : List α} {n : ℕ} {h : n < l.length} : l[n] :: drop (n + 1) l = drop n l

theorem List.cons_get_drop_succ {α : Type u} {l : List α} {n : Fin l.length} : l.get n :: drop (↑n + 1) l = drop (↑n) l

theorem List.drop_length_sub_one {α : Type u} {l : List α} (h : l ≠ []) : drop (l.length - 1) l = [l.getLast h]

@[simp]

theorem List.takeI_length {α : Type u} [Inhabited α] (n : ℕ) (l : List α) : (takeI n l).length = n

@[simp]

theorem List.takeI_nil {α : Type u} [Inhabited α] (n : ℕ) : takeI n [] = replicate n default

theorem List.takeI_eq_take {α : Type u} [Inhabited α] {n : ℕ} {l : List α} : n ≤ l.length → takeI n l = take n l

@[simp]

theorem List.takeI_left {α : Type u} [Inhabited α] (l₁ l₂ : List α) : takeI l₁.length (l₁ ++ l₂) = l₁

theorem List.takeI_left' {α : Type u} [Inhabited α] {l₁ l₂ : List α} {n : ℕ} (h : l₁.length = n) : takeI n (l₁ ++ l₂) = l₁

@[simp]

theorem List.takeD_length {α : Type u} (n : ℕ) (l : List α) (a : α) : (takeD n l a).length = n

theorem List.takeD_eq_take {α : Type u} {n : ℕ} {l : List α} (a : α) : n ≤ l.length → takeD n l a = take n l

@[simp]

theorem List.takeD_left {α : Type u} (l₁ l₂ : List α) (a : α) : takeD l₁.length (l₁ ++ l₂) a = l₁

theorem List.takeD_left' {α : Type u} {l₁ l₂ : List α} {n : ℕ} {a : α} (h : l₁.length = n) : takeD n (l₁ ++ l₂) a = l₁

foldl, foldr

theorem List.foldl_ext {α : Type u} {β : Type v} (f g : α → β → α) (a : α) {l : List β} (H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b) : foldl f a l = foldl g a l

theorem List.foldr_ext {α : Type u} {β : Type v} (f g : α → β → β) (b : β) {l : List α} (H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b) : foldr f b l = foldr g b l

theorem List.foldl_concat {α : Type u} {β : Type v} (f : β → α → β) (b : β) (x : α) (xs : List α) : foldl f b (xs ++ [x]) = f (foldl f b xs) x

theorem List.foldr_concat {α : Type u} {β : Type v} (f : α → β → β) (b : β) (x : α) (xs : List α) : foldr f b (xs ++ [x]) = foldr f (f x b) xs

theorem List.foldl_fixed' {α : Type u} {β : Type v} {f : α → β → α} {a : α} (hf : ∀ (b : β), f a b = a) (l : List β) : foldl f a l = a

theorem List.foldr_fixed' {α : Type u} {β : Type v} {f : α → β → β} {b : β} (hf : ∀ (a : α), f a b = b) (l : List α) : foldr f b l = b

@[simp]

theorem List.foldl_fixed {α : Type u} {β : Type v} {a : α} (l : List β) : foldl (fun (a : α) (x : β) => a) a l = a

@[simp]

theorem List.foldr_fixed {α : Type u} {β : Type v} {b : β} (l : List α) : foldr (fun (x : α) (b : β) => b) b l = b

theorem List.foldr_eta {α : Type u} (l : List α) : foldr cons [] l = l

theorem List.reverse_foldl {α : Type u} {l : List α} : (foldl (fun (t : List α) (h : α) => h :: t) [] l).reverse = l

theorem List.foldl_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β) (op₃ : γ → ι → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i) : foldl op₃ (f a b) l = f (foldl op₁ a l) (foldl op₂ b l)

theorem List.foldr_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : ι → α → α) (op₂ : ι → β → β) (op₃ : ι → γ → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)) : foldr op₃ (f a b) l = f (foldr op₁ a l) (foldr op₂ b l)

theorem List.injective_foldl_comp {α : Type u} {l : List (α → α)} {f : α → α} (hl : ∀ (f : α → α), f ∈ l → Function.Injective f) (hf : Function.Injective f) : Function.Injective (foldl Function.comp f l)

theorem List.append_cons_inj_of_not_mem {α : Type u} {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α} (notin_x : ¬a₂ ∈ x₁) (notin_z : ¬a₂ ∈ z₁) : x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Consider two lists l₁ and l₂ with designated elements a₁ and a₂ somewhere in them: l₁ = x₁ ++ [a₁] ++ z₁ and l₂ = x₂ ++ [a₂] ++ z₂. Assume the designated element a₂ is present in neither x₁ nor z₁. We conclude that the lists are equal (l₁ = l₂) if and only if their respective parts are equal (x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂).

theorem List.length_scanl {α : Type u} {β : Type v} {f : β → α → β} (a : β) (l : List α) : (scanl f a l).length = l.length + 1

@[simp]

theorem List.scanl_nil {α : Type u} {β : Type v} {f : β → α → β} (b : β) : scanl f b [] = [b]

@[simp]

theorem List.scanl_cons {α : Type u} {β : Type v} {f : β → α → β} {b : β} {a : α} {l : List α} : scanl f b (a :: l) = [b] ++ scanl f (f b a) l

@[simp]

theorem List.getElem?_scanl_zero {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} : (scanl f b l)[0]? = some b

@[deprecated List.getElem?_scanl_zero (since := "2024-06-12")]

theorem List.get?_zero_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} : (scanl f b l).get? 0 = some b

@[simp]

theorem List.getElem_scanl_zero {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {h : 0 < (scanl f b l).length} : (scanl f b l)[0] = b

@[deprecated List.getElem_scanl_zero (since := "2024-06-12")]

theorem List.get_zero_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {h : 0 < (scanl f b l).length} : (scanl f b l).get ⟨0, h⟩ = b

theorem List.get?_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {i : ℕ} : (scanl f b l).get? (i + 1) = ((scanl f b l).get? i).bind fun (x : β) => Option.map (fun (y : α) => f x y) (l.get? i)

theorem List.getElem_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {i : ℕ} (h : i + 1 < (scanl f b l).length) : (scanl f b l)[i + 1] = f (scanl f b l)[i] l[i]

@[deprecated List.getElem_succ_scanl (since := "2024-08-22")]

theorem List.get_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {i : ℕ} {h : i + 1 < (scanl f b l).length} : (scanl f b l).get ⟨i + 1, h⟩ = f ((scanl f b l).get ⟨i, ⋯⟩) (l.get ⟨i, ⋯⟩)

@[simp]

theorem List.scanr_nil {α : Type u} {β : Type v} (f : α → β → β) (b : β) : scanr f b [] = [b]

@[simp]

theorem List.scanr_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : List α) : scanr f b (a :: l) = foldr f b (a :: l) :: scanr f b l

theorem List.foldl1_eq_foldr1 {α : Type u} {f : α → α → α} [hassoc : Std.Associative f] (a b : α) (l : List α) : foldl f a (l ++ [b]) = foldr f b (a :: l)

theorem List.foldl_eq_of_comm_of_assoc {α : Type u} {f : α → α → α} [hcomm : Std.Commutative f] [hassoc : Std.Associative f] (a b : α) (l : List α) : foldl f a (b :: l) = f b (foldl f a l)

theorem List.foldl_eq_foldr {α : Type u} {f : α → α → α} [Std.Commutative f] [Std.Associative f] (a : α) (l : List α) : foldl f a l = foldr f a l

theorem List.foldl_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (b : β) (l : List β) : foldl f a (b :: l) = f (foldl f a l) b

theorem List.foldl_eq_foldr' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (l : List β) : foldl f a l = foldr (flip f) a l

theorem List.foldr_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → β} (hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)) (a : β) (b : α) (l : List α) : foldr f a (b :: l) = foldr f (f b a) l

theorem List.foldl_op_eq_op_foldr_assoc {α : Type u} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α} : op (foldl op a₁ l) a₂ = op a₁ (foldr (fun (x1 x2 : α) => op x1 x2) a₂ l)

theorem List.foldl_assoc_comm_cons {α : Type u} {op : α → α → α} [ha : Std.Associative op] [hc : Std.Commutative op] {l : List α} {a₁ a₂ : α} : foldl op a₂ (a₁ :: l) = op a₁ (foldl op a₂ l)

foldlM, foldrM, mapM

theorem List.foldrM_eq_foldr {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : α → β → m β) (b : β) (l : List α) : foldrM f b l = foldr (fun (a : α) (mb : m β) => mb >>= f a) (pure b) l

theorem List.foldlM_eq_foldl {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : β → α → m β) (b : β) (l : List α) : List.foldlM f b l = foldl (fun (mb : m β) (a : α) => do let b ← mb f b a) (pure b) l

intersperse

@[simp]

theorem List.intersperse_singleton {α : Type u} (a b : α) : intersperse a [b] = [b]

@[simp]

theorem List.intersperse_cons_cons {α : Type u} (a b c : α) (tl : List α) : intersperse a (b :: c :: tl) = b :: a :: intersperse a (c :: tl)

splitAt and splitOn

@[deprecated List.splitAt_eq (since := "2024-08-17")]

theorem List.splitAt_eq_take_drop {α : Type u_1} (n : ℕ) (l : List α) : splitAt n l = (take n l, drop n l)

Alias of List.splitAt_eq.

@[simp]

theorem List.splitOn_nil {α : Type u} [DecidableEq α] (a : α) : splitOn a [] = [[]]

@[simp]

theorem List.splitOnP_nil {α : Type u} (p : α → Bool) : splitOnP p [] = [[]]

theorem List.splitOnP.go_ne_nil {α : Type u} (p : α → Bool) (xs acc : List α) : go p xs acc ≠ []

theorem List.splitOnP.go_acc {α : Type u} (p : α → Bool) (xs acc : List α) : go p xs acc = modifyHead (fun (x : List α) => acc.reverse ++ x) (splitOnP p xs)

theorem List.splitOnP_ne_nil {α : Type u} (p : α → Bool) (xs : List α) : splitOnP p xs ≠ []

@[simp]

theorem List.splitOnP_cons {α : Type u} (p : α → Bool) (x : α) (xs : List α) : splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)

theorem List.splitOnP_spec {α : Type u} (p : α → Bool) (as : List α) : (zipWith (fun (x1 x2 : List α) => x1 ++ x2) (splitOnP p as) (map (fun (x : α) => [x]) (filter p as) ++ [[]])).flatten = as

The original list L can be recovered by flattening the lists produced by splitOnP p L, interspersed with the elements L.filter p.

theorem List.splitOnP_spec.flatten_zipWith {α : Type u} {xs ys : List (List α)} {a : α} (hxs : xs ≠ []) (hys : ys ≠ []) : (zipWith (fun (x x_1 : List α) => x ++ x_1) (modifyHead (cons a) xs) ys).flatten = a :: (zipWith (fun (x x_1 : List α) => x ++ x_1) xs ys).flatten

theorem List.splitOnP_eq_single {α : Type u} (p : α → Bool) (xs : List α) (h : ∀ (x : α), x ∈ xs → ¬p x = true) : splitOnP p xs = [xs]

If no element satisfies p in the list xs, then xs.splitOnP p = [xs]

theorem List.splitOnP_first {α : Type u} (p : α → Bool) (xs : List α) (h : ∀ (x : α), x ∈ xs → ¬p x = true) (sep : α) (hsep : p sep = true) (as : List α) : splitOnP p (xs ++ sep :: as) = xs :: splitOnP p as

When a list of the form [...xs, sep, ...as] is split on p, the first element is xs, assuming no element in xs satisfies p but sep does satisfy p

theorem List.intercalate_splitOn {α : Type u} (xs : List α) (x : α) [DecidableEq α] : [x].intercalate (splitOn x xs) = xs

intercalate [x] is the left inverse of splitOn x

theorem List.splitOn_intercalate {α : Type u} (ls : List (List α)) [DecidableEq α] (x : α) (hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l) (hls : ls ≠ []) : splitOn x ([x].intercalate ls) = ls

splitOn x is the left inverse of intercalate [x], on the domain consisting of each nonempty list of lists ls whose elements do not contain x

modifyLast

theorem List.modifyLast.go_append_one {α : Type u} (f : α → α) (a : α) (tl : List α) (r : Array α) : go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])

theorem List.modifyLast_append_one {α : Type u} (f : α → α) (a : α) (l : List α) : modifyLast f (l ++ [a]) = l ++ [f a]

theorem List.modifyLast_append {α : Type u} (f : α → α) (l₁ l₂ : List α) : l₂ ≠ [] → modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

map for partial functions

theorem List.sizeOf_lt_sizeOf_of_mem {α : Type u} [SizeOf α] {x : α} {l : List α} (hx : x ∈ l) : sizeOf x < sizeOf l

@[deprecated List.attach_map_coe (since := "2024-07-29")]

theorem List.attach_map_coe' {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) : map (fun (i : { i : α // i ∈ l }) => f ↑i) l.attach = map f l

Alias of List.attach_map_coe.

@[deprecated List.attach_map_val (since := "2024-07-29")]

theorem List.attach_map_val' {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) : map (fun (i : { x : α // x ∈ l }) => f ↑i) l.attach = map f l

Alias of List.attach_map_val.

find

@[deprecated List.mem_of_find?_eq_some (since := "2024-05-05")]

theorem List.find?_mem {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {l : List α✝} : find? p l = some a → a ∈ l

Alias of List.mem_of_find?_eq_some.

lookmap

theorem List.lookmap.go_append {α : Type u} (f : α → Option α) (l : List α) (acc : Array α) : go f l acc = acc.toListAppend (lookmap f l)

@[simp]

theorem List.lookmap_nil {α : Type u} (f : α → Option α) : lookmap f [] = []

@[simp]

theorem List.lookmap_cons_none {α : Type u} (f : α → Option α) {a : α} (l : List α) (h : f a = none) : lookmap f (a :: l) = a :: lookmap f l

@[simp]

theorem List.lookmap_cons_some {α : Type u} (f : α → Option α) {a b : α} (l : List α) (h : f a = some b) : lookmap f (a :: l) = b :: l

theorem List.lookmap_some {α : Type u} (l : List α) : lookmap some l = l

theorem List.lookmap_none {α : Type u} (l : List α) : lookmap (fun (x : α) => none) l = l

theorem List.lookmap_congr {α : Type u} {f g : α → Option α} {l : List α} : (∀ (a : α), a ∈ l → f a = g a) → lookmap f l = lookmap g l

theorem List.lookmap_of_forall_not {α : Type u} (f : α → Option α) {l : List α} (H : ∀ (a : α), a ∈ l → f a = none) : lookmap f l = l

theorem List.lookmap_map_eq {α : Type u} {β : Type v} (f : α → Option α) (g : α → β) (h : ∀ (a b : α), b ∈ f a → g a = g b) (l : List α) : map g (lookmap f l) = map g l

theorem List.lookmap_id' {α : Type u} (f : α → Option α) (h : ∀ (a b : α), b ∈ f a → a = b) (l : List α) : lookmap f l = l

theorem List.length_lookmap {α : Type u} (f : α → Option α) (l : List α) : (lookmap f l).length = l.length

filter

theorem List.length_eq_length_filter_add {α : Type u} {l : List α} (f : α → Bool) : l.length = (filter f l).length + (filter (fun (x : α) => !f x) l).length

filterMap

theorem List.filterMap_eq_flatMap_toList {α : Type u} {β : Type v} (f : α → Option β) (l : List α) : filterMap f l = l.flatMap fun (a : α) => (f a).toList

@[deprecated List.filterMap_eq_flatMap_toList (since := "2024-10-16")]

theorem List.filterMap_eq_bind_toList {α : Type u} {β : Type v} (f : α → Option β) (l : List α) : filterMap f l = l.flatMap fun (a : α) => (f a).toList

Alias of List.filterMap_eq_flatMap_toList.

theorem List.filterMap_congr {α : Type u} {β : Type v} {f g : α → Option β} {l : List α} (h : ∀ (x : α), x ∈ l → f x = g x) : filterMap f l = filterMap g l

theorem List.filterMap_eq_map_iff_forall_eq_some {α : Type u} {β : Type v} {f : α → Option β} {g : α → β} {l : List α} : filterMap f l = map g l ↔ ∀ (x : α), x ∈ l → f x = some (g x)

filter

theorem List.filter_singleton {α : Type u} {p : α → Bool} {a : α} : filter p [a] = bif p a then [a] else []

theorem List.filter_eq_foldr {α : Type u} (p : α → Bool) (l : List α) : filter p l = foldr (fun (a : α) (out : List α) => bif p a then a :: out else out) [] l

@[simp]

theorem List.filter_subset' {α : Type u} {p : α → Bool} (l : List α) : filter p l ⊆ l

theorem List.of_mem_filter {α : Type u} {p : α → Bool} {a : α} {l : List α} (h : a ∈ filter p l) : p a = true

theorem List.mem_of_mem_filter {α : Type u} {p : α → Bool} {a : α} {l : List α} (h : a ∈ filter p l) : a ∈ l

theorem List.mem_filter_of_mem {α : Type u} {p : α → Bool} {a : α} {l : List α} (h₁ : a ∈ l) (h₂ : p a = true) : a ∈ filter p l

theorem List.monotone_filter_left {α : Type u} (p : α → Bool) ⦃l l' : List α⦄ (h : l ⊆ l') : filter p l ⊆ filter p l'

theorem List.monotone_filter_right {α : Type u} (l : List α) ⦃p q : α → Bool⦄ (h : ∀ (a : α), p a = true → q a = true) : (filter p l).Sublist (filter q l)

theorem List.map_filter' {α : Type u} {β : Type v} (p : α → Bool) {f : α → β} (hf : Function.Injective f) (l : List α) [DecidablePred fun (b : β) => ∃ (a : α), p a = true ∧ f a = b] : map f (filter p l) = filter (fun (b : β) => decide (∃ (a : α), p a = true ∧ f a = b)) (map f l)

theorem List.filter_attach' {α : Type u} (l : List α) (p : { a : α // a ∈ l } → Bool) [DecidableEq α] : filter p l.attach = map (Subtype.map id ⋯) (filter (fun (x : α) => decide (∃ (h : x ∈ l), p ⟨x, h⟩ = true)) l).attach

theorem List.filter_attach {α : Type u} (l : List α) (p : α → Bool) : filter (fun (x : { x : α // x ∈ l }) => p ↑x) l.attach = map (Subtype.map id ⋯) (filter p l).attach

theorem List.filter_comm {α : Type u} (p q : α → Bool) (l : List α) : filter p (filter q l) = filter q (filter p l)

@[simp]

theorem List.filter_true {α : Type u} (l : List α) : filter (fun (x : α) => true) l = l

@[simp]

theorem List.filter_false {α : Type u} (l : List α) : filter (fun (x : α) => false) l = []

theorem List.span.loop_eq_take_drop {α : Type u} (p : α → Bool) (l₁ l₂ : List α) : loop p l₁ l₂ = (l₂.reverse ++ takeWhile p l₁, dropWhile p l₁)

@[simp]

theorem List.span_eq_take_drop {α : Type u} (p : α → Bool) (l : List α) : span p l = (takeWhile p l, dropWhile p l)

theorem List.dropWhile_get_zero_not {α : Type u} (p : α → Bool) (l : List α) (hl : 0 < (dropWhile p l).length) : ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

@[deprecated List.getElem_cons (since := "2024-08-19")]

theorem List.nthLe_cons {α : Type u_1} {i : ℕ} {a : α} {l : List α} (w : i < (a :: l).length) : (a :: l)[i] = if h : i = 0 then a else l[i - 1]

Alias of List.getElem_cons.

@[deprecated List.dropWhile_get_zero_not (since := "2024-08-19")]

theorem List.dropWhile_nthLe_zero_not {α : Type u} (p : α → Bool) (l : List α) (hl : 0 < (dropWhile p l).length) : ¬p ((dropWhile p l).get ⟨0, hl⟩) = true

Alias of List.dropWhile_get_zero_not.

@[simp]

theorem List.dropWhile_eq_nil_iff {α : Type u} {p : α → Bool} {l : List α} : dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.takeWhile_eq_self_iff {α : Type u} {p : α → Bool} {l : List α} : takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.takeWhile_eq_nil_iff {α : Type u} {p : α → Bool} {l : List α} : takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.get ⟨0, hl⟩) = true

theorem List.mem_takeWhile_imp {α : Type u} {p : α → Bool} {l : List α} {x : α} (hx : x ∈ takeWhile p l) : p x = true

theorem List.takeWhile_takeWhile {α : Type u} (p q : α → Bool) (l : List α) : takeWhile p (takeWhile q l) = takeWhile (fun (a : α) => decide (p a = true ∧ q a = true)) l

theorem List.takeWhile_idem {α : Type u} {p : α → Bool} {l : List α} : takeWhile p (takeWhile p l) = takeWhile p l

theorem List.find?_eq_head?_dropWhile_not {α : Type u} (p : α → Bool) (l : List α) : find? p l = (dropWhile (fun (x : α) => !p x) l).head?

theorem List.find?_not_eq_head?_dropWhile {α : Type u} (p : α → Bool) (l : List α) : find? (fun (x : α) => !p x) l = (dropWhile p l).head?

theorem List.find?_eq_head_dropWhile_not {α : Type u} {p : α → Bool} {l : List α} (h : ∃ (x : α), x ∈ l ∧ p x = true) : find? p l = some ((dropWhile (fun (x : α) => !p x) l).head ⋯)

theorem List.find?_not_eq_head_dropWhile {α : Type u} {p : α → Bool} {l : List α} (h : ∃ (x : α), x ∈ l ∧ ¬p x = true) : find? (fun (x : α) => !p x) l = some ((dropWhile p l).head ⋯)

erasep

@[simp]

theorem List.length_eraseP_add_one {α : Type u} {p : α → Bool} {l : List α} {a : α} (al : a ∈ l) (pa : p a = true) : (eraseP p l).length + 1 = l.length

erase

@[simp]

theorem List.length_erase_add_one {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : (l.erase a).length + 1 = l.length

theorem List.map_erase {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {a : α} (l : List α) : map f (l.erase a) = (map f l).erase (f a)

theorem List.map_foldl_erase {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {l₁ l₂ : List α} : map f (foldl List.erase l₁ l₂) = foldl (fun (l : List β) (a : α) => l.erase (f a)) (map f l₁) l₂

theorem List.erase_getElem {ι : Type u_1} [DecidableEq ι] {l : List ι} {i : ℕ} (hi : i < l.length) : (l.erase l[i]).Perm (l.eraseIdx i)

@[deprecated List.erase_getElem (since := "2024-08-03")]

theorem List.erase_get {ι : Type u_1} [DecidableEq ι] {l : List ι} (i : Fin l.length) : (l.erase (l.get i)).Perm (l.eraseIdx ↑i)

theorem List.length_eraseIdx_add_one {ι : Type u_1} {l : List ι} {i : ℕ} (h : i < l.length) : (l.eraseIdx i).length + 1 = l.length

diff

@[simp]

theorem List.map_diff {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {l₁ l₂ : List α} : map f (l₁.diff l₂) = (map f l₁).diff (map f l₂)

theorem List.erase_diff_erase_sublist_of_sublist {α : Type u} [DecidableEq α] {a : α} {l₁ l₂ : List α} : l₁.Sublist l₂ → ((l₂.erase a).diff (l₁.erase a)).Sublist (l₂.diff l₁)

theorem List.choose_spec {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) : choose p l hp ∈ l ∧ p (choose p l hp)

theorem List.choose_mem {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) : choose p l hp ∈ l

theorem List.choose_property {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) : p (choose p l hp)

Forall

@[simp]

theorem List.forall_cons {α : Type u} (p : α → Prop) (x : α) (l : List α) : Forall p (x :: l) ↔ p x ∧ Forall p l

theorem List.forall_iff_forall_mem {α : Type u} {p : α → Prop} {l : List α} : Forall p l ↔ ∀ (x : α), x ∈ l → p x

theorem List.Forall.imp {α : Type u} {p q : α → Prop} (h : ∀ (x : α), p x → q x) {l : List α} : Forall p l → Forall q l

@[simp]

theorem List.forall_map_iff {α : Type u} {β : Type v} {l : List α} {p : β → Prop} (f : α → β) : Forall p (map f l) ↔ Forall (p ∘ f) l

instance List.instDecidablePredForall {α : Type u} (p : α → Prop) [DecidablePred p] : DecidablePred (Forall p)

Equations

• List.instDecidablePredForall p x✝ = decidable_of_iff' (∀ (x : α), x ∈ x✝ → p x) ⋯

Miscellaneous lemmas

theorem List.get_attach {α : Type u} (L : List α) (i : Fin L.attach.length) : ↑(L.attach.get i) = L.get ⟨↑i, ⋯⟩

theorem List.dropSlice_eq {α : Type u} (xs : List α) (n m : ℕ) : dropSlice n m xs = take n xs ++ drop (n + m) xs

@[simp]

theorem List.length_dropSlice {α : Type u} (i j : ℕ) (xs : List α) : (dropSlice i j xs).length = xs.length - j ⊓ (xs.length - i)

theorem List.length_dropSlice_lt {α : Type u} (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) : (dropSlice i j xs).length < xs.length

@[deprecated "No deprecation message was provided." (since := "2024-07-25")]

theorem List.sizeOf_dropSlice_lt {α : Type u} [SizeOf α] (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) : sizeOf (dropSlice i j xs) < sizeOf xs

theorem List.disjoint_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s t : List α} (hs : ∀ (a : α), a ∈ s → p a) (ht : ∀ (a : α), a ∈ t → p a) (hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a') (h : s.Disjoint t) : (pmap f s hs).Disjoint (pmap f t ht)

The images of disjoint lists under a partially defined map are disjoint

theorem List.disjoint_map {α : Type u} {β : Type v} {f : α → β} {s t : List α} (hf : Function.Injective f) (h : s.Disjoint t) : (map f s).Disjoint (map f t)

The images of disjoint lists under an injective map are disjoint

theorem List.Disjoint.map {α : Type u} {β : Type v} {f : α → β} {s t : List α} (hf : Function.Injective f) (h : s.Disjoint t) : (List.map f s).Disjoint (List.map f t)

Alias of List.disjoint_map.

---

The images of disjoint lists under an injective map are disjoint

theorem List.Disjoint.of_map {α : Type u} {β : Type v} {f : α → β} {s t : List α} (h : (List.map f s).Disjoint (List.map f t)) : s.Disjoint t

theorem List.Disjoint.map_iff {α : Type u} {β : Type v} {f : α → β} {s t : List α} (hf : Function.Injective f) : (List.map f s).Disjoint (List.map f t) ↔ s.Disjoint t

theorem List.Perm.disjoint_left {α : Type u} {l₁ l₂ l : List α} (p : l₁.Perm l₂) : l₁.Disjoint l ↔ l₂.Disjoint l

theorem List.Perm.disjoint_right {α : Type u} {l₁ l₂ l : List α} (p : l₁.Perm l₂) : l.Disjoint l₁ ↔ l.Disjoint l₂

@[simp]

theorem List.disjoint_reverse_left {α : Type u} {l₁ l₂ : List α} : l₁.reverse.Disjoint l₂ ↔ l₁.Disjoint l₂

@[simp]

theorem List.disjoint_reverse_right {α : Type u} {l₁ l₂ : List α} : l₁.Disjoint l₂.reverse ↔ l₁.Disjoint l₂

theorem List.lookup_graph {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] (f : α → β) {a : α} {as : List α} (h : a ∈ as) : lookup a (map (fun (x : α) => (x, f x)) as) = some (f a)