Theorems about List operations.

For each List operation, we would like theorems describing the following, when relevant:

• if it is a "convenience" function, a @[simp] lemma reducing it to more basic operations (e.g. List.partition_eq_filter_filter), and otherwise:
• any special cases of equational lemmas that require additional hypotheses
• lemmas for special cases of the arguments (e.g. List.map_id)
• the length of the result (f L).length
• the i-th element, described via (f L)[i] and/or (f L)[i]? (these should typically be @[simp])
• consequences for f L of the fact x ∈ L or x ∉ L
• conditions characterizing x ∈ f L (often but not always @[simp])
• injectivity statements, or congruence statements of the form p L M → f L = f M.
• conditions characterizing the result, i.e. of the form f L = M ↔ p M for some predicate p, along with special cases of M (e.g. List.append_eq_nil : L ++ M = [] ↔ L = [] ∧ M = [])
• negative characterizations are also useful, e.g. List.cons_ne_nil
• interactions with all previously described List operations where possible (some of these should be @[simp], particularly if the result can be described by a single operation)
• characterizing (∀ (i) (_ : i ∈ f L), P i), for some predicate P

Of course for any individual operation, not all of these will be relevant or helpful, so some judgement is required.

General principles for simp normal forms for List operations:

• Conversion operations (e.g. toArray, or length) should be moved inwards aggressively, to make the conversion effective.
• Similarly, operations which work on elements should be moved inwards in preference to "structural" operations on the list, e.g. we prefer to simplify List.map f (L ++ M) ~> (List.map f L) ++ (List.map f M), List.map f L.reverse ~> (List.map f L).reverse, and List.map f (L.take n) ~> (List.map f L).take n.
• Arithmetic operations are "light", so e.g. we prefer to simplify drop i (drop j L) to drop (i + j) L, rather than the other way round.
• Function compositions are "light", so we prefer to simplify (L.map f).map g to L.map (g ∘ f).
• We try to avoid non-linear left hand sides (i.e. with subexpressions appearing multiple times), but this is only a weak preference.
• Generally, we prefer that the right hand side does not introduce duplication, however generally duplication of higher order arguments (functions, predicates, etc) is allowed, as we expect to be able to compute these once they reach ground terms.

See also

• Init.Data.List.Attach for definitions and lemmas about List.attach and List.pmap.
• Init.Data.List.Count for lemmas about List.countP and List.count.
• Init.Data.List.Erase for lemmas about List.eraseP and List.erase.
• Init.Data.List.Find for lemmas about List.find?, List.findSome?, List.findIdx, List.findIdx?, and List.indexOf
• Init.Data.List.MinMax for lemmas about List.min?, List.min, List.max? and List.max.
• Init.Data.List.Pairwise for lemmas about List.Pairwise and List.Nodup.
• Init.Data.List.Sublist for lemmas about List.Subset, List.Sublist, List.IsPrefix, List.IsSuffix, and List.IsInfix.
• Init.Data.List.TakeDrop for additional lemmas about List.take and List.drop.
• Init.Data.List.Zip for lemmas about List.zip, List.zipWith, List.zipWithAll, and List.unzip.

Further results, which first require developing further automation around Nat, appear in

• Init.Data.List.Nat.Basic: miscellaneous lemmas
• Init.Data.List.Nat.Range: List.range, List.range' and List.enum
• Init.Data.List.Nat.TakeDrop: List.take and List.drop

Also

• Init.Data.List.Monadic for additional lemmas about List.mapM and List.forM.

Preliminaries

nil

@[simp]

theorem List.nil_eq {α : Type u_1} {xs : List α} : [] = xs ↔ xs = []

length

theorem List.eq_nil_of_length_eq_zero {α✝ : Type u_1} {l : List α✝} : l.length = 0 → l = []

theorem List.ne_nil_of_length_eq_add_one {α✝ : Type u_1} {l : List α✝} {n : Nat} : l.length = n + 1 → l ≠ []

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

@[simp]

theorem List.length_eq_zero_iff {α✝ : Type u_1} {l : List α✝} : l.length = 0 ↔ l = []

theorem List.eq_nil_iff_length_eq_zero {α✝ : Type u_1} {l : List α✝} : l = [] ↔ l.length = 0

theorem List.length_pos_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → 0 < l.length

theorem List.exists_mem_of_length_pos {α : Type u_1} {l : List α} : 0 < l.length → ∃ (a : α), a ∈ l

theorem List.length_pos_iff_exists_mem {α : Type u_1} {l : List α} : 0 < l.length ↔ ∃ (a : α), a ∈ l

theorem List.exists_mem_of_length_eq_add_one {α : Type u_1} {n : Nat} {l : List α} : l.length = n + 1 → ∃ (a : α), a ∈ l

theorem List.exists_cons_of_length_pos {α : Type u_1} {l : List α} : 0 < l.length → ∃ (h : α), ∃ (t : List α), l = h :: t

theorem List.length_pos_iff_exists_cons {α : Type u_1} {l : List α} : 0 < l.length ↔ ∃ (h : α), ∃ (t : List α), l = h :: t

theorem List.exists_cons_of_length_eq_add_one {α : Type u_1} {n : Nat} {l : List α} : l.length = n + 1 → ∃ (h : α), ∃ (t : List α), l = h :: t

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

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

theorem List.length_eq_one_iff {α : Type u_1} {l : List α} : l.length = 1 ↔ ∃ (a : α), l = [a]

cons

theorem List.cons_ne_nil {α : Type u_1} (a : α) (l : List α) : a :: l ≠ []

@[simp]

theorem List.cons_ne_self {α : Type u_1} (a : α) (l : List α) : a :: l ≠ l

@[simp]

theorem List.ne_cons_self {α : Type u_1} {a : α} {l : List α} : l ≠ a :: l

theorem List.head_eq_of_cons_eq {α✝ : Type u_1} {h₁ : α✝} {t₁ : List α✝} {h₂ : α✝} {t₂ : List α✝} (H : h₁ :: t₁ = h₂ :: t₂) : h₁ = h₂

theorem List.tail_eq_of_cons_eq {α✝ : Type u_1} {h₁ : α✝} {t₁ : List α✝} {h₂ : α✝} {t₂ : List α✝} (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂

theorem List.cons_inj_right {α : Type u_1} (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l'

theorem List.cons_eq_cons {α : Type u_1} {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l'

theorem List.exists_cons_of_ne_nil {α : Type u_1} {l : List α} : l ≠ [] → ∃ (b : α), ∃ (l' : List α), l = b :: l'

theorem List.ne_nil_iff_exists_cons {α : Type u_1} {l : List α} : l ≠ [] ↔ ∃ (b : α), ∃ (l' : List α), l = b :: l'

theorem List.singleton_inj {α : Type u_1} {a b : α} : [a] = [b] ↔ a = b

@[simp]

theorem List.concat_ne_nil {α : Type u_1} (a : α) (l : List α) : l ++ [a] ≠ []

L[i] and L[i]?

get and get?.

We simplify l.get i to l[i.1]'i.2 and l.get? i to l[i]?.

@[simp]

theorem List.get_eq_getElem {α : Type u_1} {l : List α} {i : Fin l.length} : l.get i = l[↑i]

getElem!

We simplify l[i]! to (l[i]?).getD default.

@[simp]

theorem List.getElem!_eq_getElem?_getD {α : Type u_1} [Inhabited α] {l : List α} {i : Nat} : l[i]! = l[i]?.getD default

getElem? and getElem

@[simp]

theorem List.getElem?_nil {α : Type u_1} {i : Nat} : [][i]? = none

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

theorem List.getElem?_cons_zero {α : Type u_1} {a : α} {l : List α} : (a :: l)[0]? = some a

@[simp]

theorem List.getElem?_cons_succ {α : Type u_1} {a : α} {i : Nat} {l : List α} : (a :: l)[i + 1]? = l[i]?

theorem List.getElem?_cons {α✝ : Type u_1} {a : α✝} {l : List α✝} {i : Nat} : (a :: l)[i]? = if i = 0 then some a else l[i - 1]?

theorem List.getElem?_eq_some_iff {α : Type u_1} {i : Nat} {a : α} {l : List α} : l[i]? = some a ↔ ∃ (h : i < l.length), l[i] = a

theorem List.getElem_of_getElem? {α : Type u_1} {i : Nat} {a : α} {l : List α} : l[i]? = some a → ∃ (h : i < l.length), l[i] = a

theorem List.some_eq_getElem?_iff {α : Type u_1} {a : α} {i : Nat} {l : List α} : some a = l[i]? ↔ ∃ (h : i < l.length), l[i] = a

theorem List.some_getElem_eq_getElem?_iff {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.length) : some xs[i] = xs[i]? ↔ True

theorem List.getElem?_eq_some_getElem_iff {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.length) : xs[i]? = some xs[i] ↔ True

theorem List.getElem_eq_iff {α : Type u_1} {x : α} {l : List α} {i : Nat} (h : i < l.length) : l[i] = x ↔ l[i]? = some x

theorem List.getElem_eq_getElem?_get {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) : l[i] = l[i]?.get ⋯

theorem List.getElem_eq_getD {α : Type u_1} {l : List α} {i : Nat} {h : i < l.length} (fallback : α) : l[i] = l.getD i fallback

theorem List.getD_getElem? {α : Type u_1} {l : List α} {i : Nat} {d : α} : l[i]?.getD d = if p : i < l.length then l[i] else d

@[simp]

theorem List.getElem_singleton {α : Type u_1} {a : α} {i : Nat} (h : i < 1) : [a][i] = a

theorem List.getElem?_singleton {α : Type u_1} {a : α} {i : Nat} : [a][i]? = if i = 0 then some a else none

theorem List.getElem_of_eq {α : Type u_1} {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) : l[i] = l'[i]

If one has l[i] in an expression and h : l = l', rw [h] will give a "motive it not type correct" error, as it cannot rewrite the implicit i < l.length to i < l'.length directly. The theorem getElem_of_eq can be used to make such a rewrite, with rw [getElem_of_eq h].

theorem List.getElem_zero {α : Type u_1} {l : List α} (h : 0 < l.length) : l[0] = l.head ⋯

theorem List.ext_getElem? {α : Type u_1} {l₁ l₂ : List α} (h : ∀ (i : Nat), l₁[i]? = l₂[i]?) : l₁ = l₂

theorem List.ext_getElem?_iff {α : Type u_1} {l₁ l₂ : List α} : l₁ = l₂ ↔ ∀ (i : Nat), l₁[i]? = l₂[i]?

theorem List.ext_getElem {α : Type u_1} {l₁ l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]) : l₁ = l₂

theorem List.ext_getElem_iff {α : Type u_1} {l₁ l₂ : List α} : l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (i : Nat) (h₁ : i < l₁.length) (h₂ : i < l₂.length), l₁[i] = l₂[i]

@[simp]

theorem List.getElem_concat_length {α : Type u_1} {l : List α} {a : α} {i : Nat} (h : i = l.length) (w : i < (l ++ [a]).length) : (l ++ [a])[i] = a

theorem List.getElem?_concat_length {α : Type u_1} {l : List α} {a : α} : (l ++ [a])[l.length]? = some a

theorem List.eq_getElem_of_length_eq_one {α : Type u_1} (l : List α) (hl : l.length = 1) : l = [l[0]]

theorem List.eq_getElem_of_length_eq_two {α : Type u_1} (l : List α) (hl : l.length = 2) : l = [l[0], l[1]]

theorem List.eq_getElem_of_length_eq_three {α : Type u_1} (l : List α) (hl : l.length = 3) : l = [l[0], l[1], l[2]]

theorem List.eq_getElem_of_length_eq_four {α : Type u_1} (l : List α) (hl : l.length = 4) : l = [l[0], l[1], l[2], l[3]]

getD

We simplify away getD, replacing getD l n a with (l[n]?).getD a. Because of this, there is only minimal API for getD.

@[simp]

theorem List.getD_eq_getElem?_getD {α : Type u_1} {l : List α} {i : Nat} {a : α} : l.getD i a = l[i]?.getD a

theorem List.getD_cons_zero {α✝ : Type u_1} {x : α✝} {xs : List α✝} {d : α✝} : (x :: xs).getD 0 d = x

theorem List.getD_cons_succ {α✝ : Type u_1} {x : α✝} {xs : List α✝} {n : Nat} {d : α✝} : (x :: xs).getD (n + 1) d = xs.getD n d

mem

@[simp]

theorem List.not_mem_nil {α : Type u_1} {a : α} : ¬a ∈ []

@[simp]

theorem List.mem_cons {α✝ : Type u_1} {b : α✝} {l : List α✝} {a : α✝} : a ∈ b :: l ↔ a = b ∨ a ∈ l

theorem List.eq_or_mem_of_mem_cons {α : Type u_1} {a b : α} {l : List α} : a ∈ b :: l → a = b ∨ a ∈ l

theorem List.mem_cons_self {α : Type u_1} {a : α} {l : List α} : a ∈ a :: l

theorem List.mem_concat_self {α : Type u_1} {xs : List α} {a : α} : a ∈ xs ++ [a]

theorem List.mem_append_cons_self {α✝ : Type u_1} {xs : List α✝} {a : α✝} {ys : List α✝} : a ∈ xs ++ a :: ys

theorem List.eq_append_cons_of_mem {α : Type u_1} {a : α} {xs : List α} (h : a ∈ xs) : ∃ (as : List α), ∃ (bs : List α), xs = as ++ a :: bs ∧ ¬a ∈ as

theorem List.mem_cons_of_mem {α : Type u_1} (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l

theorem List.exists_mem_of_ne_nil {α : Type u_1} (l : List α) (h : l ≠ []) : ∃ (x : α), x ∈ l

theorem List.eq_nil_iff_forall_not_mem {α : Type u_1} {l : List α} : l = [] ↔ ∀ (a : α), ¬a ∈ l

@[simp]

theorem List.mem_dite_nil_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : ¬p → List α} : (x ∈ if h : p then [] else l h) ↔ ∃ (h : ¬p), x ∈ l h

@[simp]

theorem List.mem_dite_nil_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : p → List α} : (x ∈ if h : p then l h else []) ↔ ∃ (h : p), x ∈ l h

@[simp]

theorem List.mem_ite_nil_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : List α} : (x ∈ if p then [] else l) ↔ ¬p ∧ x ∈ l

@[simp]

theorem List.mem_ite_nil_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {l : List α} : (x ∈ if p then l else []) ↔ p ∧ x ∈ l

theorem List.eq_of_mem_singleton {α✝ : Type u_1} {b a : α✝} : a ∈ [b] → a = b

theorem List.mem_singleton {α : Type u_1} {a b : α} : a ∈ [b] ↔ a = b

theorem List.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} : (∀ (x : α), x ∈ a :: l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l → p x

theorem List.forall_mem_ne {α : Type u_1} {a : α} {l : List α} : (∀ (a' : α), a' ∈ l → ¬a = a') ↔ ¬a ∈ l

theorem List.forall_mem_ne' {α : Type u_1} {a : α} {l : List α} : (∀ (a' : α), a' ∈ l → ¬a' = a) ↔ ¬a ∈ l

theorem List.exists_mem_nil {α : Type u_1} (p : α → Prop) : ¬∃ (x : α), ∃ (x_1 : x ∈ []), p x

theorem List.forall_mem_nil {α : Type u_1} (p : α → Prop) (x : α) : x ∈ [] → p x

theorem List.exists_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} : (∃ (x : α), ∃ (x_1 : x ∈ a :: l), p x) ↔ p a ∨ ∃ (x : α), ∃ (x_1 : x ∈ l), p x

theorem List.forall_mem_singleton {α : Type u_1} {p : α → Prop} {a : α} : (∀ (x : α), x ∈ [a] → p x) ↔ p a

theorem List.mem_nil_iff {α : Type u_1} (a : α) : a ∈ [] ↔ False

theorem List.mem_singleton_self {α : Type u_1} (a : α) : a ∈ [a]

theorem List.mem_of_mem_cons_of_mem {α : Type u_1} {a b : α} {l : List α} : a ∈ b :: l → b ∈ l → a ∈ l

theorem List.eq_or_ne_mem_of_mem {α : Type u_1} {a b : α} {l : List α} (h' : a ∈ b :: l) : a = b ∨ a ≠ b ∧ a ∈ l

theorem List.ne_nil_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : l ≠ []

theorem List.mem_of_ne_of_mem {α : Type u_1} {a y : α} {l : List α} (h₁ : a ≠ y) (h₂ : a ∈ y :: l) : a ∈ l

theorem List.ne_of_not_mem_cons {α : Type u_1} {a b : α} {l : List α} : ¬a ∈ b :: l → a ≠ b

theorem List.not_mem_of_not_mem_cons {α : Type u_1} {a b : α} {l : List α} : ¬a ∈ b :: l → ¬a ∈ l

theorem List.not_mem_cons_of_ne_of_not_mem {α : Type u_1} {a y : α} {l : List α} : a ≠ y → ¬a ∈ l → ¬a ∈ y :: l

theorem List.ne_and_not_mem_of_not_mem_cons {α : Type u_1} {a y : α} {l : List α} : ¬a ∈ y :: l → a ≠ y ∧ ¬a ∈ l

theorem List.getElem_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → ∃ (i : Nat), ∃ (h : i < l.length), l[i] = a

theorem List.getElem?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ (i : Nat), l[i]? = some a

theorem List.mem_of_getElem {α : Type u_1} {l : List α} {i : Nat} {h : i < l.length} {a : α} (e : l[i] = a) : a ∈ l

theorem List.mem_of_getElem? {α : Type u_1} {l : List α} {i : Nat} {a : α} (e : l[i]? = some a) : a ∈ l

theorem List.mem_iff_getElem {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (i : Nat), ∃ (h : i < l.length), l[i] = a

theorem List.mem_iff_getElem? {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (i : Nat), l[i]? = some a

theorem List.exists_mem_iff_exists_getElem {α : Type u_1} {P : α → Prop} {l : List α} : (∃ (x : α), x ∈ l ∧ P x) ↔ ∃ (i : Nat), ∃ (hi : i < l.length), P l[i]

theorem List.forall_mem_iff_forall_getElem {α : Type u_1} {P : α → Prop} {l : List α} : (∀ (x : α), x ∈ l → P x) ↔ ∀ (i : Nat) (hi : i < l.length), P l[i]

@[deprecated List.forall_mem_iff_forall_getElem (since := "2026-01-29")]

theorem List.forall_getElem {α : Type u_1} {l : List α} {p : α → Prop} : (∀ (i : Nat) (h : i < l.length), p l[i]) ↔ ∀ (a : α), a ∈ l → p a

@[simp]

theorem List.elem_eq_contains {α : Type u_1} [BEq α] {a : α} {l : List α} : elem a l = l.contains a

@[simp]

theorem List.decide_mem_cons {α : Type u_1} {a y : α} [BEq α] [LawfulBEq α] {l : List α} : decide (y ∈ a :: l) = (y == a || decide (y ∈ l))

theorem List.elem_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : List α} : elem a as = true ↔ a ∈ as

theorem List.contains_iff_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : List α} : as.contains a = true ↔ a ∈ as

@[deprecated List.contains_iff_mem (since := "2025-10-26")]

theorem List.contains_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : List α} : as.contains a = true ↔ a ∈ as

theorem List.elem_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (as : List α) : elem a as = decide (a ∈ as)

@[simp]

theorem List.contains_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (as : List α) : as.contains a = decide (a ∈ as)

@[simp]

theorem List.contains_cons {α : Type u_1} [BEq α] {a b : α} {l : List α} : (a :: l).contains b = (b == a || l.contains b)

isEmpty

@[simp]

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

theorem List.nil_of_isEmpty {α : Type u_1} {l : List α} (h : l.isEmpty = true) : l = []

@[simp]

theorem List.isEmpty_eq_false_iff {α : Type u_1} {l : List α} : l.isEmpty = false ↔ l ≠ []

theorem List.isEmpty_eq_false_iff_exists_mem {α : Type u_1} {xs : List α} : xs.isEmpty = false ↔ ∃ (x : α), x ∈ xs

theorem List.isEmpty_iff_length_eq_zero {α : Type u_1} {l : List α} : l.isEmpty = true ↔ l.length = 0

any / all

theorem List.any_eq {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = decide (∃ (x : α), x ∈ l ∧ p x = true)

theorem List.all_eq {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = decide (∀ (x : α), x ∈ l → p x = true)

theorem List.decide_exists_mem {α : Type u_1} {l : List α} {p : α → Prop} [DecidablePred p] : decide (∃ (x : α), x ∈ l ∧ p x) = l.any fun (b : α) => decide (p b)

theorem List.decide_forall_mem {α : Type u_1} {l : List α} {p : α → Prop} [DecidablePred p] : decide (∀ (x : α), x ∈ l → p x) = l.all fun (b : α) => decide (p b)

@[simp]

theorem List.any_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = true ↔ ∃ (x : α), x ∈ l ∧ p x = true

@[simp]

theorem List.all_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.any_eq_false {α : Type u_1} {p : α → Bool} {l : List α} : l.any p = false ↔ ∀ (x : α), x ∈ l → ¬p x = true

@[simp]

theorem List.all_eq_false {α : Type u_1} {p : α → Bool} {l : List α} : l.all p = false ↔ ∃ (x : α), x ∈ l ∧ ¬p x = true

theorem List.any_beq {α : Type u_1} [BEq α] {l : List α} {a : α} : (l.any fun (x : α) => a == x) = l.contains a

theorem List.any_beq' {α : Type u_1} {a : α} [BEq α] [PartialEquivBEq α] {l : List α} : (l.any fun (x : α) => x == a) = l.contains a

Variant of any_beq with == reversed.

theorem List.all_bne {α : Type u_1} {a : α} [BEq α] {l : List α} : (l.all fun (x : α) => a != x) = !l.contains a

theorem List.all_bne' {α : Type u_1} {a : α} [BEq α] [PartialEquivBEq α] {l : List α} : (l.all fun (x : α) => x != a) = !l.contains a

Variant of all_bne with != reversed.

set

@[simp]

theorem List.set_nil {α : Type u_1} {i : Nat} {a : α} : [].set i a = []

@[simp]

theorem List.set_cons_zero {α : Type u_1} {x : α} {xs : List α} {a : α} : (x :: xs).set 0 a = a :: xs

@[simp]

theorem List.set_cons_succ {α : Type u_1} {x : α} {xs : List α} {i : Nat} {a : α} : (x :: xs).set (i + 1) a = x :: xs.set i a

@[simp]

theorem List.getElem_set_self {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : (l.set i a)[i] = a

@[simp]

theorem List.getElem?_set_self {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < l.length) : (l.set i a)[i]? = some a

theorem List.getElem?_set_self' {α : Type u_1} {l : List α} {i : Nat} {a : α} : (l.set i a)[i]? = Function.const α a <$> l[i]?

This differs from getElem?_set_self by monadically mapping Function.const _ a over the Option returned by l[i]?.

@[simp]

theorem List.getElem_set_ne {α : Type u_1} {l : List α} {i j : Nat} (h : i ≠ j) {a : α} (hj : j < (l.set i a).length) : (l.set i a)[j] = l[j]

@[simp]

theorem List.getElem?_set_ne {α : Type u_1} {l : List α} {i j : Nat} (h : i ≠ j) {a : α} : (l.set i a)[j]? = l[j]?

theorem List.getElem_set {α : Type u_1} {l : List α} {i j : Nat} {a : α} (h : j < (l.set i a).length) : (l.set i a)[j] = if i = j then a else l[j]

theorem List.getElem?_set {α : Type u_1} {l : List α} {i j : Nat} {a : α} : (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]?

theorem List.getElem?_set' {α : Type u_1} {l : List α} {i j : Nat} {a : α} : (l.set i a)[j]? = if i = j then Function.const α a <$> l[j]? else l[j]?

This differs from getElem?_set by monadically mapping Function.const _ a over the Option returned by l[j]?

@[simp]

theorem List.set_getElem_self {α : Type u_1} {as : List α} {i : Nat} (h : i < as.length) : as.set i as[i] = as

theorem List.set_eq_of_length_le {α : Type u_1} {l : List α} {i : Nat} (h : l.length ≤ i) {a : α} : l.set i a = l

@[simp]

theorem List.set_eq_nil_iff {α : Type u_1} {l : List α} (i : Nat) (a : α) : l.set i a = [] ↔ l = []

theorem List.set_comm {α : Type u_1} (a b : α) {i j : Nat} {l : List α} : i ≠ j → (l.set i a).set j b = (l.set j b).set i a

@[simp]

theorem List.set_set {α : Type u_1} (a : α) {b : α} {l : List α} {i : Nat} : (l.set i a).set i b = l.set i b

theorem List.mem_set {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) (a : α) : a ∈ l.set i a

theorem List.mem_or_eq_of_mem_set {α : Type u_1} {l : List α} {i : Nat} {a b : α} : a ∈ l.set i b → a ∈ l ∨ a = b

BEq

@[simp]

theorem List.beq_nil_eq {α : Type u_1} [BEq α] {l : List α} : (l == []) = l.isEmpty

@[simp]

theorem List.nil_beq_eq {α : 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₂)

@[simp]

theorem List.concat_beq_concat {α : Type u_1} [BEq α] {a b : α} {l₁ l₂ : List α} : (l₁ ++ [a] == l₂ ++ [b]) = (l₁ == l₂ && a == b)

theorem List.length_eq_of_beq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : (l₁ == l₂) = true) : l₁.length = l₂.length

@[simp]

theorem List.replicate_beq_replicate {α : Type u_1} [BEq α] {a b : α} {n : Nat} : (replicate n a == replicate n b) = (n == 0 || a == b)

@[simp]

theorem List.reflBEq_iff {α : Type u_1} [BEq α] : ReflBEq (List α) ↔ ReflBEq α

@[simp]

theorem List.lawfulBEq_iff {α : Type u_1} [BEq α] : LawfulBEq (List α) ↔ LawfulBEq α

isEqv

@[simp]

theorem List.isEqv_eq {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : ((l₁.isEqv l₂ fun (x1 x2 : α) => x1 == x2) = true) = (l₁ = l₂)

getLast

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

theorem List.getElem_length_sub_one_eq_getLast {α : Type u_1} {l : List α} (h : l.length - 1 < l.length) : l[l.length - 1] = l.getLast ⋯

@[simp]

theorem List.getLast_cons_cons {α : Type u_1} {b a : α} {l : List α} : (a :: b :: l).getLast ⋯ = (b :: l).getLast ⋯

theorem List.getLast_cons {α : Type u_1} {a : α} {l : List α} (h : l ≠ []) : (a :: l).getLast ⋯ = l.getLast h

theorem List.getLast_eq_getLastD {α : Type u_1} {a : α} {l : List α} (h : a :: l ≠ []) : (a :: l).getLast h = l.getLastD a

@[simp]

theorem List.getLastD_eq_getLast? {α : Type u_1} {a : α} {l : List α} : l.getLastD a = l.getLast?.getD a

@[simp]

theorem List.getLast_singleton {α : Type u_1} {a : α} (h : [a] ≠ []) : [a].getLast h = a

theorem List.getLast!_cons_eq_getLastD {α : Type u_1} {a : α} {l : List α} [Inhabited α] : (a :: l).getLast! = l.getLastD a

@[simp]

theorem List.getLast_mem {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h ∈ l

theorem List.getLast_mem_getLast? {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h ∈ l.getLast?

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

theorem List.getLastD_mem_cons {α : Type u_1} {l : List α} {a : α} : l.getLastD a ∈ a :: l

theorem List.getElem_cons_length {α : Type u_1} {x : α} {xs : List α} {i : Nat} (h : i = xs.length) : (x :: xs)[i] = (x :: xs).getLast ⋯

getLast?

@[simp]

theorem List.getLast?_singleton {α : Type u_1} {a : α} : [a].getLast? = some a

@[deprecated List.getLast?_eq_some_getLast (since := "2025-10-26")]

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

theorem List.getLast?_eq_getElem? {α : Type u_1} {l : List α} : l.getLast? = l[l.length - 1]?

theorem List.getLast_eq_iff_getLast?_eq_some {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []) : xs.getLast h = a ↔ xs.getLast? = some a

theorem List.getLast?_cons {α : Type u_1} {l : List α} {a : α} : (a :: l).getLast? = some (l.getLast?.getD a)

theorem List.getLast?_cons_of_ne_nil {α : Type u_1} {x : α} {xs : List α} (h : xs ≠ []) : (x :: xs).getLast? = xs.getLast?

@[simp]

theorem List.getLast?_cons_cons {α✝ : Type u_1} {a b : α✝} {l : List α✝} : (a :: b :: l).getLast? = (b :: l).getLast?

theorem List.getLast?_concat {α : Type u_1} {l : List α} {a : α} : (l ++ [a]).getLast? = some a

theorem List.getLastD_concat {α : Type u_1} {a b : α} {l : List α} : (l ++ [b]).getLastD a = b

getLast!

theorem List.getLast!_nil {α : Type u_1} [Inhabited α] : [].getLast! = default

@[simp]

theorem List.getLast!_eq_getLast?_getD {α : Type u_1} [Inhabited α] {l : List α} : l.getLast! = l.getLast?.getD default

theorem List.getLast!_of_getLast? {α : Type u_1} {a : α} [Inhabited α] {l : List α} : l.getLast? = some a → l.getLast! = a

theorem List.getLast!_eq_getElem! {α : Type u_1} [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]!

Head and tail

head

theorem List.head?_singleton {α : Type u_1} {a : α} : [a].head? = some a

theorem List.head!_of_head? {α : Type u_1} {a : α} [Inhabited α] {l : List α} : l.head? = some a → l.head! = a

theorem List.head?_eq_getElem? {α : Type u_1} {l : List α} : l.head? = l[0]?

theorem List.head_singleton {α : Type u_1} {a : α} : [a].head ⋯ = a

theorem List.head_eq_getElem {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h = l[0]

theorem List.getElem_zero_eq_head {α : Type u_1} {l : List α} (h : 0 < l.length) : l[0] = l.head ⋯

theorem List.head!_eq_getElem! {α : Type u_1} [Inhabited α] {l : List α} : l.head! = l[0]!

theorem List.headD_eq_getD {α : Type u_1} {l : List α} {fallback : α} : l.headD fallback = l.getD 0 fallback

theorem List.head_eq_iff_head?_eq_some {α : Type u_1} {a : α} {xs : List α} (h : xs ≠ []) : xs.head h = a ↔ xs.head? = some a

@[simp]

theorem List.head?_eq_none_iff {α✝ : Type u_1} {l : List α✝} : l.head? = none ↔ l = []

theorem List.head?_eq_some_iff {α : Type u_1} {xs : List α} {a : α} : xs.head? = some a ↔ ∃ (ys : List α), xs = a :: ys

@[simp]

theorem List.isSome_head? {α✝ : Type u_1} {l : List α✝} : l.head?.isSome = true ↔ l ≠ []

@[simp]

theorem List.head_mem {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h ∈ l

theorem List.mem_of_head? {α : Type u_1} {l : List α} {a : α} : l.head? = some a → a ∈ l

theorem List.mem_of_mem_head? {α : Type u_1} {l : List α} {a : α} : a ∈ l.head? → a ∈ l

theorem List.head_mem_head? {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h ∈ l.head?

theorem List.head?_eq_some_head {α : Type u_1} {l : List α} (h : l ≠ []) : l.head? = some (l.head h)

@[deprecated List.head?_eq_some_head (since := "2025-10-26")]

theorem List.head?_eq_head {α : Type u_1} {l : List α} (h : l ≠ []) : l.head? = some (l.head h)

theorem List.head?_concat {α : Type u_1} {l : List α} {a : α} : (l ++ [a]).head? = some (l.head?.getD a)

theorem List.head?_concat_concat {α✝ : Type u_1} {l : List α✝} {a b : α✝} : (l ++ [a, b]).head? = (l ++ [a]).head?

theorem List.head_of_head?_eq_some {α : Type u_1} {l : List α} {x : α} (hx : l.head? = some x) : l.head ⋯ = x

theorem List.head_of_mem_head? {α : Type u_1} {l : List α} {x : α} (hx : x ∈ l.head?) : l.head ⋯ = x

headD

@[simp]

theorem List.headD_eq_head?_getD {α : Type u_1} {a : α} {l : List α} : l.headD a = l.head?.getD a

simp unfolds headD in terms of head? and Option.getD.

tailD

@[simp]

theorem List.tailD_eq_tail? {α : Type u_1} {l l' : List α} : l.tailD l' = l.tail?.getD l'

simp unfolds tailD in terms of tail? and Option.getD.

tail

@[simp]

theorem List.length_tail {α : Type u_1} {l : List α} : l.tail.length = l.length - 1

theorem List.tail_eq_tailD {α : Type u_1} {l : List α} : l.tail = l.tailD []

theorem List.tail_eq_tail? {α : Type u_1} {l : List α} : l.tail = l.tail?.getD []

theorem List.mem_of_mem_tail {α : Type u_1} {a : α} {l : List α} (h : a ∈ l.tail) : a ∈ l

theorem List.ne_nil_of_tail_ne_nil {α : Type u_1} {l : List α} : l.tail ≠ [] → l ≠ []

@[simp]

theorem List.getElem_tail {α : Type u_1} {l : List α} {i : Nat} (h : i < l.tail.length) : l.tail[i] = l[i + 1]

@[simp]

theorem List.getElem?_tail {α : Type u_1} {l : List α} {i : Nat} : l.tail[i]? = l[i + 1]?

@[simp]

theorem List.set_tail {α : Type u_1} {l : List α} {i : Nat} {a : α} : l.tail.set i a = (l.set (i + 1) a).tail

theorem List.one_lt_length_of_tail_ne_nil {α : Type u_1} {l : List α} (h : l.tail ≠ []) : 1 < l.length

@[simp]

theorem List.head_tail {α : Type u_1} {l : List α} (h : l.tail ≠ []) : l.tail.head h = l[1]

@[simp]

theorem List.head?_tail {α : Type u_1} {l : List α} : l.tail.head? = l[1]?

@[simp]

theorem List.getLast_tail {α : Type u_1} {l : List α} (h : l.tail ≠ []) : l.tail.getLast h = l.getLast ⋯

theorem List.getLast?_tail {α : Type u_1} {l : List α} : l.tail.getLast? = if l.length = 1 then none else l.getLast?

@[simp]

theorem List.cons_head_tail {α✝ : Type u_1} {l : List α✝} (h : l ≠ []) : l.head h :: l.tail = l

Basic operations

map

@[simp]

theorem List.length_map {α : Type u_1} {β : Type u_2} {as : List α} (f : α → β) : (map f as).length = as.length

@[simp]

theorem List.isEmpty_map {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : (map f l).isEmpty = l.isEmpty

@[simp]

theorem List.getElem?_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : Nat} : (map f l)[i]? = Option.map f l[i]?

@[simp]

theorem List.getElem_map {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {i : Nat} {h : i < (map f l).length} : (map f l)[i] = f l[i]

@[simp]

theorem List.map_id_fun {α : Type u_1} : map id = id

@[simp]

theorem List.map_id_fun' {α : Type u_1} : (map fun (a : α) => a) = id

map_id_fun' differs from map_id_fun by representing the identity function as a lambda, rather than id.

theorem List.map_id {α : Type u_1} (l : List α) : map id l = l

theorem List.map_id' {α : Type u_1} (l : List α) : map (fun (a : α) => a) l = l

map_id' differs from map_id by representing the identity function as a lambda, rather than id.

theorem List.map_id'' {α : Type u_1} {f : α → α} (h : ∀ (x : α), f x = x) (l : List α) : map f l = l

Variant of map_id, with a side condition that the function is pointwise the identity.

theorem List.map_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} : map f [a] = [f a]

@[simp]

theorem List.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α} : b ∈ map f l ↔ ∃ (a : α), a ∈ l ∧ f a = b

theorem List.exists_of_mem_map {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : List α✝} {b : α✝¹} (h : b ∈ map f l) : ∃ (a : α✝), a ∈ l ∧ f a = b

theorem List.mem_map_of_mem {α : Type u_1} {β : Type u_2} {l : List α} {a : α} {f : α → β} (h : a ∈ l) : f a ∈ map f l

theorem List.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {P : β → Prop} : (∀ (i : β), i ∈ map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

@[simp]

theorem List.map_eq_nil_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : map f l = [] ↔ l = []

theorem List.eq_nil_of_map_eq_nil {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (h : map f l = []) : l = []

@[simp]

theorem List.map_inj_left {α : Type u_1} {β : Type u_2} {l : List α} {f g : α → β} : map f l = map g l ↔ ∀ (a : α), a ∈ l → f a = g a

theorem List.map_inj_right {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → β} (w : ∀ (x y : α), f x = f y → x = y) : map f l = map f l' ↔ l = l'

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

theorem List.map_inj {α✝ : Type u_1} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} : map f = map g ↔ f = g

theorem List.map_eq_cons_iff {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : map f l = b :: l₂ ↔ ∃ (a : α), ∃ (l₁ : List α), l = a :: l₁ ∧ f a = b ∧ map f l₁ = l₂

theorem List.map_eq_cons_iff' {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : α → β} {l : List α} : map f l = b :: l₂ ↔ Option.map f l.head? = some b ∧ Option.map (map f) l.tail? = some l₂

@[simp]

theorem List.map_eq_singleton_iff {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {b : β} : map f l = [b] ↔ ∃ (a : α), l = [a] ∧ f a = b

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

theorem List.map_eq_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : List α✝} {l' : List α✝¹} : map f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map f l[i]?

theorem List.map_eq_foldr {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : map f l = foldr (fun (a : α) (bs : List β) => f a :: bs) [] l

@[simp]

theorem List.map_set {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {i : Nat} {a : α} : map f (l.set i a) = (map f l).set i (f a)

@[simp]

theorem List.head_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (w : map f l ≠ []) : (map f l).head w = f (l.head ⋯)

@[simp]

theorem List.head?_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : (map f l).head? = Option.map f l.head?

@[simp]

theorem List.map_tail? {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : Option.map (map f) l.tail? = (map f l).tail?

@[simp]

theorem List.map_tail {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : map f l.tail = (map f l).tail

theorem List.headD_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {a : α} : (map f l).headD (f a) = f (l.headD a)

theorem List.tailD_map {α : Type u_1} {β : Type u_2} {f : α → β} {l l' : List α} : (map f l).tailD (map f l') = map f (l.tailD l')

@[simp]

theorem List.getLast_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} (h : map f l ≠ []) : (map f l).getLast h = f (l.getLast ⋯)

@[simp]

theorem List.getLast?_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : (map f l).getLast? = Option.map f l.getLast?

theorem List.getLastD_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a)

@[simp]

theorem List.map_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} {g : β → γ} {f : α → β} {l : List α} : map g (map f l) = map (g ∘ f) l

filter

@[simp]

theorem List.filter_cons_of_pos {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (pa : p a = true) : filter p (a :: l) = a :: filter p l

@[simp]

theorem List.filter_cons_of_neg {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (pa : ¬p a = true) : filter p (a :: l) = filter p l

theorem List.filter_cons {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} : filter p (x :: xs) = if p x = true then x :: filter p xs else filter p xs

theorem List.length_filter_le {α : Type u_1} (p : α → Bool) (l : List α) : (filter p l).length ≤ l.length

@[simp]

theorem List.filter_eq_self {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} : filter p l = l ↔ ∀ (a : α✝), a ∈ l → p a = true

theorem List.filter_bne_eq_self_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) : filter (fun (x : α) => x != a) l = l

@[simp]

theorem List.length_filter_eq_length_iff {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} : (filter p l).length = l.length ↔ ∀ (a : α✝), a ∈ l → p a = true

@[simp]

theorem List.mem_filter {α✝ : Type u_1} {p : α✝ → Bool} {as : List α✝} {x : α✝} : x ∈ filter p as ↔ x ∈ as ∧ p x = true

@[simp]

theorem List.filter_eq_nil_iff {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} : filter p l = [] ↔ ∀ (a : α✝), a ∈ l → ¬p a = true

theorem List.forall_mem_filter {α : Type u_1} {l : List α} {p : α → Bool} {P : α → Prop} : (∀ (i : α), i ∈ filter p l → P i) ↔ ∀ (j : α), j ∈ l → p j = true → P j

theorem List.getElem_filter {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} (h : i < (filter p xs).length) : p (filter p xs)[i] = true

theorem List.getElem?_filter {α : Type u_1} {a : α} {xs : List α} {p : α → Bool} {i : Nat} (h : i < (filter p xs).length) (w : (filter p xs)[i]? = some a) : p a = true

@[simp]

theorem List.filter_filter {α✝ : Type u_1} {p q : α✝ → Bool} {l : List α✝} : filter p (filter q l) = filter (fun (a : α✝) => p a && q a) l

theorem List.foldl_filter {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : β → α → β} {l : List α} {init : β} : foldl f init (filter p l) = foldl (fun (x : β) (y : α) => if p y = true then f x y else x) init l

theorem List.foldl_ite_left {α : Type u_1} {β : Type u_2} {P : α → Prop} [DecidablePred P] {l : List α} {f : β → α → β} {init : β} : foldl (fun (sofar : β) (a : α) => if P a then f sofar a else sofar) init l = foldl f init (filter (fun (b : α) => decide (P b)) l)

theorem List.foldl_ite_right {α : Type u_1} {β : Type u_2} {P : α → Prop} [DecidablePred P] {l : List α} {f : β → α → β} {init : β} : foldl (fun (sofar : β) (a : α) => if P a then sofar else f sofar a) init l = foldl f init (filter (fun (a : α) => decide ¬P a) l)

theorem List.foldr_filter {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → β → β} {l : List α} {init : β} : foldr f init (filter p l) = foldr (fun (x : α) (y : β) => if p x = true then f x y else y) init l

theorem List.filter_map {β : Type u_1} {α : Type u_2} {f : β → α} {p : α → Bool} {l : List β} : filter p (map f l) = map f (filter (p ∘ f) l)

theorem List.map_filter_eq_foldr {α : Type u_1} {β : Type u_2} {f : α → β} {p : α → Bool} {as : List α} : map f (filter p as) = foldr (fun (a : α) (bs : List β) => if p a = true then f a :: bs else bs) [] as

@[simp]

theorem List.filter_append {α : Type u_1} {p : α → Bool} (l₁ l₂ : List α) : filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂

theorem List.filter_eq_cons_iff {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} {a : α✝} {as : List α✝} : filter p l = a :: as ↔ ∃ (l₁ : List α✝), ∃ (l₂ : List α✝), l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

theorem List.filter_congr {α : Type u_1} {p q : α → Bool} {l : List α} : (∀ (x : α), x ∈ l → p x = q x) → filter p l = filter q l

theorem List.head_filter_of_pos {α : Type u_1} {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.head w) = true) : (filter p l).head ⋯ = l.head w

@[simp]

theorem List.filter_sublist {α : Type u_1} {p : α → Bool} {l : List α} : (filter p l).Sublist l

filterMap

@[simp]

theorem List.filterMap_cons_none {α : Type u_1} {β : Type u_2} {f : α → Option β} {a : α} {l : List α} (h : f a = none) : filterMap f (a :: l) = filterMap f l

@[simp]

theorem List.filterMap_cons_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {a : α} {l : List α} {b : β} (h : f a = some b) : filterMap f (a :: l) = b :: filterMap f l

@[simp]

theorem List.filterMap_eq_map {α : Type u_1} {β : Type u_2} {f : α → β} : filterMap (some ∘ f) = map f

@[simp]

theorem List.filterMap_eq_map' {α : Type u_1} {β : Type u_2} {f : α → β} : (filterMap fun (x : α) => some (f x)) = map f

Variant of filterMap_eq_map with some ∘ f expanded out to a lambda.

theorem List.filterMap_some_fun {α : Type u_1} : filterMap some = id

@[simp]

theorem List.filterMap_some {α : Type u_1} {l : List α} : filterMap some l = l

theorem List.map_filterMap_some_eq_filter_map_isSome {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} : map some (filterMap f l) = filter (fun (b : Option β) => b.isSome) (map f l)

theorem List.length_filterMap_le {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : (filterMap f l).length ≤ l.length

@[simp]

theorem List.filterMap_length_eq_length {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {l : List α✝} : (filterMap f l).length = l.length ↔ ∀ (a : α✝), a ∈ l → (f a).isSome = true

@[simp]

theorem List.filterMap_eq_filter {α : Type u_1} {p : α → Bool} : filterMap (Option.guard fun (x : α) => p x) = filter p

theorem List.filterMap_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → Option γ} {l : List α} : filterMap g (filterMap f l) = filterMap (fun (x : α) => (f x).bind g) l

theorem List.map_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {l : List α} : map g (filterMap f l) = filterMap (fun (x : α) => Option.map g (f x)) l

@[simp]

theorem List.filterMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {l : List α} : filterMap g (map f l) = filterMap (g ∘ f) l

theorem List.filter_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {l : List α} : filter p (filterMap f l) = filterMap (fun (x : α) => Option.filter p (f x)) l

theorem List.filterMap_filter {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : α → Option β} {l : List α} : filterMap f (filter p l) = filterMap (fun (x : α) => if p x = true then f x else none) l

@[simp]

theorem List.mem_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {b : β} : b ∈ filterMap f l ↔ ∃ (a : α), a ∈ l ∧ f a = some b

theorem List.forall_mem_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {P : β → Prop} : (∀ (i : β), i ∈ filterMap f l → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

@[simp]

theorem List.filterMap_append {α : Type u_1} {β : Type u_2} {l l' : List α} {f : α → Option β} : filterMap f (l ++ l') = filterMap f l ++ filterMap f l'

theorem List.map_filterMap_of_inv {α : Type u_1} {β : Type u_2} {f : α → Option β} {g : β → α} (H : ∀ (x : α), Option.map g (f x) = some x) {l : List α} : map g (filterMap f l) = l

theorem List.head_filterMap_of_eq_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (w : l ≠ []) {b : β} (h : f (l.head w) = some b) : (filterMap f l).head ⋯ = b

theorem List.forall_none_of_filterMap_eq_nil {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {xs : List α✝} (h : filterMap f xs = []) (x : α✝) : x ∈ xs → f x = none

@[simp]

theorem List.filterMap_eq_nil_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {l : List α✝} : filterMap f l = [] ↔ ∀ (a : α✝), a ∈ l → f a = none

theorem List.filterMap_eq_cons_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {l : List α✝} {b : α✝¹} {bs : List α✝¹} : filterMap f l = b :: bs ↔ ∃ (l₁ : List α✝), ∃ (a : α✝), ∃ (l₂ : List α✝), l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → f x = none) ∧ f a = some b ∧ filterMap f l₂ = bs

append

@[simp]

theorem List.nil_append_fun {α : Type u_1} : (fun (x : List α) => [] ++ x) = id

@[simp]

theorem List.cons_append_fun {α : Type u_1} {a : α} {as : List α} : (fun (bs : List α) => a :: as ++ bs) = fun (bs : List α) => a :: (as ++ bs)

@[simp]

theorem List.mem_append {α : Type u_1} {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

theorem List.not_mem_append {α : Type u_1} {a : α} {s t : List α} (h₁ : ¬a ∈ s) (h₂ : ¬a ∈ t) : ¬a ∈ s ++ t

theorem List.append_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

See also eq_append_cons_of_mem, which proves a stronger version in which the initial list must not contain the element.

theorem List.mem_iff_append {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

theorem List.forall_mem_append {α : Type u_1} {p : α → Prop} {l₁ l₂ : List α} : (∀ (x : α), x ∈ l₁ ++ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

theorem List.getElem_append {α : Type u_1} {l₁ l₂ : List α} {i : Nat} (h : i < (l₁ ++ l₂).length) : (l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]

theorem List.getElem?_append_left {α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i]? = l₁[i]?

theorem List.getElem?_append_right {α : Type u_1} {l₁ l₂ : List α} {i : Nat} : l₁.length ≤ i → (l₁ ++ l₂)[i]? = l₂[i - l₁.length]?

theorem List.getElem?_append {α : Type u_1} {l₁ l₂ : List α} {i : Nat} : (l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]?

theorem List.getElem_append_left' {α : Type u_1} {l₁ : List α} {i : Nat} (hi : i < l₁.length) (l₂ : List α) : l₁[i] = (l₁ ++ l₂)[i]

Variant of getElem_append_left useful for rewriting from the small list to the big list.

theorem List.getElem_append_right' {α : Type u_1} (l₁ : List α) {l₂ : List α} {i : Nat} (hi : i < l₂.length) : l₂[i] = (l₁ ++ l₂)[i + l₁.length]

Variant of getElem_append_right useful for rewriting from the small list to the big list.

theorem List.getElem_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {i : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) : l[i] = a

@[simp]

theorem List.singleton_append {α✝ : Type u_1} {x : α✝} {l : List α✝} : [x] ++ l = x :: l

theorem List.append_inj {α : Type u_1} {s₁ s₂ t₁ t₂ : List α} : s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂ ∧ t₁ = t₂

theorem List.append_inj_right {α✝ : Type u_1} {s₁ t₁ s₂ t₂ : List α✝} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.length = s₂.length) : t₁ = t₂

theorem List.append_inj_left {α✝ : Type u_1} {s₁ t₁ s₂ t₂ : List α✝} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.length = s₂.length) : s₁ = s₂

theorem List.append_inj' {α✝ : Type u_1} {s₁ t₁ s₂ t₂ : List α✝} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) : s₁ = s₂ ∧ t₁ = t₂

Variant of append_inj instead requiring equality of the lengths of the second lists.

theorem List.append_inj_right' {α✝ : Type u_1} {s₁ t₁ s₂ t₂ : List α✝} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) : t₁ = t₂

Variant of append_inj_right instead requiring equality of the lengths of the second lists.

theorem List.append_inj_left' {α✝ : Type u_1} {s₁ t₁ s₂ t₂ : List α✝} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) : s₁ = s₂

Variant of append_inj_left instead requiring equality of the lengths of the second lists.

theorem List.append_right_inj {α : Type u_1} {t₁ t₂ : List α} (s : List α) : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂

theorem List.append_left_inj {α : Type u_1} {s₁ s₂ : List α} (t : List α) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂

@[simp]

theorem List.append_left_eq_self {α : Type u_1} {xs ys : List α} : xs ++ ys = ys ↔ xs = []

@[simp]

theorem List.self_eq_append_left {α : Type u_1} {xs ys : List α} : ys = xs ++ ys ↔ xs = []

@[simp]

theorem List.append_right_eq_self {α : Type u_1} {xs ys : List α} : xs ++ ys = xs ↔ ys = []

@[simp]

theorem List.self_eq_append_right {α : Type u_1} {xs ys : List α} : xs = xs ++ ys ↔ ys = []

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

@[simp]

theorem List.append_eq_nil_iff {α✝ : Type u_1} {p q : List α✝} : p ++ q = [] ↔ p = [] ∧ q = []

theorem List.nil_eq_append_iff {α✝ : Type u_1} {a b : List α✝} : [] = a ++ b ↔ a = [] ∧ b = []

theorem List.eq_nil_of_append_eq_nil {α : Type u_1} {l₁ l₂ : List α} (h : l₁ ++ l₂ = []) : l₁ = [] ∧ l₂ = []

theorem List.append_ne_nil_of_left_ne_nil {α : Type u_1} {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ []

theorem List.append_ne_nil_of_right_ne_nil {α : Type u_1} {t : List α} (s : List α) : t ≠ [] → s ++ t ≠ []

theorem List.append_eq_cons_iff {α✝ : Type u_1} {as bs : List α✝} {x : α✝} {c : List α✝} : as ++ bs = x :: c ↔ as = [] ∧ bs = x :: c ∨ ∃ (as' : List α✝), as = x :: as' ∧ c = as' ++ bs

theorem List.cons_eq_append_iff {α✝ : Type u_1} {x : α✝} {cs as bs : List α✝} : x :: cs = as ++ bs ↔ as = [] ∧ bs = x :: cs ∨ ∃ (as' : List α✝), as = x :: as' ∧ cs = as' ++ bs

theorem List.append_eq_singleton_iff {α✝ : Type u_1} {a b : List α✝} {x : α✝} : a ++ b = [x] ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []

theorem List.singleton_eq_append_iff {α✝ : Type u_1} {x : α✝} {a b : List α✝} : [x] = a ++ b ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []

theorem List.append_eq_append_iff {α : Type u_1} {ws xs ys zs : List α} : ws ++ xs = ys ++ zs ↔ (∃ (as : List α), ys = ws ++ as ∧ xs = as ++ zs) ∨ ∃ (bs : List α), ws = ys ++ bs ∧ zs = bs ++ xs

@[simp]

theorem List.head_append_of_ne_nil {α : Type u_1} {l' l : List α} {w₁ : l ++ l' ≠ []} (w₂ : l ≠ []) : (l ++ l').head w₁ = l.head w₂

theorem List.head_append {α : Type u_1} {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) : (l₁ ++ l₂).head w = if h : l₁.isEmpty = true then l₂.head ⋯ else l₁.head ⋯

theorem List.head_append_left {α : Type u_1} {l₁ l₂ : List α} (h : l₁ ≠ []) : (l₁ ++ l₂).head ⋯ = l₁.head h

theorem List.head_append_right {α : Type u_1} {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l₁ = []) : (l₁ ++ l₂).head w = l₂.head ⋯

@[simp]

theorem List.head?_append {α : Type u_1} {l' l : List α} : (l ++ l').head? = l.head?.or l'.head?

theorem List.tail?_append {α : Type u_1} {l l' : List α} : (l ++ l').tail? = (Option.map (fun (x : List α) => x ++ l') l.tail?).or l'.tail?

theorem List.tail?_append_of_ne_nil {α : Type u_1} {l l' : List α} : l ≠ [] → (l ++ l').tail? = some (l.tail ++ l')

theorem List.tail_append {α : Type u_1} {l l' : List α} : (l ++ l').tail = if l.isEmpty = true then l'.tail else l.tail ++ l'

@[simp]

theorem List.tail_append_of_ne_nil {α : Type u_1} {xs ys : List α} (h : xs ≠ []) : (xs ++ ys).tail = xs.tail ++ ys

theorem List.set_append {α : Type u_1} {i : Nat} {x : α} {s t : List α} : (s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x

@[simp]

theorem List.set_append_left {α : Type u_1} {s t : List α} (i : Nat) (x : α) (h : i < s.length) : (s ++ t).set i x = s.set i x ++ t

@[simp]

theorem List.set_append_right {α : Type u_1} {s t : List α} (i : Nat) (x : α) (h : s.length ≤ i) : (s ++ t).set i x = s ++ t.set (i - s.length) x

theorem List.filterMap_eq_append_iff {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : α → Option β} : filterMap f l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

theorem List.append_eq_filterMap_iff {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : α → Option β} : L₁ ++ L₂ = filterMap f l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

theorem List.filter_eq_append_iff {α : Type u_1} {l L₁ L₂ : List α} {p : α → Bool} : filter p l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

theorem List.append_eq_filter_iff {α : Type u_1} {L₁ L₂ l : List α} {p : α → Bool} : L₁ ++ L₂ = filter p l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

@[simp]

theorem List.map_append {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ l₂ : List α} : map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

theorem List.map_eq_append_iff {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : α → β} : map f l = L₁ ++ L₂ ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

theorem List.append_eq_map_iff {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : α → β} : L₁ ++ L₂ = map f l ↔ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

@[simp]

theorem List.sum_append {α : Type u_1} [Add α] [Zero α] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 + x2) 0] [Std.Associative fun (x1 x2 : α) => x1 + x2] {l₁ l₂ : List α} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum

@[simp]

theorem List.sum_singleton {α : Type u_1} [Add α] [Zero α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 + x2) 0] {x : α} : [x].sum = x

@[simp]

theorem List.sum_reverse {α : Type u_1} [Zero α] [Add α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.Commutative fun (x1 x2 : α) => x1 + x2] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 + x2) 0] (xs : List α) : xs.reverse.sum = xs.sum

@[simp]

theorem List.prod_append {α : Type u_1} [Mul α] [One α] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 * x2) 1] [Std.Associative fun (x1 x2 : α) => x1 * x2] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod

@[simp]

theorem List.prod_singleton {α : Type u_1} [Mul α] [One α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 * x2) 1] {x : α} : [x].prod = x

@[simp]

theorem List.prod_reverse {α : Type u_1} [One α] [Mul α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.Commutative fun (x1 x2 : α) => x1 * x2] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 * x2) 1] (xs : List α) : xs.reverse.prod = xs.prod

concat

Note that concat_eq_append is a @[simp] lemma, so concat should usually not appear in goals. As such there's no need for a thorough set of lemmas describing concat.

theorem List.concat_nil {α : Type u_1} {a : α} : [].concat a = [a]

theorem List.concat_cons {α : Type u_1} {a b : α} {l : List α} : (a :: l).concat b = a :: l.concat b

theorem List.init_eq_of_concat_eq {α : Type u_1} {a b : α} {l₁ l₂ : List α} : l₁.concat a = l₂.concat b → l₁ = l₂

theorem List.last_eq_of_concat_eq {α : Type u_1} {a b : α} {l₁ l₂ : List α} : l₁.concat a = l₂.concat b → a = b

theorem List.concat_inj {α : Type u_1} {a b : α} {l l' : List α} : l.concat a = l'.concat b ↔ l = l' ∧ a = b

theorem List.concat_inj_left {α : Type u_1} {l l' : List α} (a : α) : l.concat a = l'.concat a ↔ l = l'

theorem List.concat_inj_right {α : Type u_1} {l : List α} {a a' : α} : l.concat a = l.concat a' ↔ a = a'

theorem List.concat_append {α : Type u_1} {a : α} {l₁ l₂ : List α} : l₁.concat a ++ l₂ = l₁ ++ a :: l₂

theorem List.append_concat {α : Type u_1} {a : α} {l₁ l₂ : List α} : l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a

theorem List.map_concat {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {l : List α} : map f (l.concat a) = (map f l).concat (f a)

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

flatten

@[simp]

theorem List.length_flatten {α : Type u_1} {L : List (List α)} : L.flatten.length = (map length L).sum

theorem List.flatten_singleton {α : Type u_1} {l : List α} : [l].flatten = l

@[simp]

theorem List.mem_flatten {α : Type u_1} {a : α} {L : List (List α)} : a ∈ L.flatten ↔ ∃ (l : List α), l ∈ L ∧ a ∈ l

@[simp]

theorem List.flatten_eq_nil_iff {α : Type u_1} {L : List (List α)} : L.flatten = [] ↔ ∀ (l : List α), l ∈ L → l = []

theorem List.nil_eq_flatten_iff {α : Type u_1} {L : List (List α)} : [] = L.flatten ↔ ∀ (l : List α), l ∈ L → l = []

theorem List.flatten_ne_nil_iff {α : Type u_1} {xss : List (List α)} : xss.flatten ≠ [] ↔ ∃ (xs : List α), xs ∈ xss ∧ xs ≠ []

theorem List.exists_of_mem_flatten {α✝ : Type u_1} {L : List (List α✝)} {a : α✝} : a ∈ L.flatten → ∃ (l : List α✝), l ∈ L ∧ a ∈ l

theorem List.mem_flatten_of_mem {α✝ : Type u_1} {L : List (List α✝)} {l : List α✝} {a : α✝} (lL : l ∈ L) (al : a ∈ l) : a ∈ L.flatten

theorem List.forall_mem_flatten {α : Type u_1} {p : α → Prop} {L : List (List α)} : (∀ (x : α), x ∈ L.flatten → p x) ↔ ∀ (l : List α), l ∈ L → ∀ (x : α), x ∈ l → p x

theorem List.flatten_eq_flatMap {α : Type u_1} {L : List (List α)} : L.flatten = flatMap id L

theorem List.head?_flatten {α : Type u_1} {L : List (List α)} : L.flatten.head? = findSome? (fun (l : List α) => l.head?) L

@[simp]

theorem List.map_flatten {α : Type u_1} {β : Type u_2} {f : α → β} {L : List (List α)} : map f L.flatten = (map (map f) L).flatten

@[simp]

theorem List.filterMap_flatten {α : Type u_1} {β : Type u_2} {f : α → Option β} {L : List (List α)} : filterMap f L.flatten = (map (filterMap f) L).flatten

@[simp]

theorem List.filter_flatten {α : Type u_1} {p : α → Bool} {L : List (List α)} : filter p L.flatten = (map (filter p) L).flatten

theorem List.flatten_filter_not_isEmpty {α : Type u_1} {L : List (List α)} : (filter (fun (l : List α) => !l.isEmpty) L).flatten = L.flatten

theorem List.flatten_filter_ne_nil {α : Type u_1} [DecidablePred fun (l : List α) => l ≠ []] {L : List (List α)} : (filter (fun (l : List α) => decide (l ≠ [])) L).flatten = L.flatten

@[simp]

theorem List.flatten_append {α : Type u_1} {L₁ L₂ : List (List α)} : (L₁ ++ L₂).flatten = L₁.flatten ++ L₂.flatten

theorem List.flatten_concat {α : Type u_1} {L : List (List α)} {l : List α} : (L ++ [l]).flatten = L.flatten ++ l

theorem List.flatten_flatten {α : Type u_1} {L : List (List (List α))} : L.flatten.flatten = (map flatten L).flatten

theorem List.flatten_eq_cons_iff {α : Type u_1} {xss : List (List α)} {y : α} {ys : List α} : xss.flatten = y :: ys ↔ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (cs : List (List α)), xss = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

theorem List.cons_eq_flatten_iff {α : Type u_1} {xs : List (List α)} {y : α} {ys : List α} : y :: ys = xs.flatten ↔ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (cs : List (List α)), xs = as ++ (y :: bs) :: cs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ys = bs ++ cs.flatten

theorem List.flatten_eq_singleton_iff {α : Type u_1} {xs : List (List α)} {y : α} : xs.flatten = [y] ↔ ∃ (as : List (List α)), ∃ (bs : List (List α)), xs = as ++ [y] :: bs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ∀ (l : List α), l ∈ bs → l = []

theorem List.singleton_eq_flatten_iff {α : Type u_1} {xs : List (List α)} {y : α} : [y] = xs.flatten ↔ ∃ (as : List (List α)), ∃ (bs : List (List α)), xs = as ++ [y] :: bs ∧ (∀ (l : List α), l ∈ as → l = []) ∧ ∀ (l : List α), l ∈ bs → l = []

theorem List.flatten_eq_append_iff {α : Type u_1} {xss : List (List α)} {ys zs : List α} : xss.flatten = ys ++ zs ↔ (∃ (as : List (List α)), ∃ (bs : List (List α)), xss = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (c : α), ∃ (cs : List α), ∃ (ds : List (List α)), xss = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

theorem List.append_eq_flatten_iff {α : Type u_1} {xs : List (List α)} {ys zs : List α} : ys ++ zs = xs.flatten ↔ (∃ (as : List (List α)), ∃ (bs : List (List α)), xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨ ∃ (as : List (List α)), ∃ (bs : List α), ∃ (c : α), ∃ (cs : List α), ∃ (ds : List (List α)), xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

theorem List.eq_iff_flatten_eq {α : Type u_1} {L L' : List (List α)} : L = L' ↔ L.flatten = L'.flatten ∧ map length L = map length L'

Two lists of sublists are equal iff their flattens coincide, as well as the lengths of the sublists.

flatMap

theorem List.flatMap_def {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : flatMap f l = (map f l).flatten

@[simp]

theorem List.flatMap_id {α : Type u_1} {L : List (List α)} : flatMap id L = L.flatten

@[simp]

theorem List.flatMap_id' {α : Type u_1} {L : List (List α)} : flatMap (fun (as : List α) => as) L = L.flatten

@[simp]

theorem List.length_flatMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : (flatMap f l).length = (map (fun (a : α) => (f a).length) l).sum

@[simp]

theorem List.mem_flatMap {α : Type u_1} {β : Type u_2} {f : α → List β} {b : β} {l : List α} : b ∈ flatMap f l ↔ ∃ (a : α), a ∈ l ∧ b ∈ f a

theorem List.exists_of_mem_flatMap {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} : b ∈ flatMap f l → ∃ (a : α), a ∈ l ∧ b ∈ f a

theorem List.mem_flatMap_of_mem {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} {a : α} (al : a ∈ l) (h : b ∈ f a) : b ∈ flatMap f l

@[simp]

theorem List.flatMap_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : flatMap f l = [] ↔ ∀ (x : α), x ∈ l → f x = []

theorem List.forall_mem_flatMap {β : Type u_1} {α : Type u_2} {p : β → Prop} {l : List α} {f : α → List β} : (∀ (x : β), x ∈ flatMap f l → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

theorem List.flatMap_singleton {α : Type u_1} {β : Type u_2} (f : α → List β) (x : α) : flatMap f [x] = f x

@[simp]

theorem List.flatMap_singleton' {α : Type u_1} (l : List α) : flatMap (fun (x : α) => [x]) l = l

theorem List.head?_flatMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : (flatMap f l).head? = findSome? (fun (a : α) => (f a).head?) l

theorem List.flatMap_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : α → List β} {g : β → List γ} : flatMap g (flatMap f l) = flatMap (fun (x : α) => flatMap g (f x)) l

theorem List.map_flatMap {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {g : α → List β} {l : List α} : map f (flatMap g l) = flatMap (fun (a : α) => map f (g a)) l

theorem List.flatMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → List γ) (l : List α) : flatMap g (map f l) = flatMap (fun (a : α) => g (f a)) l

theorem List.map_eq_flatMap {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : map f l = flatMap (fun (x : α) => [f x]) l

theorem List.filterMap_flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {g : α → List β} {f : β → Option γ} : filterMap f (flatMap g l) = flatMap (fun (a : α) => filterMap f (g a)) l

theorem List.filter_flatMap {α : Type u_1} {β : Type u_2} {l : List α} {g : α → List β} {f : β → Bool} : filter f (flatMap g l) = flatMap (fun (a : α) => filter f (g a)) l

theorem List.flatMap_eq_foldl {α : Type u_1} {β : Type u_2} {f : α → List β} {l : List α} : flatMap f l = foldl (fun (acc : List β) (a : α) => acc ++ f a) [] l

replicate

@[simp]

theorem List.replicate_one {α✝ : Type u_1} {a : α✝} : replicate 1 a = [a]

theorem List.replicate_succ' {n : Nat} {α✝ : Type u_1} {a : α✝} : replicate (n + 1) a = replicate n a ++ [a]

Variant of replicate_succ that concatenates a to the end of the list.

@[simp]

theorem List.mem_replicate {α : Type u_1} {a b : α} {n : Nat} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

@[simp]

theorem List.contains_replicate {α : Type u_1} [BEq α] {n : Nat} {a b : α} : (replicate n b).contains a = (a == b && !n == 0)

theorem List.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : Nat} (h : b ∈ replicate n a) : b = a

theorem List.forall_mem_replicate {α : Type u_1} {p : α → Prop} {a : α} {n : Nat} : (∀ (b : α), b ∈ replicate n a → p b) ↔ n = 0 ∨ p a

@[simp]

theorem List.replicate_succ_ne_nil {α : Type u_1} {n : Nat} {a : α} : replicate (n + 1) a ≠ []

@[simp]

theorem List.replicate_eq_nil_iff {α : Type u_1} {n : Nat} (a : α) : replicate n a = [] ↔ n = 0

@[simp]

theorem List.getElem_replicate {α : Type u_1} {a : α} {n i : Nat} (h : i < (replicate n a).length) : (replicate n a)[i] = a

theorem List.getElem?_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {i : Nat} : (replicate n a)[i]? = if i < n then some a else none

@[simp]

theorem List.getElem?_replicate_of_lt {α✝ : Type u_1} {a : α✝} {n i : Nat} (h : i < n) : (replicate n a)[i]? = some a

theorem List.head?_replicate {α : Type u_1} {a : α} {n : Nat} : (replicate n a).head? = if n = 0 then none else some a

@[simp]

theorem List.head_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} (w : replicate n a ≠ []) : (replicate n a).head w = a

@[simp]

theorem List.tail_replicate {α : Type u_1} {n : Nat} {a : α} : (replicate n a).tail = replicate (n - 1) a

@[simp]

theorem List.replicate_inj {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} {b : α✝} : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b)

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

theorem List.eq_replicate_iff {α : Type u_1} {a : α} {n : Nat} {l : List α} : l = replicate n a ↔ l.length = n ∧ ∀ (b : α), b ∈ l → b = a

theorem List.map_eq_replicate_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {b : β} : map f l = replicate l.length b ↔ ∀ (x : α), x ∈ l → f x = b

@[simp]

theorem List.map_const {α : Type u_1} {β : Type u_2} {l : List α} {b : β} : map (Function.const α b) l = replicate l.length b

@[simp]

theorem List.map_const_fun {β : Type u_1} {α : Type u_2} {x : β} : map (Function.const α x) = fun (x_1 : List α) => replicate x_1.length x

theorem List.map_const' {α : Type u_1} {β : Type u_2} {l : List α} {b : β} : map (fun (x : α) => b) l = replicate l.length b

Variant of map_const using a lambda rather than Function.const.

@[simp]

theorem List.set_replicate_self {n : Nat} {α✝ : Type u_1} {a : α✝} {i : Nat} : (replicate n a).set i a = replicate n a

@[simp]

theorem List.replicate_append_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} : replicate n a ++ replicate m a = replicate (n + m) a

theorem List.append_eq_replicate_iff {α : Type u_1} {n : Nat} {l₁ l₂ : List α} {a : α} : l₁ ++ l₂ = replicate n a ↔ l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a

theorem List.replicate_eq_append_iff {α : Type u_1} {n : Nat} {l₁ l₂ : List α} {a : α} : replicate n a = l₁ ++ l₂ ↔ l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a

@[simp]

theorem List.map_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : map f (replicate n a) = replicate n (f a)

theorem List.filter_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {p : α✝ → Bool} : filter p (replicate n a) = if p a = true then replicate n a else []

@[simp]

theorem List.filter_replicate_of_pos {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : p a = true) : filter p (replicate n a) = replicate n a

@[simp]

theorem List.filter_replicate_of_neg {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) : filter p (replicate n a) = []

theorem List.filterMap_replicate {α : Type u_1} {β : Type u_2} {n : Nat} {a : α} {f : α → Option β} : filterMap f (replicate n a) = match f a with | none => [] | some b => replicate n b

theorem List.filterMap_replicate_of_some {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : Nat} {f : α → Option β} (h : f a = some b) : filterMap f (replicate n a) = replicate n b

@[simp]

theorem List.filterMap_replicate_of_isSome {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : α → Option β} (h : (f a).isSome = true) : filterMap f (replicate n a) = replicate n ((f a).get h)

@[simp]

theorem List.filterMap_replicate_of_none {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : α → Option β} (h : f a = none) : filterMap f (replicate n a) = []

@[simp]

theorem List.flatten_replicate_nil {n : Nat} {α : Type u_1} : (replicate n []).flatten = []

@[simp]

theorem List.flatten_replicate_singleton {n : Nat} {α✝ : Type u_1} {a : α✝} : (replicate n [a]).flatten = replicate n a

@[simp]

theorem List.flatten_replicate_replicate {n m : Nat} {α✝ : Type u_1} {a : α✝} : (replicate n (replicate m a)).flatten = replicate (n * m) a

theorem List.flatMap_replicate {α : Type u_1} {n : Nat} {a : α} {β : Type u_2} {f : α → List β} : flatMap f (replicate n a) = (replicate n (f a)).flatten

@[simp]

theorem List.isEmpty_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} : (replicate n a).isEmpty = decide (n = 0)

theorem List.eq_replicate_or_eq_replicate_append_cons {α : Type u_1} (l : List α) : l = [] ∨ (∃ (n : Nat), ∃ (a : α), l = replicate n a ∧ 0 < n) ∨ ∃ (n : Nat), ∃ (a : α), ∃ (b : α), ∃ (l' : List α), l = replicate n a ++ b :: l' ∧ 0 < n ∧ a ≠ b

Every list is either empty, a non-empty replicate, or begins with a non-empty replicate followed by a different element.

theorem List.replicateRecOn {α : Type u_1} {p : List α → Prop} (l : List α) (h0 : p []) (hr : ∀ (a : α) (n : Nat), 0 < n → p (replicate n a)) (hi : ∀ (a b : α) (n : Nat) (l : List α), a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)) : p l

An induction principle for lists based on contiguous runs of identical elements.

reverse

@[simp]

theorem List.length_reverse {α : Type u_1} {as : List α} : as.reverse.length = as.length

theorem List.mem_reverseAux {α : Type u_1} {x : α} {as bs : List α} : x ∈ as.reverseAux bs ↔ x ∈ as ∨ x ∈ bs

@[simp]

theorem List.mem_reverse {α : Type u_1} {x : α} {as : List α} : x ∈ as.reverse ↔ x ∈ as

@[simp]

theorem List.reverse_eq_nil_iff {α : Type u_1} {xs : List α} : xs.reverse = [] ↔ xs = []

theorem List.reverse_ne_nil_iff {α : Type u_1} {xs : List α} : xs.reverse ≠ [] ↔ xs ≠ []

@[simp]

theorem List.isEmpty_reverse {α : Type u_1} {xs : List α} : xs.reverse.isEmpty = xs.isEmpty

theorem List.getElem?_reverse' {α : Type u_1} {l : List α} {i j : Nat} : i + j + 1 = l.length → l.reverse[i]? = l[j]?

Variant of getElem?_reverse with a hypothesis giving the linear relation between the indices.

@[simp]

theorem List.getElem?_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) : l.reverse[i]? = l[l.length - 1 - i]?

@[simp]

theorem List.getElem_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.reverse.length) : l.reverse[i] = l[l.length - 1 - i]

theorem List.reverseAux_reverseAux_nil {α : Type u_1} {as bs : List α} : (as.reverseAux bs).reverseAux [] = bs.reverseAux as

@[simp]

theorem List.reverse_reverse {α : Type u_1} (as : List α) : as.reverse.reverse = as

theorem List.reverse_eq_iff {α : Type u_1} {as bs : List α} : as.reverse = bs ↔ as = bs.reverse

@[simp]

theorem List.reverse_inj {α : Type u_1} {xs ys : List α} : xs.reverse = ys.reverse ↔ xs = ys

@[simp]

theorem List.reverse_eq_cons_iff {α : Type u_1} {xs : List α} {a : α} {ys : List α} : xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a]

@[simp]

theorem List.getLast?_reverse {α : Type u_1} {l : List α} : l.reverse.getLast? = l.head?

@[simp]

theorem List.head?_reverse {α : Type u_1} {l : List α} : l.reverse.head? = l.getLast?

theorem List.getLast?_eq_head?_reverse {α : Type u_1} {xs : List α} : xs.getLast? = xs.reverse.head?

theorem List.head?_eq_getLast?_reverse {α : Type u_1} {xs : List α} : xs.head? = xs.reverse.getLast?

theorem List.mem_of_getLast? {α : Type u_1} {l : List α} {a : α} (h : l.getLast? = some a) : a ∈ l

theorem List.mem_of_mem_getLast? {α : Type u_1} {l : List α} {a : α} (h : a ∈ l.getLast?) : a ∈ l

theorem List.getLast_of_getLast?_eq_some {α : Type u_1} {x : α} {l : List α} (hx : l.getLast? = some x) : l.getLast ⋯ = x

theorem List.getLast_of_mem_getLast? {α : Type u_1} {x : α} {l : List α} (hx : x ∈ l.getLast?) : l.getLast ⋯ = x

@[simp]

theorem List.map_reverse {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : map f l.reverse = (map f l).reverse

@[simp]

theorem List.filter_reverse {α : Type u_1} {p : α → Bool} {l : List α} : filter p l.reverse = (filter p l).reverse

@[simp]

theorem List.filterMap_reverse {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} : filterMap f l.reverse = (filterMap f l).reverse

@[simp]

theorem List.reverse_append {α : Type u_1} {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse

@[simp]

theorem List.reverse_eq_append_iff {α : Type u_1} {xs ys zs : List α} : xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

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

theorem List.reverse_eq_concat {α : Type u_1} {xs ys : List α} {a : α} : xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse

theorem List.reverse_flatten {α : Type u_1} {L : List (List α)} : L.flatten.reverse = (map reverse L).reverse.flatten

Reversing a flatten is the same as reversing the order of parts and reversing all parts.

theorem List.flatten_reverse {α : Type u_1} {L : List (List α)} : L.reverse.flatten = (map reverse L).flatten.reverse

Flattening a reverse is the same as reversing all parts and reversing the flattened result.

theorem List.reverse_flatMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : (flatMap f l).reverse = flatMap (reverse ∘ f) l.reverse

theorem List.flatMap_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : flatMap f l.reverse = (flatMap (reverse ∘ f) l).reverse

@[simp]

theorem List.reverseAux_eq {α : Type u_1} {as bs : List α} : as.reverseAux bs = as.reverse ++ bs

@[simp]

theorem List.reverse_replicate {α : Type u_1} {n : Nat} {a : α} : (replicate n a).reverse = replicate n a

theorem List.reverse_singleton {α : Type u_1} {a : α} : [a].reverse = [a]

@[simp]

theorem List.append_singleton_inj {α : Type u_1} {a b : α} {as bs : List α} : as ++ [a] = bs ++ [b] ↔ as = bs ∧ a = b

foldlM and foldrM

@[simp]

theorem List.foldlM_append {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] {f : β → α → m β} {b : β} {l l' : List α} : foldlM f b (l ++ l') = do let init ← foldlM f b l foldlM f init l'

@[simp]

theorem List.foldrM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {a : α} {l : List α} {f : α → β → m β} {b : β} : foldrM f b (a :: l) = foldrM f b l >>= f a

@[simp]

theorem List.foldlM_pure {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] {f : β → α → β} {b : β} {l : List α} : foldlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) b l = pure (foldl f b l)

@[simp]

theorem List.foldrM_pure {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → β → β} {b : β} {l : List α} : foldrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) b l = pure (foldr f b l)

theorem List.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} {f : β → α → β} {b : β} {l : List α} : foldl f b l = (foldlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) b l).run

theorem List.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {l : List α} : foldr f b l = (foldrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) b l).run

theorem List.idRun_foldlM {β : Type u_1} {α : Type u_2} {f : β → α → Id β} {b : β} {l : List α} : (foldlM f b l).run = foldl (fun (x1 : β) (x2 : α) => (f x1 x2).run) b l

theorem List.idRun_foldrM {α : Type u_1} {β : Type u_2} {f : α → β → Id β} {b : β} {l : List α} : (foldrM f b l).run = foldr (fun (x1 : α) (x2 : β) => (f x1 x2).run) b l

@[simp]

theorem List.foldlM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {l : List α} {f : β → α → m β} {b : β} : foldlM f b l.reverse = foldrM (fun (x : α) (y : β) => f y x) b l

@[simp]

theorem List.foldrM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {l : List α} {f : α → β → m β} {b : β} : foldrM f b l.reverse = foldlM (fun (x : β) (y : α) => f y x) b l

foldl and foldr

@[simp]

theorem List.foldr_cons_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {l' : List β} : foldr (fun (x : α) (ys : List β) => f x :: ys) l' l = map f l ++ l'

@[simp]

theorem List.foldr_cons_eq_append' {β : Type u_1} {l l' : List β} : foldr cons l' l = l ++ l'

Variant of foldr_cons_eq_append specalized to f = id.

@[simp]

theorem List.foldl_flip_cons_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {l' : List β} : foldl (fun (xs : List β) (y : α) => f y :: xs) l' l = (map f l).reverse ++ l'

theorem List.foldl_flip_cons_eq_append' {α : Type u_1} {l l' : List α} : foldl (fun (xs : List α) (y : α) => y :: xs) l' l = l.reverse ++ l'

Variant of foldl_flip_cons_eq_append specalized to f = id.

@[simp]

theorem List.foldr_append_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : foldr (fun (x1 : α) (x2 : List β) => f x1 ++ x2) l' l = (map f l).flatten ++ l'

@[simp]

theorem List.foldl_append_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : foldl (fun (x1 : List β) (x2 : α) => x1 ++ f x2) l' l = l' ++ (map f l).flatten

@[simp]

theorem List.foldr_flip_append_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : foldr (fun (x : α) (ys : List β) => ys ++ f x) l' l = l' ++ (map f l).reverse.flatten

@[simp]

theorem List.foldl_flip_append_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β} : foldl (fun (xs : List β) (y : α) => f y ++ xs) l' l = (map f l).reverse.flatten ++ l'

theorem List.foldr_cons_nil {α : Type u_1} {l : List α} : foldr cons [] l = l

theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {f : β₁ → β₂} {g : α → β₂ → α} {l : List β₁} {init : α} : foldl g init (map f l) = foldl (fun (x : α) (y : β₁) => g x (f y)) init l

theorem List.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {f : α₁ → α₂} {g : α₂ → β → β} {l : List α₁} {init : β} : foldr g init (map f l) = foldr (fun (x : α₁) (y : β) => g (f x) y) init l

theorem List.foldl_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : γ → β → γ} {l : List α} {init : γ} : foldl g init (filterMap f l) = foldl (fun (x : γ) (y : α) => match f y with | some b => g x b | none => x) init l

theorem List.foldr_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ → γ} {l : List α} {init : γ} : foldr g init (filterMap f l) = foldr (fun (x : α) (y : γ) => match f x with | some b => g b y | none => y) init l

theorem List.foldl_map_hom {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : foldl f' (g a) (map g l) = g (foldl f a l)

theorem List.foldr_map_hom {α : Type u_1} {β : Type u_2} {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α} (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : foldr f' (g a) (map g l) = g (foldr f a l)

@[simp]

theorem List.foldrM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → β → m β} {b : β} {l l' : List α} : foldrM f b (l ++ l') = do let init ← foldrM f b l' foldrM f init l

@[simp]

theorem List.foldl_append {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {l l' : List α} : foldl f b (l ++ l') = foldl f (foldl f b l) l'

@[simp]

theorem List.foldr_append {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {l l' : List α} : foldr f b (l ++ l') = foldr f (foldr f b l') l

theorem List.foldl_flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → List β} {g : γ → β → γ} {l : List α} {init : γ} : foldl g init (flatMap f l) = foldl (fun (acc : γ) (x : α) => foldl g acc (f x)) init l

theorem List.foldr_flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → List β} {g : β → γ → γ} {l : List α} {init : γ} : foldr g init (flatMap f l) = foldr (fun (x : α) (acc : γ) => foldr g acc (f x)) init l

theorem List.foldl_flatten {β : Type u_1} {α : Type u_2} {f : β → α → β} {b : β} {L : List (List α)} : foldl f b L.flatten = foldl (fun (b : β) (l : List α) => foldl f b l) b L

theorem List.foldr_flatten {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {L : List (List α)} : foldr f b L.flatten = foldr (fun (l : List α) (b : β) => foldr f b l) b L

@[simp]

theorem List.foldl_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : β → α → β} {b : β} : foldl f b l.reverse = foldr (fun (x : α) (y : β) => f y x) b l

@[simp]

theorem List.foldr_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β} : foldr f b l.reverse = foldl (fun (x : β) (y : α) => f y x) b l

theorem List.foldl_eq_foldr_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : β → α → β} {b : β} : foldl f b l = foldr (fun (x : α) (y : β) => f y x) b l.reverse

theorem List.foldr_eq_foldl_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β} : foldr f b l = foldl (fun (x : β) (y : α) => f y x) b l.reverse

theorem List.foldl_assoc {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α} : foldl op (op a₁ a₂) l = op a₁ (foldl op a₂ l)

theorem List.foldr_assoc {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α} : foldr op (op a₁ a₂) l = op (foldr op a₁ l) a₂

theorem List.foldl_eq_apply_foldr {α : Type u_1} {init x : α} {xs : List α} {f : α → α → α} [Std.Associative f] [Std.LawfulRightIdentity f init] : foldl f x xs = f x (foldr f init xs)

theorem List.foldr_eq_apply_foldl {α : Type u_1} {init x : α} {xs : List α} {f : α → α → α} [Std.Associative f] [Std.LawfulLeftIdentity f init] : foldr f x xs = f (foldl f init xs) x

theorem List.foldr_eq_foldl {α : Type u_1} {init : α} {xs : List α} {f : α → α → α} [Std.Associative f] [Std.LawfulIdentity f init] : foldr f init xs = foldl f init xs

theorem List.sum_eq_foldl {α : Type u_1} [Zero α] [Add α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {xs : List α} : xs.sum = foldl (fun (x1 x2 : α) => x1 + x2) 0 xs

theorem List.prod_eq_foldl {α : Type u_1} [One α] [Mul α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {xs : List α} : xs.prod = foldl (fun (x1 x2 : α) => x1 * x2) 1 xs

theorem List.foldl_hom {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁} (H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) : foldl g₂ (f init) l = f (foldl g₁ init l)

theorem List.foldr_hom {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ : α → β₂ → β₂} {l : List α} {init : β₁} (H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) : foldr g₂ (f init) l = f (foldr g₁ init l)

def List.foldlRecOn {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : β → α → β) {b : β} : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op b a)) → motive (foldl op b l)

A reasoning principle for proving propositions about the result of List.foldl by establishing an invariant that is true for the initial data and preserved by the operation being folded.

Because the motive can return a type in any sort, this function may be used to construct data as well as to prove propositions.

Example:

example {xs : List Nat} : xs.foldl (· + ·) 1 > 0 := by
  apply List.foldlRecOn
  . show 0 < 1; trivial
  . show ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < b + a
    intros; omega

Equations

• List.foldlRecOn [] x✝³ x✝¹ x✝ = x✝¹
• List.foldlRecOn (hd :: tl) x✝³ x✝¹ x✝ = List.foldlRecOn tl x✝³ (x✝ x✝² x✝¹ hd ⋯) fun (y : β) (hy : motive y) (x : α) (hx : x ∈ tl) => x✝ y hy x ⋯

@[simp]

theorem List.foldlRecOn_nil {β : Type u_1} {α : Type u_2} {b : β} {motive : β → Sort u_3} {op : β → α → β} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ [] → motive (op b a)) : foldlRecOn [] op hb hl = hb

@[simp]

theorem List.foldlRecOn_cons {β : Type u_1} {α : Type u_2} {b : β} {x : α} {l : List α} {motive : β → Sort u_3} {op : β → α → β} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ x :: l → motive (op b a)) : foldlRecOn (x :: l) op hb hl = foldlRecOn l op (hl b hb x ⋯) fun (b : β) (c : motive b) (a : α) (m : a ∈ l) => hl b c a ⋯

def List.foldrRecOn {β : Type u_1} {α : Type u_2} {motive : β → Sort u_3} (l : List α) (op : α → β → β) {b : β} : motive b → ((b : β) → motive b → (a : α) → a ∈ l → motive (op a b)) → motive (foldr op b l)

A reasoning principle for proving propositions about the result of List.foldr by establishing an invariant that is true for the initial data and preserved by the operation being folded.

Because the motive can return a type in any sort, this function may be used to construct data as well as to prove propositions.

Example:

example {xs : List Nat} : xs.foldr (· + ·) 1 > 0 := by
  apply List.foldrRecOn
  . show 0 < 1; trivial
  . show ∀ (b : Nat), 0 < b → ∀ (a : Nat), a ∈ xs → 0 < a + b
    intros; omega

Equations

• List.foldrRecOn [] x✝³ x✝¹ x✝ = x✝¹
• List.foldrRecOn (x_5 :: l) x✝³ x✝¹ x✝ = x✝ (List.foldr x✝³ x✝² l) (List.foldrRecOn l x✝³ x✝¹ fun (b : β) (c : motive b) (a : α) (m : a ∈ l) => x✝ b c a ⋯) x_5 ⋯

@[simp]

theorem List.foldrRecOn_nil {β : Type u_1} {α : Type u_2} {b : β} {motive : β → Sort u_3} {op : α → β → β} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ [] → motive (op a b)) : foldrRecOn [] op hb hl = hb

@[simp]

theorem List.foldrRecOn_cons {β : Type u_1} {α : Type u_2} {b : β} {x : α} {l : List α} {motive : β → Sort u_3} {op : α → β → β} (hb : motive b) (hl : (b : β) → motive b → (a : α) → a ∈ x :: l → motive (op a b)) : foldrRecOn (x :: l) op hb hl = hl (foldr op b l) (foldrRecOn l op hb fun (b : β) (c : motive b) (a : α) (m : a ∈ l) => hl b c a ⋯) x ⋯

theorem List.foldl_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop} (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) : r (foldl (fun (acc : β) (a : α) => f acc a) a l) (foldl (fun (acc : γ) (a : α) => g acc a) b l)

We can prove that two folds over the same list are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the list, preserves the relation.

theorem List.foldr_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop} (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) : r (foldr (fun (a : α) (acc : β) => f a acc) a l) (foldr (fun (a : α) (acc : γ) => g a acc) b l)

We can prove that two folds over the same list are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the list, preserves the relation.

@[simp]

theorem List.foldl_add_const {α : Type u_1} {l : List α} {a b : Nat} : foldl (fun (x : Nat) (x_1 : α) => x + a) b l = b + a * l.length

@[simp]

theorem List.foldr_add_const {α : Type u_1} {l : List α} {a b : Nat} : foldr (fun (x : α) (x_1 : Nat) => x_1 + a) b l = b + a * l.length

Further results about getLast and getLast?

@[simp]

theorem List.head_reverse {α : Type u_1} {l : List α} (h : l.reverse ≠ []) : l.reverse.head h = l.getLast ⋯

theorem List.getLast_eq_head_reverse {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h = l.reverse.head ⋯

@[simp]

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

theorem List.getLast?_eq_some_iff {α : Type u_1} {xs : List α} {a : α} : xs.getLast? = some a ↔ ∃ (ys : List α), xs = ys ++ [a]

@[simp]

theorem List.getLast?_isSome {α✝ : Type u_1} {l : List α✝} : l.getLast?.isSome = true ↔ l ≠ []

@[simp]

theorem List.getLast_reverse {α : Type u_1} {l : List α} (h : l.reverse ≠ []) : l.reverse.getLast h = l.head ⋯

theorem List.head_eq_getLast_reverse {α : Type u_1} {l : List α} (h : l ≠ []) : l.head h = l.reverse.getLast ⋯

@[simp]

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

theorem List.getLast_append {α : Type u_1} {l' l : List α} (h : l ++ l' ≠ []) : (l ++ l').getLast h = if h' : l'.isEmpty = true then l.getLast ⋯ else l'.getLast ⋯

theorem List.getLast_append_right {α : Type u_1} {l' l : List α} (h : l' ≠ []) : (l ++ l').getLast ⋯ = l'.getLast h

theorem List.getLast_append_left {α : Type u_1} {l' l : List α} (w : l ++ l' ≠ []) (h : l' = []) : (l ++ l').getLast w = l.getLast ⋯

@[simp]

theorem List.getLast?_append {α : Type u_1} {l l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast?

theorem List.getLast_filter_of_pos {α : Type u_1} {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.getLast w) = true) : (filter p l).getLast ⋯ = l.getLast w

theorem List.getLast_filterMap_of_eq_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (w : l ≠ []) {b : β} (h : f (l.getLast w) = some b) : (filterMap f l).getLast ⋯ = b

theorem List.getLast?_flatMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} : (flatMap f l).getLast? = findSome? (fun (a : α) => (f a).getLast?) l.reverse

theorem List.getLast?_flatten {α : Type u_1} {L : List (List α)} : L.flatten.getLast? = findSome? (fun (l : List α) => l.getLast?) L.reverse

theorem List.getLast?_replicate {α : Type u_1} {a : α} {n : Nat} : (replicate n a).getLast? = if n = 0 then none else some a

@[simp]

theorem List.getLast_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} (w : replicate n a ≠ []) : (replicate n a).getLast w = a

Additional operations

leftpad

theorem List.leftpad_prefix {α : Type u_1} {n : Nat} {a : α} {l : List α} : replicate (n - l.length) a <+: leftpad n a l

theorem List.leftpad_suffix {α : Type u_1} {n : Nat} {a : α} {l : List α} : l <:+ leftpad n a l

List membership

contains / elem

Recall that the preferred simp normal form is contains rather than elem.

theorem List.elem_cons_self {α : Type u_1} {as : List α} [BEq α] [LawfulBEq α] {a : α} : elem a (a :: as) = true

theorem List.contains_eq_any_beq {α : Type u_1} [BEq α] {l : List α} {a : α} : l.contains a = l.any fun (x : α) => a == x

theorem List.contains_iff_exists_mem_beq {α : Type u_1} [BEq α] {l : List α} {a : α} : l.contains a = true ↔ ∃ (a' : α), a' ∈ l ∧ (a == a') = true

@[simp]

theorem List.contains_map {β : Type u_1} {α : Type u_2} [BEq β] {l : List α} {x : β} {f : α → β} : (map f l).contains x = l.any fun (a : α) => x == f a

@[simp]

theorem List.contains_filter {α : Type u_1} [BEq α] {l : List α} {x : α} {p : α → Bool} : (filter p l).contains x = l.any fun (a : α) => x == a && p a

@[simp]

theorem List.contains_filterMap {β : Type u_1} {α : Type u_2} [BEq β] {l : List α} {x : β} {f : α → Option β} : (filterMap f l).contains x = l.any fun (a : α) => Option.any (fun (b : β) => x == b) (f a)

@[simp]

theorem List.contains_append {α : Type u_1} [BEq α] {l₁ l₂ : List α} {x : α} : (l₁ ++ l₂).contains x = (l₁.contains x || l₂.contains x)

@[simp]

theorem List.contains_flatten {α : Type u_1} [BEq α] {l : List (List α)} {x : α} : l.flatten.contains x = l.any fun (l : List α) => l.contains x

@[simp]

theorem List.contains_reverse {α : Type u_1} [BEq α] {l : List α} {x : α} : l.reverse.contains x = l.contains x

@[simp]

theorem List.contains_flatMap {β : Type u_1} {α : Type u_2} [BEq β] {l : List α} {f : α → List β} {x : β} : (flatMap f l).contains x = l.any fun (a : α) => (f a).contains x

Sublists

partition

Because we immediately simplify partition into two filters for verification purposes, we do not separately develop much theory about it.

@[simp]

theorem List.partition_eq_filter_filter {α : Type u_1} {p : α → Bool} {l : List α} : partition p l = (filter p l, filter (not ∘ p) l)

theorem List.mem_partition {α✝ : Type u_1} {l : List α✝} {a : α✝} {p : α✝ → Bool} : a ∈ l ↔ a ∈ (partition p l).fst ∨ a ∈ (partition p l).snd

dropLast

dropLast is the specification for Array.pop, so theorems about List.dropLast are often used for theorems about Array.pop.

@[simp]

theorem List.length_dropLast {α : Type u_1} {xs : List α} : xs.dropLast.length = xs.length - 1

@[simp]

theorem List.getElem_dropLast {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.dropLast.length) : xs.dropLast[i] = xs[i]

theorem List.getElem?_dropLast {α : Type u_1} {xs : List α} {i : Nat} : xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none

theorem List.head_dropLast {α : Type u_1} {xs : List α} (h : xs.dropLast ≠ []) : xs.dropLast.head h = xs.head ⋯

theorem List.head?_dropLast {α : Type u_1} {xs : List α} : xs.dropLast.head? = if 1 < xs.length then xs.head? else none

theorem List.getLast_dropLast {α : Type u_1} {xs : List α} (h : xs.dropLast ≠ []) : xs.dropLast.getLast h = xs[xs.length - 2]

theorem List.getLast?_dropLast {α : Type u_1} {xs : List α} : xs.dropLast.getLast? = if xs.length ≤ 1 then none else xs[xs.length - 2]?

theorem List.dropLast_cons_of_ne_nil {α : Type u} {x : α} {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast

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

@[simp]

theorem List.map_dropLast {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : map f l.dropLast = (map f l).dropLast

@[simp]

theorem List.dropLast_append_of_ne_nil {α : Type u} {l l' : List α} : l ≠ [] → (l' ++ l).dropLast = l' ++ l.dropLast

theorem List.dropLast_append {α : Type u_1} {l₁ l₂ : List α} : (l₁ ++ l₂).dropLast = if l₂.isEmpty = true then l₁.dropLast else l₁ ++ l₂.dropLast

theorem List.dropLast_append_cons {α✝ : Type u_1} {l₁ : List α✝} {b : α✝} {l₂ : List α✝} : (l₁ ++ b :: l₂).dropLast = l₁ ++ (b :: l₂).dropLast

@[simp]

theorem List.dropLast_concat {α✝ : Type u_1} {l₁ : List α✝} {b : α✝} : (l₁ ++ [b]).dropLast = l₁

@[simp]

theorem List.dropLast_replicate {α : Type u_1} {n : Nat} {a : α} : (replicate n a).dropLast = replicate (n - 1) a

@[simp]

theorem List.dropLast_cons_self_replicate {α : Type u_1} {n : Nat} {a : α} : (a :: replicate n a).dropLast = replicate n a

@[simp]

theorem List.tail_reverse {α : Type u_1} {l : List α} : l.reverse.tail = l.dropLast.reverse

splitAt

We don't provide any API for splitAt, beyond the @[simp] lemma splitAt n l = (l.take n, l.drop n), which is proved in Init.Data.List.TakeDrop.

theorem List.splitAt_go {α : Type u_1} {xs : List α} {i : Nat} {l acc : List α} : splitAt.go l xs i acc = if i < xs.length then (acc.reverse ++ take i xs, drop i xs) else (l, [])

Logic

any / all

theorem List.not_any_eq_all_not {α : Type u_1} {l : List α} {p : α → Bool} : (!l.any p) = l.all fun (a : α) => !p a

theorem List.not_all_eq_any_not {α : Type u_1} {l : List α} {p : α → Bool} : (!l.all p) = l.any fun (a : α) => !p a

theorem List.and_any_distrib_left {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool} : (q && l.any p) = l.any fun (a : α) => q && p a

theorem List.and_any_distrib_right {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool} : (l.any p && q) = l.any fun (a : α) => p a && q

theorem List.or_all_distrib_left {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool} : (q || l.all p) = l.all fun (a : α) => q || p a

theorem List.or_all_distrib_right {α : Type u_1} {l : List α} {p : α → Bool} {q : Bool} : (l.all p || q) = l.all fun (a : α) => p a || q

theorem List.any_eq_not_all_not {α : Type u_1} {l : List α} {p : α → Bool} : l.any p = !l.all fun (x : α) => !p x

theorem List.all_eq_not_any_not {α : Type u_1} {l : List α} {p : α → Bool} : l.all p = !l.any fun (x : α) => !p x

@[simp]

theorem List.any_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {p : β → Bool} : (map f l).any p = l.any (p ∘ f)

@[simp]

theorem List.all_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {p : β → Bool} : (map f l).all p = l.all (p ∘ f)

@[simp]

theorem List.any_filter {α : Type u_1} {l : List α} {p q : α → Bool} : (filter p l).any q = l.any fun (a : α) => p a && q a

@[simp]

theorem List.all_filter {α : Type u_1} {l : List α} {p q : α → Bool} : (filter p l).all q = l.all fun (a : α) => !p a || q a

@[simp]

theorem List.any_filterMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β} {p : β → Bool} : (filterMap f l).any p = l.any fun (a : α) => match f a with | some b => p b | none => false

@[simp]

theorem List.all_filterMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β} {p : β → Bool} : (filterMap f l).all p = l.all fun (a : α) => match f a with | some b => p b | none => true

@[simp]

theorem List.any_append {α : Type u_1} {f : α → Bool} {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f)

@[simp]

theorem List.all_append {α : Type u_1} {f : α → Bool} {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f)

@[simp]

theorem List.any_flatten {α : Type u_1} {f : α → Bool} {l : List (List α)} : l.flatten.any f = l.any fun (x : List α) => x.any f

@[simp]

theorem List.all_flatten {α : Type u_1} {f : α → Bool} {l : List (List α)} : l.flatten.all f = l.all fun (x : List α) => x.all f

@[simp]

theorem List.any_flatMap {α : Type u_1} {β : Type u_2} {p : β → Bool} {l : List α} {f : α → List β} : (flatMap f l).any p = l.any fun (a : α) => (f a).any p

@[simp]

theorem List.all_flatMap {α : Type u_1} {β : Type u_2} {p : β → Bool} {l : List α} {f : α → List β} : (flatMap f l).all p = l.all fun (a : α) => (f a).all p

@[simp]

theorem List.any_reverse {α : Type u_1} {f : α → Bool} {l : List α} : l.reverse.any f = l.any f

@[simp]

theorem List.all_reverse {α : Type u_1} {f : α → Bool} {l : List α} : l.reverse.all f = l.all f

@[simp]

theorem List.any_replicate {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (replicate n a).any f = if n = 0 then false else f a

@[simp]

theorem List.all_replicate {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (replicate n a).all f = if n = 0 then true else f a

theorem List.any_congr {α : Type u_1} {l₁ l₂ : List α} (w : l₁ = l₂) {p q : α → Bool} (h : ∀ (a : α), p a = q a) : l₁.any p = l₂.any q

theorem List.all_congr {α : Type u_1} {l₁ l₂ : List α} (w : l₁ = l₂) {p q : α → Bool} (h : ∀ (a : α), p a = q a) : l₁.all p = l₂.all q

theorem List.contains_congr {α : Type u_1} [BEq α] [PartialEquivBEq α] {l : List α} {x y : α} (h : (x == y) = true) : l.contains x = l.contains y

Manipulating elements

replace

@[simp]

theorem List.replace_cons_self {α : Type u_1} [BEq α] {as : List α} {b : α} [LawfulBEq α] {a : α} : (a :: as).replace a b = b :: as

@[simp]

theorem List.replace_singleton {α : Type u_1} [BEq α] {a b c : α} : [a].replace b c = [if (b == a) = true then c else a]

@[simp]

theorem List.replace_of_not_mem {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l : List α} (h : ¬a ∈ l) : l.replace a b = l

@[simp]

theorem List.length_replace {α : Type u_1} [BEq α] {a b : α} {l : List α} : (l.replace a b).length = l.length

theorem List.getElem?_replace {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l : List α} {i : Nat} : (l.replace a b)[i]? = if (l[i]? == some a) = true then if a ∈ take i l then some a else some b else l[i]?

theorem List.getElem?_replace_of_ne {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l : List α} {i : Nat} (h : l[i]? ≠ some a) : (l.replace a b)[i]? = l[i]?

theorem List.getElem_replace {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l : List α} {i : Nat} (h : i < l.length) : (l.replace a b)[i] = if (l[i] == a) = true then if a ∈ take i l then a else b else l[i]

theorem List.getElem_replace_of_ne {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l : List α} {i : Nat} {h : i < l.length} (h' : l[i] ≠ a) : (l.replace a b)[i] = l[i]

theorem List.head?_replace {α : Type u_1} [BEq α] {l : List α} {a b : α} : (l.replace a b).head? = match l.head? with | none => none | some x => some (if (a == x) = true then b else x)

theorem List.head_replace {α : Type u_1} [BEq α] {l : List α} {a b : α} (w : l.replace a b ≠ []) : (l.replace a b).head w = if (a == l.head ⋯) = true then b else l.head ⋯

theorem List.replace_append {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l₁ l₂ : List α} : (l₁ ++ l₂).replace a b = if a ∈ l₁ then l₁.replace a b ++ l₂ else l₁ ++ l₂.replace a b

theorem List.replace_append_left {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l₁ l₂ : List α} (h : a ∈ l₁) : (l₁ ++ l₂).replace a b = l₁.replace a b ++ l₂

theorem List.replace_append_right {α : Type u_1} [BEq α] {a b : α} [LawfulBEq α] {l₁ l₂ : List α} (h : ¬a ∈ l₁) : (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b

theorem List.replace_take {α : Type u_1} [BEq α] {a b : α} {l : List α} {i : Nat} : (take i l).replace a b = take i (l.replace a b)

@[simp]

theorem List.replace_replicate_self {α : Type u_1} [BEq α] {n : Nat} {b : α} [LawfulBEq α] {a : α} (h : 0 < n) : (replicate n a).replace a b = b :: replicate (n - 1) a

@[simp]

theorem List.replace_replicate_ne {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a b c : α} (h : (!b == a) = true) : (replicate n a).replace b c = replicate n a

insert

@[simp]

theorem List.insert_nil {α : Type u_1} [BEq α] (a : α) : List.insert a [] = [a]

@[simp]

theorem List.contains_insert {α : Type u_1} [BEq α] [PartialEquivBEq α] {l : List α} {a x : α} : (List.insert a l).contains x = (x == a || l.contains x)

@[simp]

theorem List.insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : List.insert a l = l

@[simp]

theorem List.insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) : List.insert a l = a :: l

@[simp]

theorem List.mem_insert_iff {α : Type u_1} [BEq α] [LawfulBEq α] {b a : α} {l : List α} : a ∈ List.insert b l ↔ a = b ∨ a ∈ l

theorem List.mem_insert_self {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : a ∈ List.insert a l

theorem List.mem_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {l : List α} (h : a ∈ l) : a ∈ List.insert b l

theorem List.eq_or_mem_of_mem_insert {α : Type u_1} [BEq α] [LawfulBEq α] {b a : α} {l : List α} (h : a ∈ List.insert b l) : a = b ∨ a ∈ l

@[simp]

theorem List.length_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : (List.insert a l).length = l.length

@[simp]

theorem List.length_insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) : (List.insert a l).length = l.length + 1

theorem List.length_insert {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : (List.insert a l).length = l.length + if a ∈ l then 0 else 1

theorem List.length_le_length_insert {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : l.length ≤ (List.insert a l).length

theorem List.length_insert_pos {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : 0 < (List.insert a l).length

theorem List.insert_eq {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : List.insert a l = if a ∈ l then l else a :: l

theorem List.getElem?_insert_zero {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : (List.insert a l)[0]? = if a ∈ l then l[0]? else some a

theorem List.getElem?_insert_succ {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} : (List.insert a l)[i + 1]? = if a ∈ l then l[i + 1]? else l[i]?

theorem List.getElem?_insert {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} : (List.insert a l)[i]? = if a ∈ l then l[i]? else if i = 0 then some a else l[i - 1]?

theorem List.getElem_insert {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} (h : i < l.length) : (List.insert a l)[i] = if a ∈ l then l[i] else if i = 0 then a else l[i - 1]

theorem List.head?_insert {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : (List.insert a l).head? = some (if h : a ∈ l then l.head ⋯ else a)

theorem List.head_insert {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} (w : List.insert a l ≠ []) : (List.insert a l).head w = if h : a ∈ l then l.head ⋯ else a

theorem List.insert_append {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} : List.insert a (l₁ ++ l₂) = if a ∈ l₂ then l₁ ++ l₂ else List.insert a l₁ ++ l₂

theorem List.insert_append_of_mem_left {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} (h : a ∈ l₂) : List.insert a (l₁ ++ l₂) = l₁ ++ l₂

theorem List.insert_append_of_not_mem_left {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α} (h : ¬a ∈ l₂) : List.insert a (l₁ ++ l₂) = List.insert a l₁ ++ l₂

@[simp]

theorem List.insert_replicate_self {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a : α} (h : 0 < n) : List.insert a (replicate n a) = replicate n a

@[simp]

theorem List.insert_replicate_ne {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} (h : (!b == a) = true) : List.insert b (replicate n a) = b :: replicate n a

@[simp]

theorem List.any_insert {α : Type u_1} [BEq α] [LawfulBEq α] {f : α → Bool} {l : List α} {a : α} : (List.insert a l).any f = (f a || l.any f)

@[simp]

theorem List.all_insert {α : Type u_1} [BEq α] [LawfulBEq α] {f : α → Bool} {l : List α} {a : α} : (List.insert a l).all f = (f a && l.all f)

removeAll

@[simp]

theorem List.removeAll_nil {α : Type u_1} [BEq α] {xs : List α} : xs.removeAll [] = xs

theorem List.cons_removeAll {α : Type u_1} [BEq α] {x : α} {xs ys : List α} : (x :: xs).removeAll ys = if ys.contains x = false then x :: xs.removeAll ys else xs.removeAll ys

theorem List.removeAll_cons {α : Type u_1} [BEq α] {xs : List α} {y : α} {ys : List α} : xs.removeAll (y :: ys) = (filter (fun (x : α) => !x == y) xs).removeAll ys

@[simp]

theorem List.filter_removeAll_filter {α : Type u_1} [BEq α] [LawfulBEq α] {p : α → Bool} {xs ys : List α} : (filter p xs).removeAll (filter p ys) = (filter p xs).removeAll ys

eraseDupsBy and eraseDups

@[simp]

theorem List.eraseDupsBy_nil {α : Type u_1} {r : α → α → Bool} : eraseDupsBy r [] = []

theorem List.eraseDupsBy_cons {α✝ : Type u_1} {a : α✝} {as : List α✝} {r : α✝ → α✝ → Bool} : eraseDupsBy r (a :: as) = a :: eraseDupsBy r (filter (fun (b : α✝) => decide (r b a = false)) as)

@[simp]

theorem List.eraseDups_nil {α : Type u_1} [BEq α] : [].eraseDups = []

theorem List.eraseDups_cons {α : Type u_1} [BEq α] {a : α} {as : List α} : (a :: as).eraseDups = a :: (filter (fun (b : α) => !b == a) as).eraseDups

theorem List.eraseDups_append {α : Type u_1} [BEq α] [LawfulBEq α] {as bs : List α} : (as ++ bs).eraseDups = as.eraseDups ++ (bs.removeAll as).eraseDups

@[simp]

theorem List.mem_eraseDups {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : a ∈ l.eraseDups ↔ a ∈ l

Membership is preserved by eraseDups: an element is in the deduplicated list iff it was in the original list.

Legacy lemmas about get, get?, and get!.

Hopefully these should not be needed, in favour of lemmas about xs[i], xs[i]?, and xs[i]!, to which these simplify.

We may consider deprecating or downstreaming these lemmas.

theorem List.get_cons_zero {α✝ : Type u_1} {a : α✝} {l : List α✝} : (a :: l).get 0 = a

theorem List.get_cons_succ {α : Type u_1} {i : Nat} {a : α} {as : List α} {h : i + 1 < (a :: as).length} : (a :: as).get ⟨i + 1, h⟩ = as.get ⟨i, ⋯⟩

theorem List.get_cons_succ' {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} : (a :: as).get i.succ = as.get i

theorem List.get_mk_zero {α : Type u_1} {l : List α} (h : 0 < l.length) : l.get ⟨0, h⟩ = l.head ⋯

theorem List.get_of_eq {α : Type u_1} {l l' : List α} (h : l = l') (i : Fin l.length) : l.get i = l'.get ⟨↑i, ⋯⟩

If one has l.get i in an expression (with i : Fin l.length) and h : l = l', rw [h] will give a "motive is not type correct" error, as it cannot rewrite the i : Fin l.length to Fin l'.length directly. The theorem get_of_eq can be used to make such a rewrite, with rw [get_of_eq h].

theorem List.getElem!_nil {α : Type u_1} [Inhabited α] {n : Nat} : [][n]! = default

theorem List.getElem!_cons_zero {α : Type u_1} {a : α} [Inhabited α] {l : List α} : (a :: l)[0]! = a

theorem List.getElem!_cons_succ {α : Type u_1} {a : α} {i : Nat} [Inhabited α] {l : List α} : (a :: l)[i + 1]! = l[i]!

theorem List.getElem!_of_getElem? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {i : Nat} : l[i]? = some a → l[i]! = a

theorem List.ext_get {α : Type u_1} {l₁ l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) : l₁ = l₂

theorem List.get_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ (n : Fin l.length), l.get n = a

theorem List.get_mem {α : Type u_1} (l : List α) (n : Fin l.length) : l.get n ∈ l

theorem List.mem_iff_get {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : Fin l.length), l.get n = a

intercalate

@[simp]

theorem List.intercalate_nil {α : Type u_1} {ys : List α} : ys.intercalate [] = []

@[simp]

theorem List.intercalate_singleton {α : Type u_1} {ys xs : List α} : ys.intercalate [xs] = xs

@[simp]

theorem List.intercalate_cons_cons {α : Type u_1} {ys l l' : List α} {zs : List (List α)} : ys.intercalate (l :: l' :: zs) = l ++ ys ++ ys.intercalate (l' :: zs)

@[simp]

theorem List.intercalate_cons_cons_left {α : Type u_1} {ys l : List α} {x : α} {zs : List (List α)} : ys.intercalate ((x :: l) :: zs) = x :: ys.intercalate (l :: zs)

theorem List.intercalate_cons_of_ne_nil {α : Type u_1} {ys l : List α} {zs : List (List α)} (h : zs ≠ []) : ys.intercalate (l :: zs) = l ++ ys ++ ys.intercalate zs