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

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} :
l.get? n = none l.length n
@[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 α) (n : Nat) (a : α) :
l.getD n a = l[n]?.getD a

get! #

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

theorem List.get!_eq_getD {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) :
l.get! n = l.getD n default
@[simp]
theorem List.get!_eq_getElem! {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) :
l.get! n = l[n]!

getElem! #

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

@[simp]
theorem List.getElem!_eq_getElem?_getD {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) :
l[n]! = l[n]?.getD default

getElem? and getElem #

@[simp]
theorem List.getElem?_eq_getElem {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) :
l[n]? = some l[n]
theorem List.getElem?_eq_some_iff {α : Type u_1} {n : Nat} {a : α} {l : List α} :
l[n]? = some a ∃ (h : n < l.length), l[n] = a
theorem List.some_eq_getElem?_iff {α : Type u_1} {a : α} {n : Nat} {l : List α} :
some a = l[n]? ∃ (h : n < l.length), l[n] = a
@[simp]
theorem List.getElem?_eq_none_iff {α✝ : Type u_1} {l : List α✝} {n : Nat} :
l[n]? = none l.length n
@[simp]
theorem List.none_eq_getElem?_iff {α : Type u_1} {l : List α} {n : Nat} :
none = l[n]? l.length n
theorem List.getElem?_eq_none {α✝ : Type u_1} {l : List α✝} {n : Nat} (h : l.length n) :
l[n]? = none
@[simp]
theorem List.some_getElem_eq_getElem?_iff {α : Type u_1} (xs : List α) (i : Nat) (h : i < xs.length) :
some xs[i] = xs[i]? True
@[simp]
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 α} {n : Nat} {h : n < l.length} :
l[n] = x l[n]? = some x
theorem List.getElem_eq_getElem?_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) :
l[i] = l[i]?.get
@[simp]
theorem List.getElem?_nil {α : Type u_1} {n : Nat} :
[][n]? = none
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 : α} {n : Nat} {l : List α} :
(a :: l)[n + 1]? = l[n]?
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]?
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].

@[simp]
theorem List.getElem_singleton {α : Type u_1} {i : Nat} (a : α) (h : i < 1) :
[a][i] = a
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 : ∀ (n : Nat), l₁[n]? = l₂[n]?) :
l₁ = l₂
theorem List.ext_getElem {α : Type u_1} {l₁ l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁[n] = l₂[n]) :
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
theorem List.isSome_getElem? {α : Type u_1} {l : List α} {n : Nat} :
l[n]?.isSome = true n < l.length
theorem List.isNone_getElem? {α : Type u_1} {l : List α} {n : Nat} :
l[n]?.isNone = true l.length n

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.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) :
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∃ (n : Nat), ∃ (h : n < l.length), l[n] = a
theorem List.getElem?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a l) :
∃ (n : Nat), l[n]? = some a
theorem List.mem_of_getElem? {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) :
a l
theorem List.mem_iff_getElem {α : Type u_1} {a : α} {l : List α} :
a l ∃ (n : Nat), ∃ (h : n < l.length), l[n] = a
theorem List.mem_iff_getElem? {α : Type u_1} {a : α} {l : List α} :
a l ∃ (n : Nat), l[n]? = some a
theorem List.forall_getElem {α : Type u_1} {l : List α} {p : αProp} :
(∀ (n : Nat) (h : n < l.length), p l[n]) ∀ (a : α), a lp 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 α} :
List.elem a as = true a as
@[simp]
theorem List.elem_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (as : List α) :
List.elem a as = decide (a as)

isEmpty #

theorem List.isEmpty_iff {α : Type u_1} {l : List α} :
l.isEmpty = true 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
@[simp]
theorem List.isEmpty_eq_true {α : Type u_1} {l : List α} :
l.isEmpty = true l = []
@[simp]
theorem List.isEmpty_eq_false {α : Type u_1} {l : List α} :
l.isEmpty = false l []

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} {a : α} [BEq α] [LawfulBEq α] {l : List α} :
(l.any fun (x : α) => a == x) = true a l
theorem List.any_beq' {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} :
(l.any fun (x : α) => x == a) = true a l
theorem List.all_bne {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} :
(l.all fun (x : α) => a != x) = true ¬a l
theorem List.all_bne' {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} :
(l.all fun (x : α) => x != a) = true ¬a l

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 α} {m n : Nat} {a : α} (h : n < (l.set m a).length) :
(l.set m a)[n] = if m = n then a else l[n]
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]?

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.reflBEq_iff {α : Type u_1} [BEq α] :
@[simp]
theorem List.lawfulBEq_iff {α : Type u_1} [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₂)
theorem List.length_eq_of_beq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (h : (l₁ == l₂) = true) :
l₁.length = l₂.length

Lexicographic ordering #

theorem List.lt_irrefl {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) (l : List α) :
¬l < l
theorem List.lt_trans {α : Type u_1} [LT α] [DecidableRel LT.lt] (lt_trans : ∀ {x y z : α}, x < yy < zx < z) (le_trans : ∀ {x y z : α}, ¬x < y¬y < z¬x < z) {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) :
l₁ < l₃
theorem List.lt_antisymm {α : Type u_1} [LT α] (lt_antisymm : ∀ {x y : α}, ¬x < y¬y < xx = y) {l₁ l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) :
l₁ = l₂

foldlM and foldrM #

@[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 : β) :
List.foldlM f b l.reverse = List.foldrM (fun (x : α) (y : β) => f y x) b l
@[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 α) :
List.foldlM f b (l ++ l') = do let initList.foldlM f b l List.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 : β) :
List.foldrM f b (a :: l) = List.foldrM f b l >>= f a
theorem List.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} (f : βαβ) (b : β) (l : List α) :
theorem List.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (l : List α) :
@[simp]
theorem List.id_run_foldlM {β : Type u_1} {α : Type u_2} (f : βαId β) (b : β) (l : List α) :
(List.foldlM f b l).run = List.foldl f b l
@[simp]
theorem List.id_run_foldrM {α : Type u_1} {β : Type u_2} (f : αβId β) (b : β) (l : List α) :
(List.foldrM f b l).run = List.foldr f b l

foldl and foldr #

@[simp]
theorem List.foldr_cons_eq_append {α : Type u_1} {l' : List α} (l : List α) :
List.foldr List.cons l' l = l ++ l'
@[reducible, inline, deprecated List.foldr_cons_eq_append]
abbrev List.foldr_self_append {α : Type u_1} {l' : List α} (l : List α) :
List.foldr List.cons l' l = l ++ l'
Equations
Instances For
    @[simp]
    theorem List.foldl_flip_cons_eq_append {α : Type u_1} {l' : List α} (l : List α) :
    List.foldl (fun (x : List α) (y : α) => y :: x) l' l = l.reverse ++ l'
    theorem List.foldr_cons_nil {α : Type u_1} (l : List α) :
    List.foldr List.cons [] l = l
    @[reducible, inline, deprecated List.foldr_cons_nil]
    abbrev List.foldr_self {α : Type u_1} (l : List α) :
    List.foldr List.cons [] l = l
    Equations
    Instances For
      theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁β₂) (g : αβ₂α) (l : List β₁) (init : α) :
      List.foldl g init (List.map f l) = List.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 : β) :
      List.foldr g init (List.map f l) = List.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 : γ) :
      List.foldl g init (List.filterMap f l) = List.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 : γ) :
      List.foldr g init (List.filterMap f l) = List.foldr (fun (x : α) (y : γ) => match f x with | some b => g b y | none => y) init l
      theorem List.foldl_map' {α : Type u_1} {β : Type u_2} (g : αβ) (f : ααα) (f' : βββ) (a : α) (l : List α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) :
      List.foldl f' (g a) (List.map g l) = g (List.foldl f a l)
      theorem List.foldr_map' {α : Type u_1} {β : Type u_2} (g : αβ) (f : ααα) (f' : βββ) (a : α) (l : List α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) :
      List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)
      theorem List.foldl_assoc {α : Type u_1} {op : ααα} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α} :
      List.foldl op (op a₁ a₂) l = op a₁ (List.foldl op a₂ l)
      theorem List.foldr_assoc {α : Type u_1} {op : ααα} [ha : Std.Associative op] {l : List α} {a₁ a₂ : α} :
      List.foldr op (op a₁ a₂) l = op (List.foldr op a₁ l) a₂
      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)) :
      List.foldl g₂ (f init) l = f (List.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)) :
      List.foldr g₂ (f init) l = f (List.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 lmotive (op b a))motive (List.foldl op b l)

      Prove a proposition about the result of List.foldl, by proving it for the initial data, and the implication that the operation applied to any element of the list preserves the property.

      The motive can take values in Sort _, so this may be used to construct data, as well as to prove propositions.

      Equations
      Instances For
        @[simp]
        theorem List.foldlRecOn_nil {β : Type u_1} {b : β} {α : Type u_2} {op : βαβ} {motive : βSort u_3} (hb : motive b) (hl : (b : β) → motive b(a : α) → a []motive (op b a)) :
        List.foldlRecOn [] op b hb hl = hb
        @[simp]
        theorem List.foldlRecOn_cons {β : Type u_1} {b : β} {α : Type u_2} {x : α} {l : List α} {op : βαβ} {motive : βSort u_3} (hb : motive b) (hl : (b : β) → motive b(a : α) → a x :: lmotive (op b a)) :
        List.foldlRecOn (x :: l) op b hb hl = List.foldlRecOn l op (op b x) (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 lmotive (op a b))motive (List.foldr op b l)

        Prove a proposition about the result of List.foldr, by proving it for the initial data, and the implication that the operation applied to any element of the list preserves the property.

        The motive can take values in Sort _, so this may be used to construct data, as well as to prove propositions.

        Equations
        Instances For
          @[simp]
          theorem List.foldrRecOn_nil {β : Type u_1} {b : β} {α : Type u_2} {op : αββ} {motive : βSort u_3} (hb : motive b) (hl : (b : β) → motive b(a : α) → a []motive (op a b)) :
          List.foldrRecOn [] op b hb hl = hb
          @[simp]
          theorem List.foldrRecOn_cons {β : Type u_1} {b : β} {α : Type u_2} {x : α} {l : List α} {op : αββ} {motive : βSort u_3} (hb : motive b) (hl : (b : β) → motive b(a : α) → a x :: lmotive (op a b)) :
          List.foldrRecOn (x :: l) op b hb hl = hl (List.foldr op b l) (List.foldrRecOn l op b 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} {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 (List.foldl (fun (acc : β) (a : α) => f acc a) a l) (List.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} {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 (List.foldr (fun (a : α) (acc : β) => f a acc) a l) (List.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) :
          List.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) :
          List.foldr (fun (x : α) (x : Nat) => x + a) b l = b + a * l.length

          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]
          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 α) :
          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.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 α) (n : Nat) (h : n = xs.length) :
          (x :: xs)[n] = (x :: xs).getLast
          @[deprecated List.getElem_cons_length]
          theorem List.get_cons_length {α : Type u_1} (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
          (x :: xs).get n, = (x :: xs).getLast

          getLast? #

          @[simp]
          theorem List.getLast?_singleton {α : Type u_1} (a : α) :
          [a].getLast? = some a
          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)
          @[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?]
          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 α) :
          (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 al.getLast! = a
          theorem List.getLast!_eq_getElem! {α : Type u_1} [Inhabited α] {l : List α} :
          l.getLast! = l[l.length - 1]!

          Head and tail #

          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 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 α✝} :
          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.head?_isSome {α✝ : 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_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 α) :
          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?

          Basic operations #

          map #

          @[simp]
          theorem List.map_id_fun {α : Type u_1} :
          List.map id = id
          @[simp]
          theorem List.map_id_fun' {α : Type u_1} :
          (List.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 α) :
          List.map id l = l
          theorem List.map_id' {α : Type u_1} (l : List α) :
          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 α) :
          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 : α) :
          List.map f [a] = [f a]
          @[simp]
          theorem List.length_map {α : Type u_1} {β : Type u_2} (as : List α) (f : αβ) :
          (List.map f as).length = as.length
          @[simp]
          theorem List.getElem?_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (n : Nat) :
          (List.map f l)[n]? = Option.map f l[n]?
          @[deprecated List.getElem?_map]
          theorem List.get?_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (n : Nat) :
          (List.map f l).get? n = Option.map f (l.get? n)
          @[simp]
          theorem List.getElem_map {α : Type u_1} {β : Type u_2} (f : αβ) {l : List α} {n : Nat} {h : n < (List.map f l).length} :
          (List.map f l)[n] = f l[n]
          @[deprecated List.getElem_map]
          theorem List.get_map {α : Type u_1} {β : Type u_2} (f : αβ) {l : List α} {n : Fin (List.map f l).length} :
          (List.map f l).get n = f (l.get n, )
          @[simp]
          theorem List.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : αβ} {l : List α} :
          b List.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 List.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 List.map f l
          theorem List.forall_mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {P : βProp} :
          (∀ (i : β), i List.map f lP i) ∀ (j : α), j lP (f j)
          @[reducible, inline, deprecated List.forall_mem_map]
          abbrev List.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {P : βProp} :
          (∀ (i : β), i List.map f lP i) ∀ (j : α), j lP (f j)
          Equations
          Instances For
            @[simp]
            theorem List.map_inj_left {α : Type u_1} {β : Type u_2} {l : List α} {f g : αβ} :
            List.map f l = List.map g l ∀ (a : α), a lf a = g a
            theorem List.map_congr_left {α✝ : Type u_1} {l : List α✝} {α✝¹ : Type u_2} {f g : α✝α✝¹} (h : ∀ (a : α✝), a lf a = g a) :
            theorem List.map_inj {α✝ : Type u_1} {α✝¹ : Type u_2} {f g : α✝α✝¹} :
            @[simp]
            theorem List.map_eq_nil_iff {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} :
            List.map f l = [] l = []
            @[reducible, inline, deprecated List.map_eq_nil_iff]
            abbrev List.map_eq_nil {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} :
            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 : List.map f l = []) :
              l = []
              theorem List.map_eq_cons_iff {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : αβ} {l : List α} :
              List.map f l = b :: l₂ ∃ (a : α), ∃ (l₁ : List α), l = a :: l₁ f a = b List.map f l₁ = l₂
              @[reducible, inline, deprecated List.map_eq_cons_iff]
              abbrev List.map_eq_cons {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : αβ} {l : List α} :
              List.map f l = b :: l₂ ∃ (a : α), ∃ (l₁ : List α), l = a :: l₁ f a = b List.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 α} :
                List.map f l = b :: l₂ Option.map f l.head? = some b Option.map (List.map f) l.tail? = some l₂
                @[reducible, inline, deprecated List.map_eq_cons']
                abbrev List.map_eq_cons' {α : Type u_1} {β : Type u_2} {b : β} {l₂ : List β} {f : αβ} {l : List α} :
                List.map f l = b :: l₂ Option.map f l.head? = some b Option.map (List.map f) l.tail? = some l₂
                Equations
                Instances For
                  theorem List.map_eq_map_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝α✝¹} {l : List α✝} {g : α✝α✝¹} :
                  List.map f l = List.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 α✝¹} :
                  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 α) :
                  List.map f l = List.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 : α} :
                  List.map f (l.set i a) = (List.map f l).set i (f a)
                  @[deprecated]
                  theorem List.set_map {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {n : Nat} {a : α} :
                  (List.map f l).set n (f a) = List.map f (l.set n a)
                  @[simp]
                  theorem List.head_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (w : List.map f l []) :
                  (List.map f l).head w = f (l.head )
                  @[simp]
                  theorem List.head?_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                  (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 (List.map f) l.tail? = (List.map f l).tail?
                  @[simp]
                  theorem List.map_tail {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                  List.map f l.tail = (List.map f l).tail
                  theorem List.headD_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (a : α) :
                  (List.map f l).headD (f a) = f (l.headD a)
                  theorem List.tailD_map {α : Type u_1} {β : Type u_2} (f : αβ) (l l' : List α) :
                  (List.map f l).tailD (List.map f l') = List.map f (l.tailD l')
                  @[simp]
                  theorem List.getLast_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (h : List.map f l []) :
                  (List.map f l).getLast h = f (l.getLast )
                  @[simp]
                  theorem List.getLast?_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                  (List.map f l).getLast? = Option.map f l.getLast?
                  theorem List.getLastD_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (a : α) :
                  (List.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 α) :
                  List.map g (List.map f l) = List.map (g f) l

                  filter #

                  @[simp]
                  theorem List.filter_cons_of_pos {α : Type u_1} {p : αBool} {a : α} {l : List α} (pa : p a = true) :
                  List.filter p (a :: l) = a :: List.filter p l
                  @[simp]
                  theorem List.filter_cons_of_neg {α : Type u_1} {p : αBool} {a : α} {l : List α} (pa : ¬p a = true) :
                  theorem List.filter_cons {α : Type u_1} {x : α} {xs : List α} {p : αBool} :
                  List.filter p (x :: xs) = if p x = true then x :: List.filter p xs else List.filter p xs
                  theorem List.length_filter_le {α : Type u_1} (p : αBool) (l : List α) :
                  (List.filter p l).length l.length
                  @[simp]
                  theorem List.filter_eq_self {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} :
                  List.filter p l = l ∀ (a : α✝), a lp a = true
                  @[simp]
                  theorem List.filter_length_eq_length {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} :
                  (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 List.filter p as x as p x = true
                  @[simp]
                  theorem List.filter_eq_nil_iff {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} :
                  List.filter p l = [] ∀ (a : α✝), a l¬p a = true
                  @[reducible, inline, deprecated List.filter_eq_nil_iff]
                  abbrev List.filter_eq_nil {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} :
                  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 List.filter p lP i) ∀ (j : α), j lp j = trueP j
                    @[reducible, inline, deprecated List.forall_mem_filter]
                    abbrev List.forall_mem_filter_iff {α : Type u_1} {l : List α} {p : αBool} {P : αProp} :
                    (∀ (i : α), i List.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 α✝) :
                      List.filter p (List.filter q l) = List.filter (fun (a : α✝) => p a && q a) l
                      theorem List.foldl_filter {α : Type u_1} {β : Type u_2} (p : αBool) (f : βαβ) (l : List α) (init : β) :
                      List.foldl f init (List.filter p l) = List.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 : β) :
                      List.foldr f init (List.filter p l) = List.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 β) :
                      @[reducible, inline, deprecated List.filter_map]
                      abbrev List.map_filter {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) :
                      Equations
                      Instances For
                        theorem List.map_filter_eq_foldr {α : Type u_1} {β : Type u_2} (f : αβ) (p : αBool) (as : List α) :
                        List.map f (List.filter p as) = List.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 α) :
                        List.filter p (l₁ ++ l₂) = List.filter p l₁ ++ List.filter p l₂
                        theorem List.filter_eq_cons_iff {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} {a : α✝} {as : List α✝} :
                        List.filter p l = a :: as ∃ (l₁ : List α✝), ∃ (l₂ : List α✝), l = l₁ ++ a :: l₂ (∀ (x : α✝), x l₁¬p x = true) p a = true List.filter p l₂ = as
                        @[reducible, inline, deprecated List.filter_eq_cons_iff]
                        abbrev List.filter_eq_cons {α✝ : Type u_1} {p : α✝Bool} {l : List α✝} {a : α✝} {as : List α✝} :
                        List.filter p l = a :: as ∃ (l₁ : List α✝), ∃ (l₂ : List α✝), l = l₁ ++ a :: l₂ (∀ (x : α✝), x l₁¬p x = true) p a = true List.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)List.filter p l = List.filter q l
                          @[reducible, inline, deprecated List.filter_congr]
                          abbrev List.filter_congr' {α : Type u_1} {p q : αBool} {l : List α} :
                          (∀ (x : α), x lp x = q x)List.filter p l = List.filter q l
                          Equations
                          Instances For
                            theorem List.head_filter_of_pos {α : Type u_1} {p : αBool} {l : List α} (w : l []) (h : p (l.head w) = true) :
                            (List.filter p l).head = l.head w
                            @[simp]
                            theorem List.filter_sublist {α : Type u_1} {p : αBool} (l : List α) :
                            (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) :
                            @[simp]
                            theorem List.filterMap_cons_some {α : Type u_1} {β : Type u_2} {f : αOption β} {a : α} {l : List α} {b : β} (h : f a = some b) :
                            @[simp]
                            theorem List.filterMap_eq_map {α : Type u_1} {β : Type u_2} (f : αβ) :
                            @[simp]
                            theorem List.filterMap_some_fun {α : Type u_1} :
                            theorem List.filterMap_some {α : Type u_1} (l : List α) :
                            List.filterMap some l = l
                            theorem List.map_filterMap_some_eq_filter_map_isSome {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
                            List.map some (List.filterMap f l) = List.filter (fun (b : Option β) => b.isSome) (List.map f l)
                            theorem List.length_filterMap_le {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
                            (List.filterMap f l).length l.length
                            @[simp]
                            theorem List.filterMap_length_eq_length {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝Option α✝¹} {l : List α✝} :
                            (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) :
                            List.filterMap (Option.guard fun (x : α) => p x = true) = List.filter p
                            theorem List.filterMap_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption β) (g : βOption γ) (l : List α) :
                            List.filterMap g (List.filterMap f l) = List.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 α) :
                            List.map g (List.filterMap f l) = List.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 α) :
                            theorem List.filter_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (p : βBool) (l : List α) :
                            List.filter p (List.filterMap f l) = List.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 α) :
                            List.filterMap f (List.filter p l) = List.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 List.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 List.filterMap f lP i) ∀ (j : α), j l∀ (b : β), f j = some bP b
                            @[reducible, inline, deprecated List.forall_mem_filterMap]
                            abbrev List.forall_mem_filterMap_iff {α : Type u_1} {β : Type u_2} {f : αOption β} {l : List α} {P : βProp} :
                            (∀ (i : β), i List.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 β) :
                              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 α) :
                              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) :
                              (List.filterMap f l).head = b
                              theorem List.forall_none_of_filterMap_eq_nil {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝Option α✝¹} {xs : List α✝} (h : List.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 α✝} :
                              List.filterMap f l = [] ∀ (a : α✝), a lf a = none
                              @[reducible, inline, deprecated List.filterMap_eq_nil_iff]
                              abbrev List.filterMap_eq_nil {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝Option α✝¹} {l : List α✝} :
                              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 α✝¹} :
                                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 List.filterMap f l₂ = bs
                                @[reducible, inline, deprecated List.filterMap_eq_cons_iff]
                                abbrev List.filterMap_eq_cons {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝Option α✝¹} {l : List α✝} {b : α✝¹} {bs : List α✝¹} :
                                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 List.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)
                                  theorem List.getElem_append {α : Type u_1} {l₁ l₂ : List α} (n : Nat) (h : n < (l₁ ++ l₂).length) :
                                  (l₁ ++ l₂)[n] = if h' : n < l₁.length then l₁[n] else l₂[n - l₁.length]
                                  theorem List.getElem?_append_left {α : Type u_1} {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
                                  (l₁ ++ l₂)[n]? = l₁[n]?
                                  theorem List.getElem?_append_right {α : Type u_1} {l₁ l₂ : List α} {n : Nat} :
                                  l₁.length n(l₁ ++ l₂)[n]? = l₂[n - l₁.length]?
                                  theorem List.getElem?_append {α : Type u_1} {l₁ l₂ : List α} {n : Nat} :
                                  (l₁ ++ l₂)[n]? = if n < l₁.length then l₁[n]? else l₂[n - l₁.length]?
                                  @[deprecated List.getElem?_append_right]
                                  theorem List.get?_append_right {α : Type u_1} {l₁ l₂ : List α} {n : Nat} (h : l₁.length n) :
                                  (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
                                  theorem List.getElem_append_left' {α : Type u_1} (l₂ : List α) {l₁ : List α} {n : Nat} (hn : n < l₁.length) :
                                  l₁[n] = (l₁ ++ l₂)[n]

                                  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 α} {n : Nat} (hn : n < l₂.length) :
                                  l₂[n] = (l₁ ++ l₂)[n + l₁.length]

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

                                  @[deprecated]
                                  theorem List.get_append_right_aux {α : Type u_1} {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
                                  n - l₁.length < l₂.length
                                  @[deprecated List.getElem_append_right]
                                  theorem List.get_append_right' {α : Type u_1} {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
                                  (l₁ ++ l₂).get n, h₂ = l₂.get n - l₁.length,
                                  theorem List.getElem_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
                                  l[n] = a
                                  @[deprecated]
                                  theorem List.get_of_append_proof {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
                                  n < l.length
                                  @[deprecated List.getElem_of_append]
                                  theorem List.get_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) :
                                  l.get n, = a
                                  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.

                                  @[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 = []
                                  @[simp]
                                  theorem List.append_eq_nil {α✝ : Type u_1} {p q : List α✝} :
                                  p ++ q = [] p = [] q = []
                                  theorem List.getLast_concat {α : Type u_1} {a : α} (l : List α) :
                                  (l ++ [a]).getLast = a
                                  @[deprecated List.getElem_append]
                                  theorem List.get_append {α : Type u_1} {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length) :
                                  (l₁ ++ l₂).get n, = l₁.get n, h
                                  @[deprecated List.getElem_append_left]
                                  theorem List.get_append_left {α : Type u_1} {i : Nat} (as bs : List α) (h : i < as.length) {h' : i < (as ++ bs).length} :
                                  (as ++ bs).get i, h' = as.get i, h
                                  @[deprecated List.getElem_append_right]
                                  theorem List.get_append_right {α : Type u_1} {i : Nat} (as bs : List α) (h : as.length i) {h' : i < (as ++ bs).length} {h'' : i - as.length < bs.length} :
                                  (as ++ bs).get i, h' = bs.get i - as.length, h''
                                  @[deprecated List.getElem?_append_left]
                                  theorem List.get?_append {α : Type u_1} {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
                                  (l₁ ++ l₂).get? n = l₁.get? n
                                  @[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]
                                  abbrev List.tail_append_left {α : Type u_1} {xs ys : List α} (h : xs []) :
                                  (xs ++ ys).tail = xs.tail ++ ys
                                  Equations
                                  Instances For
                                    theorem List.nil_eq_append_iff {α✝ : Type u_1} {a b : List α✝} :
                                    [] = a ++ b a = [] b = []
                                    @[reducible, inline, deprecated List.nil_eq_append_iff]
                                    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]
                                      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]
                                      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]
                                      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]
                                        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_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]
                                          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']
                                            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.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.mem_append_eq {α : Type u_1} (a : α) (s t : List α) :
                                              (a s ++ t) = (a s a t)
                                              @[reducible, inline, deprecated List.mem_append_left]
                                              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]
                                                abbrev List.mem_append_of_mem_right {α : Type u_1} {b : α} {bs : List α} (as : List α) :
                                                b bsb as ++ bs
                                                Equations
                                                Instances For
                                                  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.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
                                                  @[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 α) :
                                                  List.foldrM f b (l ++ l') = do let initList.foldrM f b l' List.foldrM f init l
                                                  @[simp]
                                                  theorem List.foldl_append {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (l l' : List α) :
                                                  List.foldl f b (l ++ l') = List.foldl f (List.foldl f b l) l'
                                                  @[simp]
                                                  theorem List.foldr_append {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (l l' : List α) :
                                                  List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') l
                                                  theorem List.filterMap_eq_append_iff {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : αOption β} :
                                                  List.filterMap f l = L₁ ++ L₂ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.filterMap f l₁ = L₁ List.filterMap f l₂ = L₂
                                                  @[reducible, inline, deprecated List.filterMap_eq_append_iff]
                                                  abbrev List.filterMap_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : αOption β} :
                                                  List.filterMap f l = L₁ ++ L₂ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.filterMap f l₁ = L₁ List.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₂ = List.filterMap f l ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.filterMap f l₁ = L₁ List.filterMap f l₂ = L₂
                                                    @[reducible, inline, deprecated List.append_eq_filterMap]
                                                    abbrev List.append_eq_filterMap {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : αOption β} :
                                                    L₁ ++ L₂ = List.filterMap f l ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.filterMap f l₁ = L₁ List.filterMap f l₂ = L₂
                                                    Equations
                                                    Instances For
                                                      theorem List.filter_eq_append_iff {α : Type u_1} {l L₁ L₂ : List α} {p : αBool} :
                                                      List.filter p l = L₁ ++ L₂ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.filter p l₁ = L₁ List.filter p l₂ = L₂
                                                      theorem List.append_eq_filter_iff {α : Type u_1} {L₁ L₂ l : List α} {p : αBool} :
                                                      L₁ ++ L₂ = List.filter p l ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.filter p l₁ = L₁ List.filter p l₂ = L₂
                                                      @[reducible, inline, deprecated List.append_eq_filter_iff]
                                                      abbrev List.append_eq_filter {α : Type u_1} {L₁ L₂ l : List α} {p : αBool} :
                                                      L₁ ++ L₂ = List.filter p l ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.filter p l₁ = L₁ List.filter p l₂ = L₂
                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem List.map_append {α : Type u_1} {β : Type u_2} (f : αβ) (l₁ l₂ : List α) :
                                                        List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂
                                                        theorem List.map_eq_append_iff {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : αβ} :
                                                        List.map f l = L₁ ++ L₂ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.map f l₁ = L₁ List.map f l₂ = L₂
                                                        theorem List.append_eq_map_iff {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : αβ} :
                                                        L₁ ++ L₂ = List.map f l ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.map f l₁ = L₁ List.map f l₂ = L₂
                                                        @[reducible, inline, deprecated List.map_eq_append_iff]
                                                        abbrev List.map_eq_append {α : Type u_1} {β : Type u_2} {l : List α} {L₁ L₂ : List β} {f : αβ} :
                                                        List.map f l = L₁ ++ L₂ ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.map f l₁ = L₁ List.map f l₂ = L₂
                                                        Equations
                                                        Instances For
                                                          @[reducible, inline, deprecated List.append_eq_map_iff]
                                                          abbrev List.append_eq_map {α : Type u_1} {β : Type u_2} {L₁ L₂ : List β} {l : List α} {f : αβ} :
                                                          L₁ ++ L₂ = List.map f l ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.map f l₁ = L₁ List.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 : α) :
                                                            [].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 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]
                                                            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_ne_nil {α : Type u_1} (a : α) (l : List α) :
                                                              l.concat 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 α) :
                                                              List.map f (l.concat a) = (List.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 = (List.map List.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 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) :
                                                              a L.flatten
                                                              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 α)} :
                                                              L.flatten = L.flatMap id
                                                              theorem List.head?_flatten {α : Type u_1} {L : List (List α)} :
                                                              L.flatten.head? = List.findSome? (fun (l : List α) => l.head?) L
                                                              theorem List.foldl_flatten {β : Type u_1} {α : Type u_2} (f : βαβ) (b : β) (L : List (List α)) :
                                                              List.foldl f b L.flatten = List.foldl (fun (b : β) (l : List α) => List.foldl f b l) b L
                                                              theorem List.foldr_flatten {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (L : List (List α)) :
                                                              List.foldr f b L.flatten = List.foldr (fun (l : List α) (b : β) => List.foldr f b l) b L
                                                              @[simp]
                                                              theorem List.map_flatten {α : Type u_1} {β : Type u_2} (f : αβ) (L : List (List α)) :
                                                              List.map f L.flatten = (List.map (List.map f) L).flatten
                                                              @[simp]
                                                              theorem List.filterMap_flatten {α : Type u_1} {β : Type u_2} (f : αOption β) (L : List (List α)) :
                                                              List.filterMap f L.flatten = (List.map (List.filterMap f) L).flatten
                                                              @[simp]
                                                              theorem List.filter_flatten {α : Type u_1} (p : αBool) (L : List (List α)) :
                                                              List.filter p L.flatten = (List.map (List.filter p) L).flatten
                                                              theorem List.flatten_filter_not_isEmpty {α : Type u_1} {L : List (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 α)} :
                                                              (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 = (List.map List.flatten L).flatten
                                                              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.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.eq_iff_flatten_eq {α : Type u_1} {L L' : List (List α)} :
                                                              L = L' L.flatten = L'.flatten List.map List.length L = List.map List.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 β) :
                                                              l.flatMap f = (List.map f l).flatten
                                                              @[simp]
                                                              theorem List.flatMap_id {α : Type u_1} (l : List (List α)) :
                                                              l.flatMap id = l.flatten
                                                              @[simp]
                                                              theorem List.mem_flatMap {α : Type u_1} {β : Type u_2} {f : αList β} {b : β} {l : List α} :
                                                              b l.flatMap f ∃ (a : α), a l b f a
                                                              theorem List.exists_of_mem_flatMap {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : αList β} :
                                                              b l.flatMap f∃ (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 l.flatMap f
                                                              @[simp]
                                                              theorem List.flatMap_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                              l.flatMap f = [] ∀ (x : α), x lf x = []
                                                              @[reducible, inline, deprecated List.flatMap_eq_nil_iff]
                                                              abbrev List.bind_eq_nil {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                              l.flatMap f = [] ∀ (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 l.flatMap fp x) ∀ (a : α), a l∀ (b : β), b f ap b
                                                                theorem List.flatMap_singleton {α : Type u_1} {β : Type u_2} (f : αList β) (x : α) :
                                                                [x].flatMap f = f x
                                                                @[simp]
                                                                theorem List.flatMap_singleton' {α : Type u_1} (l : List α) :
                                                                (l.flatMap fun (x : α) => [x]) = l
                                                                theorem List.head?_flatMap {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                                (l.flatMap f).head? = List.findSome? (fun (a : α) => (f a).head?) l
                                                                @[simp]
                                                                theorem List.flatMap_append {α : Type u_1} {β : Type u_2} (xs ys : List α) (f : αList β) :
                                                                (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f
                                                                @[reducible, inline, deprecated List.flatMap_append]
                                                                abbrev List.append_bind {α : Type u_1} {β : Type u_2} (xs ys : List α) (f : αList β) :
                                                                (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f
                                                                Equations
                                                                Instances For
                                                                  theorem List.flatMap_assoc {γ : Type u_1} {α : Type u_2} {β : Type u_3} (l : List α) (f : αList β) (g : βList γ) :
                                                                  (l.flatMap f).flatMap g = l.flatMap fun (x : α) => (f x).flatMap g
                                                                  theorem List.map_flatMap {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : βγ) (g : αList β) (l : List α) :
                                                                  List.map f (l.flatMap g) = l.flatMap fun (a : α) => List.map f (g a)
                                                                  theorem List.flatMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : βList γ) (l : List α) :
                                                                  (List.map f l).flatMap g = l.flatMap fun (a : α) => g (f a)
                                                                  theorem List.map_eq_flatMap {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                                                                  List.map f l = l.flatMap fun (x : α) => [f x]
                                                                  theorem List.filterMap_flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : List α) (g : αList β) (f : βOption γ) :
                                                                  List.filterMap f (l.flatMap g) = l.flatMap fun (a : α) => List.filterMap f (g a)
                                                                  theorem List.filter_flatMap {α : Type u_1} {β : Type u_2} (l : List α) (g : αList β) (f : βBool) :
                                                                  List.filter f (l.flatMap g) = l.flatMap fun (a : α) => List.filter f (g a)
                                                                  theorem List.flatMap_eq_foldl {α : Type u_1} {β : Type u_2} (f : αList β) (l : List α) :
                                                                  l.flatMap f = List.foldl (fun (acc : List β) (a : α) => acc ++ f a) [] l

                                                                  replicate #

                                                                  @[simp]
                                                                  theorem List.replicate_one {α✝ : Type u_1} {a : α✝} :
                                                                  @[simp]
                                                                  theorem List.mem_replicate {α : Type u_1} {a b : α} {n : Nat} :
                                                                  b List.replicate n a n 0 b = a
                                                                  @[simp, deprecated List.mem_replicate]
                                                                  theorem List.contains_replicate {α : Type u_1} [BEq α] {n : Nat} {a b : α} :
                                                                  (List.replicate n b).contains a = (a == b && !n == 0)
                                                                  @[simp, deprecated List.mem_replicate]
                                                                  theorem List.decide_mem_replicate {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {n : Nat} :
                                                                  decide (b List.replicate n a) = (decide ¬(n == 0) = true && b == a)
                                                                  theorem List.eq_of_mem_replicate {α : Type u_1} {a b : α} {n : Nat} (h : b List.replicate n a) :
                                                                  b = a
                                                                  theorem List.forall_mem_replicate {α : Type u_1} {p : αProp} {a : α} {n : Nat} :
                                                                  (∀ (b : α), b List.replicate n ap b) n = 0 p a
                                                                  @[simp]
                                                                  theorem List.replicate_succ_ne_nil {α : Type u_1} (n : Nat) (a : α) :
                                                                  List.replicate (n + 1) a []
                                                                  @[simp]
                                                                  theorem List.replicate_eq_nil_iff {α : Type u_1} {n : Nat} (a : α) :
                                                                  List.replicate n a = [] n = 0
                                                                  @[reducible, inline, deprecated List.replicate_eq_nil_iff]
                                                                  abbrev List.replicate_eq_nil {α : Type u_1} {n : Nat} (a : α) :
                                                                  List.replicate n a = [] n = 0
                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem List.getElem_replicate {α : Type u_1} (a : α) {n m : Nat} (h : m < (List.replicate n a).length) :
                                                                    (List.replicate n a)[m] = a
                                                                    @[deprecated List.getElem_replicate]
                                                                    theorem List.get_replicate {α : Type u_1} (a : α) {n : Nat} (m : Fin (List.replicate n a).length) :
                                                                    (List.replicate n a).get m = a
                                                                    theorem List.getElem?_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} :
                                                                    (List.replicate n a)[m]? = if m < n then some a else none
                                                                    @[simp]
                                                                    theorem List.getElem?_replicate_of_lt {α✝ : Type u_1} {a : α✝} {n m : Nat} (h : m < n) :
                                                                    (List.replicate n a)[m]? = some a
                                                                    theorem List.head?_replicate {α : Type u_1} (a : α) (n : Nat) :
                                                                    (List.replicate n a).head? = if n = 0 then none else some a
                                                                    @[simp]
                                                                    theorem List.head_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} (w : List.replicate n a []) :
                                                                    (List.replicate n a).head w = a
                                                                    @[simp]
                                                                    theorem List.tail_replicate {α : Type u_1} (n : Nat) (a : α) :
                                                                    (List.replicate n a).tail = List.replicate (n - 1) a
                                                                    @[simp]
                                                                    theorem List.replicate_inj {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} {b : α✝} :
                                                                    List.replicate n a = List.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 = List.replicate l.length a
                                                                    theorem List.eq_replicate_iff {α : Type u_1} {a : α} {n : Nat} {l : List α} :
                                                                    l = List.replicate n a l.length = n ∀ (b : α), b lb = a
                                                                    @[reducible, inline, deprecated List.eq_replicate_iff]
                                                                    abbrev List.eq_replicate {α : Type u_1} {a : α} {n : Nat} {l : List α} :
                                                                    l = List.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 : β} :
                                                                      List.map f l = List.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 : β) :
                                                                      List.map (Function.const α x) = fun (x_1 : List α) => List.replicate x_1.length x
                                                                      theorem List.map_const' {α : Type u_1} {β : Type u_2} (l : List α) (b : β) :
                                                                      List.map (fun (x : α) => b) l = List.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} :
                                                                      (List.replicate n a).set i a = List.replicate n a
                                                                      @[simp]
                                                                      theorem List.append_replicate_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} :
                                                                      theorem List.append_eq_replicate_iff {α : Type u_1} {n : Nat} {l₁ l₂ : List α} {a : α} :
                                                                      l₁ ++ l₂ = List.replicate n a l₁.length + l₂.length = n l₁ = List.replicate l₁.length a l₂ = List.replicate l₂.length a
                                                                      @[reducible, inline, deprecated List.append_eq_replicate_iff]
                                                                      abbrev List.append_eq_replicate {α : Type u_1} {n : Nat} {l₁ l₂ : List α} {a : α} :
                                                                      l₁ ++ l₂ = List.replicate n a l₁.length + l₂.length = n l₁ = List.replicate l₁.length a l₂ = List.replicate l₂.length a
                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem List.map_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝α✝¹} :
                                                                        theorem List.filter_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {p : α✝Bool} :
                                                                        List.filter p (List.replicate n a) = if p a = true then List.replicate n a else []
                                                                        @[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 β} :
                                                                        List.filterMap f (List.replicate n a) = match f a with | none => [] | some b => List.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) :
                                                                        @[simp]
                                                                        theorem List.filterMap_replicate_of_isSome {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : αOption β} (h : (f a).isSome = true) :
                                                                        @[simp]
                                                                        theorem List.filterMap_replicate_of_none {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : αOption β} (h : f a = none) :
                                                                        @[simp]
                                                                        theorem List.flatten_replicate_nil {n : Nat} {α : Type u_1} :
                                                                        (List.replicate n []).flatten = []
                                                                        @[simp]
                                                                        theorem List.flatten_replicate_singleton {n : Nat} {α✝ : Type u_1} {a : α✝} :
                                                                        (List.replicate n [a]).flatten = List.replicate n a
                                                                        @[simp]
                                                                        theorem List.flatten_replicate_replicate {n m : Nat} {α✝ : Type u_1} {a : α✝} :
                                                                        (List.replicate n (List.replicate m a)).flatten = List.replicate (n * m) a
                                                                        theorem List.flatMap_replicate {α : Type u_1} {n : Nat} {a : α} {β : Type u_2} (f : αList β) :
                                                                        (List.replicate n a).flatMap f = (List.replicate n (f a)).flatten
                                                                        @[simp]
                                                                        theorem List.isEmpty_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} :
                                                                        (List.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 = List.replicate n a 0 < n) ∃ (n : Nat), ∃ (a : α), ∃ (b : α), ∃ (l' : List α), l = List.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.

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

                                                                        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 []
                                                                        theorem List.getElem?_reverse' {α : Type u_1} {l : List α} (i j : Nat) :
                                                                        i + j + 1 = l.lengthl.reverse[i]? = l[j]?

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

                                                                        @[deprecated List.getElem?_reverse']
                                                                        theorem List.get?_reverse' {α : Type u_1} {l : List α} (i j : Nat) (h : i + j + 1 = l.length) :
                                                                        l.reverse.get? i = l.get? j
                                                                        @[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]
                                                                        @[deprecated List.getElem?_reverse]
                                                                        theorem List.get?_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.length) :
                                                                        l.reverse.get? i = l.get? (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]
                                                                        @[reducible, inline, deprecated List.reverse_eq_cons_iff]
                                                                        abbrev List.reverse_eq_cons {α : Type u_1} {xs : List α} {a : α} {ys : List α} :
                                                                        xs.reverse = a :: ys xs = ys.reverse ++ [a]
                                                                        Equations
                                                                        Instances For
                                                                          @[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_mem_getLast? {α : Type u_1} {l : List α} {a : α} (h : a l.getLast?) :
                                                                          a l
                                                                          @[simp]
                                                                          theorem List.map_reverse {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                                                                          List.map f l.reverse = (List.map f l).reverse
                                                                          @[deprecated List.map_reverse]
                                                                          theorem List.reverse_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                                                                          (List.map f l).reverse = List.map f l.reverse
                                                                          @[simp]
                                                                          theorem List.filter_reverse {α : Type u_1} (p : αBool) (l : List α) :
                                                                          List.filter p l.reverse = (List.filter p l).reverse
                                                                          @[simp]
                                                                          theorem List.filterMap_reverse {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
                                                                          List.filterMap f l.reverse = (List.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
                                                                          @[reducible, inline, deprecated List.reverse_eq_append_iff]
                                                                          abbrev List.reverse_eq_append {α : Type u_1} {xs ys zs : List α} :
                                                                          xs.reverse = ys ++ zs xs = zs.reverse ++ ys.reverse
                                                                          Equations
                                                                          Instances For
                                                                            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 = (List.map List.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 = (List.map List.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 β) :
                                                                            (l.flatMap f).reverse = l.reverse.flatMap (List.reverse f)
                                                                            theorem List.flatMap_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
                                                                            l.reverse.flatMap f = (l.flatMap (List.reverse f)).reverse
                                                                            @[simp]
                                                                            theorem List.reverseAux_eq {α : Type u_1} (as bs : List α) :
                                                                            as.reverseAux bs = as.reverse ++ bs
                                                                            @[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 : β) :
                                                                            List.foldrM f b l.reverse = List.foldlM (fun (x : β) (y : α) => f y x) b l
                                                                            @[simp]
                                                                            theorem List.foldl_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : βαβ) (b : β) :
                                                                            List.foldl f b l.reverse = List.foldr (fun (x : α) (y : β) => f y x) b l
                                                                            @[simp]
                                                                            theorem List.foldr_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : αββ) (b : β) :
                                                                            List.foldr f b l.reverse = List.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 : β) :
                                                                            List.foldl f b l = List.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 : β) :
                                                                            List.foldr f b l = List.foldl (fun (x : β) (y : α) => f y x) b l.reverse
                                                                            @[simp]
                                                                            theorem List.reverse_replicate {α : Type u_1} (n : Nat) (a : α) :
                                                                            (List.replicate n a).reverse = List.replicate n a

                                                                            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
                                                                            theorem List.getLast_eq_iff_getLast_eq_some {α : Type u_1} {a : α} {xs : List α} (h : xs []) :
                                                                            xs.getLast h = a xs.getLast? = some a
                                                                            @[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 []
                                                                            theorem List.mem_of_getLast?_eq_some {α : Type u_1} {xs : List α} {a : α} (h : xs.getLast? = some a) :
                                                                            a xs
                                                                            @[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) :
                                                                            (List.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) :
                                                                            (List.filterMap f l).getLast = b
                                                                            theorem List.getLast?_flatMap {α : Type u_1} {β : Type u_2} {L : List α} {f : αList β} :
                                                                            (L.flatMap f).getLast? = List.findSome? (fun (a : α) => (f a).getLast?) L.reverse
                                                                            theorem List.getLast?_flatten {α : Type u_1} {L : List (List α)} :
                                                                            L.flatten.getLast? = List.findSome? (fun (l : List α) => l.getLast?) L.reverse
                                                                            theorem List.getLast?_replicate {α : Type u_1} (a : α) (n : Nat) :
                                                                            (List.replicate n a).getLast? = if n = 0 then none else some a
                                                                            @[simp]
                                                                            theorem List.getLast_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} (w : List.replicate n a []) :
                                                                            (List.replicate n a).getLast w = a

                                                                            Additional operations #

                                                                            leftpad #

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

                                                                            List membership #

                                                                            elem / contains #

                                                                            theorem List.elem_cons_self {α : Type u_1} {as : List α} [BEq α] [LawfulBEq α] {a : α} :
                                                                            List.elem a (a :: as) = true
                                                                            @[simp]
                                                                            theorem List.contains_cons {α : Type u_1} {a : α} {as : List α} {x : α} [BEq α] :
                                                                            (a :: as).contains x = (x == a || as.contains x)
                                                                            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
                                                                            theorem List.contains_iff_mem {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} :
                                                                            l.contains a = true a l

                                                                            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 α) :
                                                                            theorem List.partition_eq_filter_filter.aux {α : Type u_1} (p : αBool) (l : List α) {as bs : List α} :
                                                                            List.partition.loop p l (as, bs) = (as.reverse ++ List.filter p l, bs.reverse ++ List.filter (not p) l)
                                                                            theorem List.mem_partition {α✝ : Type u_1} {l : List α✝} {a : α✝} {p : α✝Bool} :
                                                                            a l a (List.partition p l).fst a (List.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]
                                                                            @[deprecated List.getElem_dropLast]
                                                                            theorem List.get_dropLast {α : Type u_1} (xs : List α) (i : Fin xs.dropLast.length) :
                                                                            xs.dropLast.get i = xs.get 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 α) :
                                                                            List.map f l.dropLast = (List.map f l).dropLast
                                                                            @[simp]
                                                                            theorem List.dropLast_append_of_ne_nil {α : Type u} {l : List α} (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 : α) :
                                                                            (List.replicate n a).dropLast = List.replicate (n - 1) a
                                                                            @[simp]
                                                                            theorem List.dropLast_cons_self_replicate {α : Type u_1} (n : Nat) (a : α) :
                                                                            (a :: List.replicate n a).dropLast = List.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 α} (n : Nat) (l acc : List α) :
                                                                            List.splitAt.go l xs n acc = if n < xs.length then (acc.reverse ++ List.take n xs, List.drop n xs) else (l, [])

                                                                            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_of_not_mem {α : Type u_1} [BEq α] {a b : α} {l : List α} (h : (!List.elem a l) = true) :
                                                                            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 List.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 List.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 α} {n : Nat} :
                                                                            (List.take n l).replace a b = List.take n (l.replace a b)
                                                                            @[simp]
                                                                            theorem List.replace_replicate_self {α : Type u_1} [BEq α] {n : Nat} {b : α} [LawfulBEq α] {a : α} (h : 0 < n) :
                                                                            (List.replicate n a).replace a b = b :: List.replicate (n - 1) a
                                                                            @[simp]
                                                                            theorem List.replace_replicate_ne {α : Type u_1} [BEq α] {n : Nat} {a b c : α} (h : (!b == a) = true) :
                                                                            (List.replicate n a).replace b c = List.replicate n a

                                                                            insert #

                                                                            @[simp]
                                                                            theorem List.insert_nil {α : Type u_1} [BEq α] (a : α) :
                                                                            List.insert a [] = [a]
                                                                            @[simp]
                                                                            theorem List.insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a 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
                                                                            @[simp]
                                                                            theorem List.mem_insert_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
                                                                            theorem List.mem_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {l : List α} (h : a 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_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) :
                                                                            @[simp]
                                                                            theorem List.insert_replicate_ne {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b : α} (h : (!b == a) = true) :

                                                                            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} :
                                                                            (List.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} :
                                                                            (List.map f l).all p = l.all (p f)
                                                                            @[simp]
                                                                            theorem List.any_filter {α : Type u_1} {l : List α} {p q : αBool} :
                                                                            (List.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} :
                                                                            (List.filter p l).all q = l.all fun (a : α) => decide (p a = trueq a = true)
                                                                            @[simp]
                                                                            theorem List.any_filterMap {α : Type u_1} {β : Type u_2} {l : List α} {f : αOption β} {p : βBool} :
                                                                            (List.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} :
                                                                            (List.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} {x y : List α} :
                                                                            (x ++ y).any f = (x.any f || y.any f)
                                                                            @[simp]
                                                                            theorem List.all_append {α : Type u_1} {f : αBool} {x y : List α} :
                                                                            (x ++ y).all f = (x.all f && y.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
                                                                            @[reducible, inline, deprecated List.any_flatten]
                                                                            abbrev List.any_join {α : Type u_1} {f : αBool} {l : List (List α)} :
                                                                            l.flatten.any f = l.any fun (x : List α) => x.any f
                                                                            Equations
                                                                            Instances For
                                                                              @[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
                                                                              @[reducible, inline, deprecated List.all_flatten]
                                                                              abbrev List.all_join {α : Type u_1} {f : αBool} {l : List (List α)} :
                                                                              l.flatten.all f = l.all fun (x : List α) => x.all f
                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem List.any_flatMap {α : Type u_1} {β : Type u_2} {p : βBool} {l : List α} {f : αList β} :
                                                                                (l.flatMap f).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 β} :
                                                                                (l.flatMap f).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 : α} :
                                                                                (List.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 : α} :
                                                                                (List.replicate n a).all f = if n = 0 then true else f a
                                                                                @[simp]
                                                                                theorem List.any_insert {α : Type u_1} {f : αBool} [BEq α] [LawfulBEq α] {l : List α} {a : α} :
                                                                                (List.insert a l).any f = (f a || l.any f)
                                                                                @[simp]
                                                                                theorem List.all_insert {α : Type u_1} {f : αBool} [BEq α] [LawfulBEq α] {l : List α} {a : α} :
                                                                                (List.insert a l).all f = (f a && l.all f)

                                                                                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?_zero {α : Type u_1} (l : List α) :
                                                                                l.get? 0 = 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.get!_of_get? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} :
                                                                                l.get? n = some al.get! n = a
                                                                                theorem List.get!_len_le {α : Type u_1} [Inhabited α] {l : List α} {n : Nat} :
                                                                                l.length nl.get! n = default
                                                                                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 : α} {n : Nat} [Inhabited α] {l : List α} :
                                                                                (a :: l)[n + 1]! = l[n]!
                                                                                theorem List.getElem!_of_getElem? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} :
                                                                                l[n]? = some al[n]! = 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?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a l) :
                                                                                ∃ (n : Nat), l.get? n = some a
                                                                                theorem List.get_mem {α : Type u_1} (l : List α) (n : Fin l.length) :
                                                                                l.get n l
                                                                                theorem List.mem_of_get? {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l.get? n = some a) :
                                                                                a l
                                                                                theorem List.mem_iff_get {α : Type u_1} {a : α} {l : List α} :
                                                                                a l ∃ (n : Fin l.length), l.get n = a
                                                                                theorem List.mem_iff_get? {α : Type u_1} {a : α} {l : List α} :
                                                                                a l ∃ (n : Nat), l.get? n = some a

                                                                                Deprecations #

                                                                                @[deprecated List.getD_eq_getElem?_getD]
                                                                                theorem List.getD_eq_get? {α : Type u_1} (l : List α) (n : Nat) (a : α) :
                                                                                l.getD n a = (l.get? n).getD a
                                                                                @[deprecated List.getElem_singleton]
                                                                                theorem List.get_singleton {α : Type u_1} (a : α) (n : Fin 1) :
                                                                                [a].get n = a
                                                                                @[deprecated List.getElem?_concat_length]
                                                                                theorem List.get?_concat_length {α : Type u_1} (l : List α) (a : α) :
                                                                                (l ++ [a]).get? l.length = some a
                                                                                @[deprecated List.getElem_set_self]
                                                                                theorem List.get_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
                                                                                (l.set i a).get i, h = a
                                                                                @[deprecated List.getElem_set_ne]
                                                                                theorem List.get_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).get j, hj = l.get j,
                                                                                @[deprecated List.getElem_set]
                                                                                theorem List.get_set {α : Type u_1} {l : List α} {m n : Nat} {a : α} (h : n < (l.set m a).length) :
                                                                                (l.set m a).get n, h = if m = n then a else l.get n,
                                                                                @[reducible, inline, deprecated List.cons_inj_right]
                                                                                abbrev List.cons_inj {α : Type u_1} (a : α) {l l' : List α} :
                                                                                a :: l = a :: l' l = l'
                                                                                Equations
                                                                                Instances For
                                                                                  @[reducible, inline, deprecated List.ne_nil_of_length_eq_add_one]
                                                                                  abbrev List.ne_nil_of_length_eq_succ {α✝ : Type u_1} {l : List α✝} {n : Nat} :
                                                                                  l.length = n + 1l []
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[deprecated]
                                                                                    theorem List.get_cons_cons_one {α✝ : Type u_1} {a₁ a₂ : α✝} {as : List α✝} :
                                                                                    (a₁ :: a₂ :: as).get 1 = a₂
                                                                                    @[deprecated List.filter_flatten]
                                                                                    theorem List.join_map_filter {α : Type u_1} (p : αBool) (l : List (List α)) :
                                                                                    (List.map (List.filter p) l).flatten = List.filter p l.flatten
                                                                                    @[reducible, inline, deprecated List.getElem_eq_getElem?_get]
                                                                                    abbrev List.getElem_eq_getElem? {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) :
                                                                                    l[i] = l[i]?.get
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, inline, deprecated List.flatten_eq_nil_iff]
                                                                                      abbrev List.join_eq_nil {α : Type u_1} {L : List (List α)} :
                                                                                      L.flatten = [] ∀ (l : List α), l Ll = []
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, inline, deprecated List.flatten_ne_nil_iff]
                                                                                        abbrev List.join_ne_nil {α : Type u_1} {xs : List (List α)} :
                                                                                        xs.flatten [] ∃ (x : List α), x xs x []
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[reducible, inline, deprecated List.flatten_eq_cons_iff]
                                                                                          abbrev List.join_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
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[reducible, inline, deprecated List.flatten_eq_cons_iff]
                                                                                            abbrev List.join_eq_cons {α : 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
                                                                                            Equations
                                                                                            Instances For
                                                                                              @[reducible, inline, deprecated List.flatten_eq_append_iff]
                                                                                              abbrev List.join_eq_append {α : 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
                                                                                              Equations
                                                                                              Instances For
                                                                                                @[reducible, inline, deprecated List.mem_of_getElem?]
                                                                                                abbrev List.getElem?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) :
                                                                                                a l
                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[reducible, inline, deprecated List.mem_of_get?]
                                                                                                  abbrev List.get?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l.get? n = some a) :
                                                                                                  a l
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[reducible, inline, deprecated List.getElem_set_self]
                                                                                                    abbrev List.getElem_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
                                                                                                    (l.set i a)[i] = a
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[reducible, inline, deprecated List.getElem?_set_self]
                                                                                                      abbrev List.getElem?_set_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < l.length) :
                                                                                                      (l.set i a)[i]? = some a
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[reducible, inline, deprecated List.set_eq_nil_iff]
                                                                                                        abbrev List.set_eq_nil {α : Type u_1} {l : List α} (n : Nat) (a : α) :
                                                                                                        l.set n a = [] l = []
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[reducible, inline, deprecated List.flatten_nil]
                                                                                                          abbrev List.join_nil {α : Type u_1} :
                                                                                                          [].flatten = []
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[reducible, inline, deprecated List.flatten_cons]
                                                                                                            abbrev List.join_cons {α✝ : Type u_1} {l : List α✝} {ls : List (List α✝)} :
                                                                                                            (l :: ls).flatten = l ++ ls.flatten
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[reducible, inline, deprecated List.length_flatten]
                                                                                                              abbrev List.length_join {α : Type u_1} (L : List (List α)) :
                                                                                                              L.flatten.length = (List.map List.length L).sum
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[reducible, inline, deprecated List.flatten_singleton]
                                                                                                                abbrev List.join_singleton {α : Type u_1} (l : List α) :
                                                                                                                [l].flatten = l
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[reducible, inline, deprecated List.mem_flatten]
                                                                                                                  abbrev List.mem_join {α : Type u_1} {a : α} {L : List (List α)} :
                                                                                                                  a L.flatten ∃ (l : List α), l L a l
                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[reducible, inline, deprecated List.flatten_eq_nil_iff]
                                                                                                                    abbrev List.join_eq_nil_iff {α : Type u_1} {L : List (List α)} :
                                                                                                                    L.flatten = [] ∀ (l : List α), l Ll = []
                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[reducible, inline, deprecated List.flatten_ne_nil_iff]
                                                                                                                      abbrev List.join_ne_nil_iff {α : Type u_1} {xs : List (List α)} :
                                                                                                                      xs.flatten [] ∃ (x : List α), x xs x []
                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[reducible, inline, deprecated List.exists_of_mem_flatten]
                                                                                                                        abbrev List.exists_of_mem_join {α✝ : Type u_1} {L : List (List α✝)} {a : α✝} :
                                                                                                                        a L.flatten∃ (l : List α✝), l L a l
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[reducible, inline, deprecated List.mem_flatten_of_mem]
                                                                                                                          abbrev List.mem_join_of_mem {α✝ : Type u_1} {L : List (List α✝)} {l : List α✝} {a : α✝} (lL : l L) (al : a l) :
                                                                                                                          a L.flatten
                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[reducible, inline, deprecated List.forall_mem_flatten]
                                                                                                                            abbrev List.forall_mem_join {α : Type u_1} {p : αProp} {L : List (List α)} :
                                                                                                                            (∀ (x : α), x L.flattenp x) ∀ (l : List α), l L∀ (x : α), x lp x
                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[reducible, inline, deprecated List.flatten_eq_flatMap]
                                                                                                                              abbrev List.join_eq_bind {α : Type u_1} {L : List (List α)} :
                                                                                                                              L.flatten = L.flatMap id
                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                @[reducible, inline, deprecated List.head?_flatten]
                                                                                                                                abbrev List.head?_join {α : Type u_1} {L : List (List α)} :
                                                                                                                                L.flatten.head? = List.findSome? (fun (l : List α) => l.head?) L
                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  @[reducible, inline, deprecated List.foldl_flatten]
                                                                                                                                  abbrev List.foldl_join {β : Type u_1} {α : Type u_2} (f : βαβ) (b : β) (L : List (List α)) :
                                                                                                                                  List.foldl f b L.flatten = List.foldl (fun (b : β) (l : List α) => List.foldl f b l) b L
                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    @[reducible, inline, deprecated List.foldr_flatten]
                                                                                                                                    abbrev List.foldr_join {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (L : List (List α)) :
                                                                                                                                    List.foldr f b L.flatten = List.foldr (fun (l : List α) (b : β) => List.foldr f b l) b L
                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      @[reducible, inline, deprecated List.map_flatten]
                                                                                                                                      abbrev List.map_join {α : Type u_1} {β : Type u_2} (f : αβ) (L : List (List α)) :
                                                                                                                                      List.map f L.flatten = (List.map (List.map f) L).flatten
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[reducible, inline, deprecated List.filterMap_flatten]
                                                                                                                                        abbrev List.filterMap_join {α : Type u_1} {β : Type u_2} (f : αOption β) (L : List (List α)) :
                                                                                                                                        List.filterMap f L.flatten = (List.map (List.filterMap f) L).flatten
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[reducible, inline, deprecated List.filter_flatten]
                                                                                                                                          abbrev List.filter_join {α : Type u_1} (p : αBool) (L : List (List α)) :
                                                                                                                                          List.filter p L.flatten = (List.map (List.filter p) L).flatten
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            @[reducible, inline, deprecated List.flatten_filter_not_isEmpty]
                                                                                                                                            abbrev List.join_filter_not_isEmpty {α : Type u_1} {L : List (List α)} :
                                                                                                                                            (List.filter (fun (l : List α) => !l.isEmpty) L).flatten = L.flatten
                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[reducible, inline, deprecated List.flatten_filter_ne_nil]
                                                                                                                                              abbrev List.join_filter_ne_nil {α : Type u_1} [DecidablePred fun (l : List α) => l []] {L : List (List α)} :
                                                                                                                                              (List.filter (fun (l : List α) => decide (l [])) L).flatten = L.flatten
                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[reducible, inline, deprecated List.flatten_append]
                                                                                                                                                abbrev List.join_append {α : Type u_1} (L₁ L₂ : List (List α)) :
                                                                                                                                                (L₁ ++ L₂).flatten = L₁.flatten ++ L₂.flatten
                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[reducible, inline, deprecated List.flatten_concat]
                                                                                                                                                  abbrev List.join_concat {α : Type u_1} (L : List (List α)) (l : List α) :
                                                                                                                                                  (L ++ [l]).flatten = L.flatten ++ l
                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[reducible, inline, deprecated List.flatten_flatten]
                                                                                                                                                    abbrev List.join_join {α : Type u_1} {L : List (List (List α))} :
                                                                                                                                                    L.flatten.flatten = (List.map List.flatten L).flatten
                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[reducible, inline, deprecated List.flatten_eq_append_iff]
                                                                                                                                                      abbrev List.join_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
                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        @[reducible, inline, deprecated List.eq_iff_flatten_eq]
                                                                                                                                                        abbrev List.eq_iff_join_eq {α : Type u_1} {L L' : List (List α)} :
                                                                                                                                                        L = L' L.flatten = L'.flatten List.map List.length L = List.map List.length L'
                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[reducible, inline, deprecated List.flatten_replicate_nil]
                                                                                                                                                          abbrev List.join_replicate_nil {n : Nat} {α : Type u_1} :
                                                                                                                                                          (List.replicate n []).flatten = []
                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[reducible, inline, deprecated List.flatten_replicate_singleton]
                                                                                                                                                            abbrev List.join_replicate_singleton {n : Nat} {α✝ : Type u_1} {a : α✝} :
                                                                                                                                                            (List.replicate n [a]).flatten = List.replicate n a
                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[reducible, inline, deprecated List.flatten_replicate_replicate]
                                                                                                                                                              abbrev List.join_replicate_replicate {n m : Nat} {α✝ : Type u_1} {a : α✝} :
                                                                                                                                                              (List.replicate n (List.replicate m a)).flatten = List.replicate (n * m) a
                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                @[reducible, inline, deprecated List.reverse_flatten]
                                                                                                                                                                abbrev List.reverse_join {α : Type u_1} (L : List (List α)) :
                                                                                                                                                                L.flatten.reverse = (List.map List.reverse L).reverse.flatten
                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[reducible, inline, deprecated List.flatten_reverse]
                                                                                                                                                                  abbrev List.join_reverse {α : Type u_1} (L : List (List α)) :
                                                                                                                                                                  L.reverse.flatten = (List.map List.reverse L).flatten.reverse
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[reducible, inline, deprecated List.getLast?_flatten]
                                                                                                                                                                    abbrev List.getLast?_join {α : Type u_1} {L : List (List α)} :
                                                                                                                                                                    L.flatten.getLast? = List.findSome? (fun (l : List α) => l.getLast?) L.reverse
                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[reducible, inline, deprecated List.flatten_eq_flatMap]
                                                                                                                                                                      abbrev List.flatten_eq_bind {α : Type u_1} {L : List (List α)} :
                                                                                                                                                                      L.flatten = L.flatMap id
                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[reducible, inline, deprecated List.flatMap_def]
                                                                                                                                                                        abbrev List.bind_def {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
                                                                                                                                                                        l.flatMap f = (List.map f l).flatten
                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[reducible, inline, deprecated List.flatMap_id]
                                                                                                                                                                          abbrev List.bind_id {α : Type u_1} (l : List (List α)) :
                                                                                                                                                                          l.flatMap id = l.flatten
                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[reducible, inline, deprecated List.mem_flatMap]
                                                                                                                                                                            abbrev List.mem_bind {α : Type u_1} {β : Type u_2} {f : αList β} {b : β} {l : List α} :
                                                                                                                                                                            b l.flatMap f ∃ (a : α), a l b f a
                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[reducible, inline, deprecated List.exists_of_mem_flatMap]
                                                                                                                                                                              abbrev List.exists_of_mem_bind {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : αList β} :
                                                                                                                                                                              b l.flatMap f∃ (a : α), a l b f a
                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[reducible, inline, deprecated List.mem_flatMap_of_mem]
                                                                                                                                                                                abbrev List.mem_bind_of_mem {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : αList β} {a : α} (al : a l) (h : b f a) :
                                                                                                                                                                                b l.flatMap f
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[reducible, inline, deprecated List.flatMap_eq_nil_iff]
                                                                                                                                                                                  abbrev List.bind_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                                                                                                                                                  l.flatMap f = [] ∀ (x : α), x lf x = []
                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[reducible, inline, deprecated List.forall_mem_flatMap]
                                                                                                                                                                                    abbrev List.forall_mem_bind {β : Type u_1} {α : Type u_2} {p : βProp} {l : List α} {f : αList β} :
                                                                                                                                                                                    (∀ (x : β), x l.flatMap fp x) ∀ (a : α), a l∀ (b : β), b f ap b
                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      @[reducible, inline, deprecated List.flatMap_singleton]
                                                                                                                                                                                      abbrev List.bind_singleton {α : Type u_1} {β : Type u_2} (f : αList β) (x : α) :
                                                                                                                                                                                      [x].flatMap f = f x
                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        @[reducible, inline, deprecated List.flatMap_singleton']
                                                                                                                                                                                        abbrev List.bind_singleton' {α : Type u_1} (l : List α) :
                                                                                                                                                                                        (l.flatMap fun (x : α) => [x]) = l
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[reducible, inline, deprecated List.head?_flatMap]
                                                                                                                                                                                          abbrev List.head_bind {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                                                                                                                                                          (l.flatMap f).head? = List.findSome? (fun (a : α) => (f a).head?) l
                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[reducible, inline, deprecated List.flatMap_append]
                                                                                                                                                                                            abbrev List.bind_append {α : Type u_1} {β : Type u_2} (xs ys : List α) (f : αList β) :
                                                                                                                                                                                            (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f
                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[reducible, inline, deprecated List.flatMap_assoc]
                                                                                                                                                                                              abbrev List.bind_assoc {γ : Type u_1} {α : Type u_2} {β : Type u_3} (l : List α) (f : αList β) (g : βList γ) :
                                                                                                                                                                                              (l.flatMap f).flatMap g = l.flatMap fun (x : α) => (f x).flatMap g
                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[reducible, inline, deprecated List.map_flatMap]
                                                                                                                                                                                                abbrev List.map_bind {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : βγ) (g : αList β) (l : List α) :
                                                                                                                                                                                                List.map f (l.flatMap g) = l.flatMap fun (a : α) => List.map f (g a)
                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[reducible, inline, deprecated List.flatMap_map]
                                                                                                                                                                                                  abbrev List.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : βList γ) (l : List α) :
                                                                                                                                                                                                  (List.map f l).flatMap g = l.flatMap fun (a : α) => g (f a)
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    @[reducible, inline, deprecated List.map_eq_flatMap]
                                                                                                                                                                                                    abbrev List.map_eq_bind {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                                                                                                                                                                                                    List.map f l = l.flatMap fun (x : α) => [f x]
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      @[reducible, inline, deprecated List.filterMap_flatMap]
                                                                                                                                                                                                      abbrev List.filterMap_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : List α) (g : αList β) (f : βOption γ) :
                                                                                                                                                                                                      List.filterMap f (l.flatMap g) = l.flatMap fun (a : α) => List.filterMap f (g a)
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        @[reducible, inline, deprecated List.filter_flatMap]
                                                                                                                                                                                                        abbrev List.filter_bind {α : Type u_1} {β : Type u_2} (l : List α) (g : αList β) (f : βBool) :
                                                                                                                                                                                                        List.filter f (l.flatMap g) = l.flatMap fun (a : α) => List.filter f (g a)
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          @[reducible, inline, deprecated List.flatMap_eq_foldl]
                                                                                                                                                                                                          abbrev List.bind_eq_foldl {α : Type u_1} {β : Type u_2} (f : αList β) (l : List α) :
                                                                                                                                                                                                          l.flatMap f = List.foldl (fun (acc : List β) (a : α) => acc ++ f a) [] l
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            @[reducible, inline, deprecated List.flatMap_replicate]
                                                                                                                                                                                                            abbrev List.bind_replicate {α : Type u_1} {n : Nat} {a : α} {β : Type u_2} (f : αList β) :
                                                                                                                                                                                                            (List.replicate n a).flatMap f = (List.replicate n (f a)).flatten
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              @[reducible, inline, deprecated List.reverse_flatMap]
                                                                                                                                                                                                              abbrev List.reverse_bind {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
                                                                                                                                                                                                              (l.flatMap f).reverse = l.reverse.flatMap (List.reverse f)
                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                @[reducible, inline, deprecated List.flatMap_reverse]
                                                                                                                                                                                                                abbrev List.bind_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
                                                                                                                                                                                                                l.reverse.flatMap f = (l.flatMap (List.reverse f)).reverse
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  @[reducible, inline, deprecated List.getLast?_flatMap]
                                                                                                                                                                                                                  abbrev List.getLast?_bind {α : Type u_1} {β : Type u_2} {L : List α} {f : αList β} :
                                                                                                                                                                                                                  (L.flatMap f).getLast? = List.findSome? (fun (a : α) => (f a).getLast?) L.reverse
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    @[reducible, inline, deprecated List.any_flatMap]
                                                                                                                                                                                                                    abbrev List.any_bind {α : Type u_1} {β : Type u_2} {p : βBool} {l : List α} {f : αList β} :
                                                                                                                                                                                                                    (l.flatMap f).any p = l.any fun (a : α) => (f a).any p
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      @[reducible, inline, deprecated List.all_flatMap]
                                                                                                                                                                                                                      abbrev List.all_bind {α : Type u_1} {β : Type u_2} {p : βBool} {l : List α} {f : αList β} :
                                                                                                                                                                                                                      (l.flatMap f).all p = l.all fun (a : α) => (f a).all p
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        @[reducible, inline, deprecated List.get?_eq_none]
                                                                                                                                                                                                                        abbrev List.get?_len_le {α : Type u_1} {l : List α} {n : Nat} :
                                                                                                                                                                                                                        l.length nl.get? n = none
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          @[reducible, inline, deprecated List.getElem?_eq_some_iff]
                                                                                                                                                                                                                          abbrev List.getElem?_eq_some {α : Type u_1} {n : Nat} {a : α} {l : List α} :
                                                                                                                                                                                                                          l[n]? = some a ∃ (h : n < l.length), l[n] = a
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            @[reducible, inline, deprecated List.get?_eq_some_iff]
                                                                                                                                                                                                                            abbrev List.get?_eq_some {α✝ : Type u_1} {a : α✝} {l : List α✝} {n : Nat} :
                                                                                                                                                                                                                            l.get? n = some a ∃ (h : n < l.length), l.get n, h = a
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              @[deprecated LawfulGetElem.getElem?_def]
                                                                                                                                                                                                                              theorem List.getElem?_eq {α : Type u_1} (l : List α) (i : Nat) :
                                                                                                                                                                                                                              l[i]? = if h : i < l.length then some l[i] else none
                                                                                                                                                                                                                              @[reducible, inline, deprecated List.getElem?_eq_none]
                                                                                                                                                                                                                              abbrev List.getElem?_len_le {α✝ : Type u_1} {l : List α✝} {n : Nat} (h : l.length n) :
                                                                                                                                                                                                                              l[n]? = none
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For