Documentation

Init.Data.List.Lemmas

Theorems about List operations. #

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

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:

See also

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

Also

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 = 0l = []
theorem List.ne_nil_of_length_eq_add_one {α✝ : Type u_1} {l : List α✝} {n : Nat} :
l.length = n + 1l []
theorem List.ne_nil_of_length_pos {α✝ : Type u_1} {l : List α✝} :
0 < l.lengthl []
@[simp]
theorem List.length_eq_zero {α✝ : Type u_1} {l : List α✝} :
l.length = 0 l = []
theorem List.length_pos_of_mem {α : Type u_1} {a : α} {l : List α} :
a l0 < 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 {α : Type u_1} {l : List α} :
0 < l.length l []
theorem List.length_eq_one {α : 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]
theorem List.get?_eq_none {α : Type u_1} {l : List α} {n : Nat} :
l.length nl.get? n = none
theorem List.get?_eq_get {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) :
l.get? n = some (l.get n, h)
theorem List.get?_eq_some_iff {α✝ : Type u_1} {a : α✝} {l : List α✝} {n : Nat} :
l.get? n = some a (h : n < l.length), l.get n, h = a
theorem List.get?_eq_none_iff {α✝ : Type u_1} {l : List α✝} {n : Nat} :
@[simp]
theorem List.get?_eq_getElem? {α : Type u_1} (l : List α) (i : Nat) :
l.get? i = l[i]?

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

get! #

We simplify l.get! i to l[i]!.

theorem List.get!_eq_getD {α : Type u_1} [Inhabited α] (l : List α) (i : Nat) :
l.get! i = l.getD i default
@[simp]
theorem List.get!_eq_getElem! {α : Type u_1} [Inhabited α] (l : List α) (i : Nat) :
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) :

getElem? and getElem #

@[simp]
theorem List.getElem?_eq_none_iff {α✝ : Type u_1} {l : List α✝} {i : Nat} :
@[simp]
theorem List.none_eq_getElem?_iff {α : Type u_1} {l : List α} {i : Nat} :
theorem List.getElem?_eq_none {α✝ : Type u_1} {l : List α✝} {i : Nat} (h : l.length i) :
@[simp]
theorem List.getElem?_eq_getElem {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) :
l[i]? = some l[i]
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.some_eq_getElem?_iff {α : Type u_1} {a : α} {i : Nat} {l : List α} :
some a = l[i]? (h : i < l.length), l[i] = a
@[simp]
theorem List.some_getElem_eq_getElem?_iff {α : Type u_1} (xs : List α) (i : Nat) (h : i < xs.length) :
@[simp]
theorem List.getElem?_eq_some_getElem_iff {α : Type u_1} (xs : List α) (i : Nat) (h : i < xs.length) :
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.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?_nil {α : Type u_1} {i : Nat} :
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 {α✝ : outParam (Type u_1)} {a : α✝} {l : List α✝} {i : Nat} :
(a :: l)[i]? = if i = 0 then some a else l[i - 1]?
@[simp]
theorem List.getElem_singleton {α : Type u_1} {i : Nat} (a : α) (h : i < 1) :
[a][i] = a
theorem List.getElem?_singleton {α : Type u_1} (a : α) (i : Nat) :
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 {α : 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₂
@[simp]
theorem List.getElem_concat_length {α : Type u_1} (l : List α) (a : α) (i : Nat) :
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

mem #

@[simp]
theorem List.not_mem_nil {α : Type u_1} (a : α) :
@[simp]
theorem List.mem_cons {α✝ : Type u_1} {b : α✝} {l : List α✝} {a : α✝} :
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 la 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 : ¬pList α} :
(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 : pList α} :
(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
@[simp]
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 :: lp x) p a ∀ (x : α), x lp 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 : α) :
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 :: lb la 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) :
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 :: la 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 :: la 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) :
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.forall_getElem {α : Type u_1} {l : List α} {p : αProp} :
(∀ (i : Nat) (h : i < l.length), p l[i]) ∀ (a : α), a lp 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 {α : 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 #

theorem List.isEmpty_iff {α : Type u_1} {l : List α} :
theorem List.isEmpty_eq_false_iff_exists_mem {α : Type u_1} {xs : List α} :
xs.isEmpty = false (x : α), x xs
@[simp]
theorem List.isEmpty_eq_true {α : Type u_1} {l : List α} :
@[simp]
theorem List.isEmpty_eq_false {α : Type u_1} {l : List α} :

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 lp 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 lp 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 lp 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} (n : Nat) (a : α) :
[].set n 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 α) (n : Nat) (a : α) :
(x :: xs).set (n + 1) a = x :: xs.set n 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 α} {n : Nat} (h : l.length n) {a : α} :
l.set n a = l
@[simp]
theorem List.set_eq_nil_iff {α : Type u_1} {l : List α} (n : Nat) (a : α) :
l.set n a = [] l = []
theorem List.set_comm {α : Type u_1} (a b : α) {n m : Nat} (l : List α) :
n m(l.set n a).set m b = (l.set m b).set n a
@[simp]
theorem List.set_set {α : Type u_1} (a b : α) (l : List α) (n : Nat) :
(l.set n a).set n b = l.set n b
theorem List.mem_set {α : Type u_1} (l : List α) (n : Nat) (h : n < l.length) (a : α) :
a l.set n a
theorem List.mem_or_eq_of_mem_set {α : Type u_1} {l : List α} {n : Nat} {a b : α} :
a l.set n ba l a = b

BEq #

@[simp]
theorem List.beq_nil_iff {α : Type u_1} [BEq α] {l : List α} :
(l == []) = l.isEmpty
@[simp]
theorem List.nil_beq_iff {α : Type u_1} [BEq α] {l : List α} :
([] == l) = l.isEmpty
@[simp]
theorem List.cons_beq_cons {α : Type u_1} [BEq α] {a b : α} {l₁ l₂ : List α} :
(a :: l₁ == b :: l₂) = (a == b && l₁ == l₂)
@[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, irreducible]
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 α] :
@[simp]
theorem List.lawfulBEq_iff {α : Type u_1} [BEq α] :

isEqv #

@[simp]
theorem List.isEqv_eq {α : Type u_1} [DecidableEq α] {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
@[deprecated List.getLast_eq_getElem (since := "2024-07-15")]
theorem List.getLast_eq_get {α : Type u_1} (l : List α) (h : l []) :
l.getLast h = l.get l.length - 1,
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 α) :
@[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 []) :
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 : α) :
theorem List.getLast?_eq_getLast {α : Type u_1} (l : List α) (h : l []) :
theorem List.getLast?_eq_getElem? {α : Type u_1} (l : List α) :
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 : α} :
@[simp]
theorem List.getLast?_cons_cons {α✝ : Type u_1} {a b : α✝} {l : List α✝} :
(a :: b :: l).getLast? = (b :: l).getLast?
@[deprecated List.getLast?_eq_getElem? (since := "2024-07-07")]
theorem List.getLast?_eq_get? {α : Type u_1} (l : List α) :
l.getLast? = l.get? (l.length - 1)
theorem List.getLast?_concat {α : Type u_1} {a : α} (l : List α) :
theorem List.getLastD_concat {α : Type u_1} (a b : α) (l : List α) :
(l ++ [b]).getLastD a = b

getLast! #

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

Head and tail #

theorem List.head?_singleton {α : Type u_1} (a : α) :
theorem List.head!_of_head? {α : Type u_1} {a : α} [Inhabited α] {l : List α} :
l.head? = some al.head! = a
theorem List.head?_eq_head {α : Type u_1} {l : List α} (h : l []) :
l.head? = some (l.head h)
theorem List.head?_eq_getElem? {α : Type u_1} (l : List α) :
l.head? = l[0]?
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_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 α✝} :
theorem List.head?_eq_some_iff {α : Type u_1} {xs : List α} {a : α} :
xs.head? = some a (ys : List α), xs = a :: ys
@[simp]
theorem List.head?_isSome {α✝ : Type u_1} {l : List α✝} :
@[simp]
theorem List.head_mem {α : Type u_1} {l : List α} (h : l []) :
l.head h 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?_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?

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 α) :
theorem List.tail_eq_tailD {α : Type u_1} (l : List α) :
theorem List.tail_eq_tail? {α : Type u_1} (l : List α) :
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 α) :
@[simp]
theorem List.getLast_tail {α : Type u_1} (l : List α) (h : l.tail []) :
l.tail.getLast h = l.getLast

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.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} :
@[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 lP i) ∀ (j : α), j lP (f j)
@[reducible, inline, deprecated List.forall_mem_map (since := "2024-07-25")]
abbrev List.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {P : βProp} :
(∀ (i : β), i map f lP i) ∀ (j : α), j lP (f j)
Equations
Instances For
    @[simp]
    theorem List.map_eq_nil_iff {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} :
    map f l = [] l = []
    @[reducible, inline, deprecated List.map_eq_nil_iff (since := "2024-09-05")]
    abbrev List.map_eq_nil {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} :
    map f l = [] l = []
    Equations
    Instances For
      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 lf a = g a
      theorem List.map_inj_right {α : Type u_1} {β : Type u_2} {l l' : List α} {f : αβ} (w : ∀ (x y : α), f x = f yx = 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 lf 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₂
      @[reducible, inline, deprecated List.map_eq_cons_iff (since := "2024-09-05")]
      abbrev List.map_eq_cons {α : 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₂
      Equations
      Instances For
        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₂
        @[reducible, inline, deprecated List.map_eq_cons' (since := "2024-09-05")]
        abbrev List.map_eq_cons' {α : 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₂
        Equations
        Instances For
          @[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 lf 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)
          @[deprecated "Use the reverse direction of `map_set`." (since := "2024-09-20")]
          theorem List.set_map {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {n : Nat} {a : α} :
          (map f l).set n (f a) = map f (l.set n 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 α) :
          @[simp]
          theorem List.map_tail? {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
          @[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 α) :
          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 α) :
          @[simp]
          theorem List.filter_eq_self {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} :
          filter p l = l ∀ (a : α✝), a lp a = true
          @[simp]
          theorem List.filter_length_eq_length {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} :
          (filter p l).length = l.length ∀ (a : α✝), a lp 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
          @[reducible, inline, deprecated List.filter_eq_nil_iff (since := "2024-09-05")]
          abbrev List.filter_eq_nil {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} :
          filter p l = [] ∀ (a : α✝), a l¬p a = true
          Equations
          Instances For
            theorem List.forall_mem_filter {α : Type u_1} {l : List α} {p : αBool} {P : αProp} :
            (∀ (i : α), i filter p lP i) ∀ (j : α), j lp j = trueP j
            @[reducible, inline, deprecated List.forall_mem_filter (since := "2024-07-25")]
            abbrev List.forall_mem_filter_iff {α : Type u_1} {l : List α} {p : αBool} {P : αProp} :
            (∀ (i : α), i filter p lP i) ∀ (j : α), j lp j = trueP j
            Equations
            Instances For
              @[simp]
              theorem List.filter_filter {α✝ : Type u_1} {p : α✝Bool} (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.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} {p : αBool} (f : βα) (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 β) => bif p a 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
              @[reducible, inline, deprecated List.filter_eq_cons_iff (since := "2024-09-05")]
              abbrev List.filter_eq_cons {α✝ : 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
              Equations
              Instances For
                theorem List.filter_congr {α : Type u_1} {p q : αBool} {l : List α} :
                (∀ (x : α), x lp 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 : αβ) :
                @[simp]
                theorem List.filterMap_some {α : Type u_1} (l : List α) :
                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 α) :
                @[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 = true) = 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 lP i) ∀ (j : α), j l∀ (b : β), f j = some bP b
                @[reducible, inline, deprecated List.forall_mem_filterMap (since := "2024-07-25")]
                abbrev List.forall_mem_filterMap_iff {α : Type u_1} {β : Type u_2} {f : αOption β} {l : List α} {P : βProp} :
                (∀ (i : β), i filterMap f lP i) ∀ (j : α), j l∀ (b : β), f j = some bP b
                Equations
                Instances For
                  @[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 xsf x = none
                  @[simp]
                  theorem List.filterMap_eq_nil_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝Option α✝¹} {l : List α✝} :
                  filterMap f l = [] ∀ (a : α✝), a lf a = none
                  @[reducible, inline, deprecated List.filterMap_eq_nil_iff (since := "2024-09-05")]
                  abbrev List.filterMap_eq_nil {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝Option α✝¹} {l : List α✝} :
                  filterMap f l = [] ∀ (a : α✝), a lf a = none
                  Equations
                  Instances For
                    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
                    @[reducible, inline, deprecated List.filterMap_eq_cons_iff (since := "2024-09-05")]
                    abbrev List.filterMap_eq_cons {α✝ : 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
                    Equations
                    Instances For

                      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
                      @[deprecated List.mem_append (since := "2025-01-13")]
                      theorem List.mem_append_eq {α : Type u_1} (a : α) (s t : List α) :
                      (a s ++ t) = (a s a t)
                      @[reducible, inline, deprecated List.mem_append_left (since := "2024-11-20")]
                      abbrev List.mem_append_of_mem_left {α : Type u_1} {a : α} {as : List α} (bs : List α) :
                      a asa as ++ bs
                      Equations
                      Instances For
                        @[reducible, inline, deprecated List.mem_append_right (since := "2024-11-20")]
                        abbrev List.mem_append_of_mem_right {α : Type u_1} {b : α} {bs : List α} (as : List α) :
                        b bsb as ++ bs
                        Equations
                        Instances For
                          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 α) {l₁ : List α} {i : Nat} (hi : i < l₁.length) :
                          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₂.lengths₁ = 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} {x y : List α} :
                          x ++ y = y x = []
                          @[simp]
                          theorem List.self_eq_append_left {α : Type u_1} {x y : List α} :
                          y = x ++ y x = []
                          @[simp]
                          theorem List.append_right_eq_self {α : Type u_1} {x y : List α} :
                          x ++ y = x y = []
                          @[simp]
                          theorem List.self_eq_append_right {α : Type u_1} {x y : List α} :
                          x = x ++ y y = []
                          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 = []
                          @[reducible, inline, deprecated List.append_eq_nil_iff (since := "2025-01-13")]
                          abbrev List.append_eq_nil {α✝ : Type u_1} {p q : List α✝} :
                          p ++ q = [] p = [] q = []
                          Equations
                          Instances For
                            @[simp]
                            theorem List.nil_eq_append_iff {α✝ : Type u_1} {a b : List α✝} :
                            [] = a ++ b a = [] b = []
                            @[reducible, inline, deprecated List.nil_eq_append_iff (since := "2024-07-24")]
                            abbrev List.nil_eq_append {α✝ : Type u_1} {a b : List α✝} :
                            [] = a ++ b a = [] b = []
                            Equations
                            Instances For
                              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 []
                              @[deprecated List.append_ne_nil_of_left_ne_nil (since := "2024-07-24")]
                              theorem List.append_ne_nil_of_ne_nil_left {α : Type u_1} {s : List α} (h : s []) (t : List α) :
                              s ++ t []
                              @[deprecated List.append_ne_nil_of_right_ne_nil (since := "2024-07-24")]
                              theorem List.append_ne_nil_of_ne_nil_right {α : Type u_1} {t : List α} (s : List α) :
                              t []s ++ t []
                              theorem List.append_eq_cons_iff {α✝ : Type u_1} {a b : List α✝} {x : α✝} {c : List α✝} :
                              a ++ b = x :: c a = [] b = x :: c (a' : List α✝), a = x :: a' c = a' ++ b
                              @[reducible, inline, deprecated List.append_eq_cons_iff (since := "2024-07-24")]
                              abbrev List.append_eq_cons {α✝ : Type u_1} {a b : List α✝} {x : α✝} {c : List α✝} :
                              a ++ b = x :: c a = [] b = x :: c (a' : List α✝), a = x :: a' c = a' ++ b
                              Equations
                              Instances For
                                theorem List.cons_eq_append_iff {α✝ : Type u_1} {x : α✝} {c a b : List α✝} :
                                x :: c = a ++ b a = [] b = x :: c (a' : List α✝), a = x :: a' c = a' ++ b
                                @[reducible, inline, deprecated List.cons_eq_append_iff (since := "2024-07-24")]
                                abbrev List.cons_eq_append {α✝ : Type u_1} {x : α✝} {c a b : List α✝} :
                                x :: c = a ++ b a = [] b = x :: c (a' : List α✝), a = x :: a' c = a' ++ b
                                Equations
                                Instances For
                                  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} {a b c d : List α} :
                                  a ++ b = c ++ d ( (a' : List α), c = a ++ a' b = a' ++ d) (c' : List α), a = c ++ c' d = c' ++ b
                                  @[reducible, inline, deprecated List.append_inj (since := "2024-07-24")]
                                  abbrev List.append_inj_of_length_left {α : Type u_1} {s₁ s₂ t₁ t₂ : List α} :
                                  s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengths₁ = s₂ t₁ = t₂
                                  Equations
                                  Instances For
                                    @[reducible, inline, deprecated List.append_inj' (since := "2024-07-24")]
                                    abbrev List.append_inj_of_length_right {α✝ : Type u_1} {s₁ t₁ s₂ t₂ : List α✝} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) :
                                    s₁ = s₂ t₁ = t₂
                                    Equations
                                    Instances For
                                      @[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
                                      @[reducible, inline, deprecated List.tail_append_of_ne_nil (since := "2024-07-24")]
                                      abbrev List.tail_append_left {α : Type u_1} {xs ys : List α} (h : xs []) :
                                      (xs ++ ys).tail = xs.tail ++ ys
                                      Equations
                                      Instances For
                                        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₂
                                        @[reducible, inline, deprecated List.filterMap_eq_append_iff (since := "2024-09-05")]
                                        abbrev List.filterMap_eq_append {α : 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₂
                                        Equations
                                        Instances For
                                          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₂
                                          @[reducible, inline, deprecated List.append_eq_filterMap (since := "2024-09-05")]
                                          abbrev List.append_eq_filterMap {α : 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₂
                                          Equations
                                          Instances For
                                            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₂
                                            @[reducible, inline, deprecated List.append_eq_filter_iff (since := "2024-09-05")]
                                            abbrev List.append_eq_filter {α : 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₂
                                            Equations
                                            Instances For
                                              @[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₂
                                              @[reducible, inline, deprecated List.map_eq_append_iff (since := "2024-09-05")]
                                              abbrev List.map_eq_append {α : 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₂
                                              Equations
                                              Instances For
                                                @[reducible, inline, deprecated List.append_eq_map_iff (since := "2024-09-05")]
                                                abbrev List.append_eq_map {α : 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₂
                                                Equations
                                                Instances For

                                                  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 : α) :
                                                  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 bl₁ = l₂
                                                  theorem List.last_eq_of_concat_eq {α : Type u_1} {a b : α} {l₁ l₂ : List α} :
                                                  l₁.concat a = l₂.concat ba = 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'
                                                  @[reducible, inline, deprecated List.concat_inj (since := "2024-09-05")]
                                                  abbrev List.concat_eq_concat {α : Type u_1} {a b : α} {l l' : List α} :
                                                  l.concat a = l'.concat b l = l' a = b
                                                  Equations
                                                  Instances For
                                                    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 α)) :
                                                    theorem List.flatten_singleton {α : Type u_1} (l : List α) :
                                                    @[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 Ll = []
                                                    @[simp]
                                                    theorem List.nil_eq_flatten_iff {α : Type u_1} {L : List (List α)} :
                                                    [] = L.flatten ∀ (l : List α), l Ll = []
                                                    theorem List.flatten_ne_nil_iff {α : Type u_1} {xs : List (List α)} :
                                                    xs.flatten [] (x : List α), x xs x []
                                                    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) :
                                                    theorem List.forall_mem_flatten {α : Type u_1} {p : αProp} {L : List (List α)} :
                                                    (∀ (x : α), x L.flattenp x) ∀ (l : List α), l L∀ (x : α), x lp x
                                                    theorem List.flatten_eq_flatMap {α : Type u_1} {L : List (List α)} :
                                                    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 α)) :
                                                    @[simp]
                                                    theorem List.filter_flatten {α : Type u_1} (p : αBool) (L : List (List α)) :
                                                    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_eq_cons_iff {α : Type u_1} {xs : List (List α)} {y : α} {ys : List α} :
                                                    xs.flatten = y :: ys (as : List (List α)), (bs : List α), (cs : List (List α)), xs = as ++ (y :: bs) :: cs (∀ (l : List α), l asl = []) 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 asl = []) 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 asl = []) ∀ (l : List α), l bsl = []
                                                    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 asl = []) ∀ (l : List α), l bsl = []
                                                    theorem List.flatten_eq_append_iff {α : Type u_1} {xs : List (List α)} {ys zs : List α} :
                                                    xs.flatten = ys ++ zs ( (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.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 α)} :

                                                    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 α)) :
                                                    @[simp]
                                                    theorem List.flatMap_id' {α : Type u_1} (l : List (List α)) :
                                                    flatMap (fun (a : List α) => a) 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 lf x = []
                                                    @[reducible, inline, deprecated List.flatMap_eq_nil_iff (since := "2024-09-05")]
                                                    abbrev List.bind_eq_nil {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                    flatMap f l = [] ∀ (x : α), x lf x = []
                                                    Equations
                                                    Instances For
                                                      theorem List.forall_mem_flatMap {β : Type u_1} {α : Type u_2} {p : βProp} {l : List α} {f : αList β} :
                                                      (∀ (x : β), x flatMap f lp x) ∀ (a : α), a l∀ (b : β), b f ap 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
                                                      @[simp]
                                                      theorem List.flatMap_append {α : Type u_1} {β : Type u_2} (xs ys : List α) (f : αList β) :
                                                      flatMap f (xs ++ ys) = flatMap f xs ++ flatMap f ys
                                                      @[reducible, inline, deprecated List.flatMap_append (since := "2024-07-24")]
                                                      abbrev List.append_bind {α : Type u_1} {β : Type u_2} (xs ys : List α) (f : αList β) :
                                                      flatMap f (xs ++ ys) = flatMap f xs ++ flatMap f ys
                                                      Equations
                                                      Instances For
                                                        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 : α✝} :
                                                        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, deprecated List.mem_replicate (since := "2024-09-05")]
                                                        theorem List.contains_replicate {α : Type u_1} [BEq α] {n : Nat} {a b : α} :
                                                        (replicate n b).contains a = (a == b && !n == 0)
                                                        @[simp, deprecated List.mem_replicate (since := "2024-09-05")]
                                                        theorem List.decide_mem_replicate {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {n : Nat} :
                                                        decide (b replicate n a) = (decide ¬(n == 0) = true && b == a)
                                                        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 ap 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
                                                        @[reducible, inline, deprecated List.replicate_eq_nil_iff (since := "2024-09-05")]
                                                        abbrev List.replicate_eq_nil {α : Type u_1} {n : Nat} (a : α) :
                                                        replicate n a = [] n = 0
                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem List.getElem_replicate {α : Type u_1} (a : α) {n m : Nat} (h : m < (replicate n a).length) :
                                                          (replicate n a)[m] = a
                                                          theorem List.getElem?_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} :
                                                          @[simp]
                                                          theorem List.getElem?_replicate_of_lt {α✝ : Type u_1} {a : α✝} {n m : Nat} (h : m < n) :
                                                          theorem List.head?_replicate {α : Type u_1} (a : α) (n : Nat) :
                                                          @[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 lb = 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 lb = a
                                                          @[reducible, inline, deprecated List.eq_replicate_iff (since := "2024-09-05")]
                                                          abbrev List.eq_replicate {α : Type u_1} {a : α} {n : Nat} {l : List α} :
                                                          l = replicate n a l.length = n ∀ (b : α), b lb = a
                                                          Equations
                                                          Instances For
                                                            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 lf x = b
                                                            @[simp]
                                                            theorem List.map_const {α : Type u_1} {β : Type u_2} (l : List α) (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
                                                            @[reducible, inline, deprecated List.replicate_append_replicate (since := "2025-01-16")]
                                                            abbrev List.append_replicate_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} :
                                                            replicate n a ++ replicate m a = replicate (n + m) a
                                                            Equations
                                                            Instances For
                                                              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
                                                              @[reducible, inline, deprecated List.append_eq_replicate_iff (since := "2024-09-05")]
                                                              abbrev List.append_eq_replicate {α : 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
                                                              Equations
                                                              Instances For
                                                                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} :
                                                                @[simp]
                                                                theorem List.filter_replicate_of_pos {α✝ : Type u_1} {p : α✝Bool} {n : Nat} {a : α✝} (h : p a = true) :
                                                                @[simp]
                                                                theorem List.filter_replicate_of_neg {α✝ : Type u_1} {p : α✝Bool} {n : Nat} {a : α✝} (h : ¬p a = true) :
                                                                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 =>