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 = []

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₁ :: t₁ = h₂ :: t₂h₁ = h₂
theorem List.tail_eq_of_cons_eq :
∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂t₁ = t₂
theorem List.cons_inj_right {α : Type u_1} (a : α) {l : List α} {l' : List α} :
a :: l = a :: l' l = l'
@[reducible, inline, deprecated]
abbrev List.cons_inj {α : Type u_1} (a : α) {l : List α} {l' : List α} :
a :: l = a :: l' l = l'
Equations
Instances For
    theorem List.cons_eq_cons {α : Type u_1} {a : α} {b : α} {l : List α} {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.singleton_inj {α : Type u_1} {a : α} {b : α} :
    [a] = [b] a = b

    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 []
    @[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
      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]

      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]?.

      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
      @[deprecated]
      theorem List.get_cons_cons_one :
      ∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, (a₁ :: a₂ :: as).get 1 = a₂
      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?_len_le {α : 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 :
      ∀ {α : 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 :
      ∀ {α : 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]?
      @[simp]
      theorem List.get_eq_getElem {α : Type u_1} (l : List α) (i : Fin l.length) :
      l.get i = l[i]
      theorem List.getElem?_eq_some {α : Type u_1} {i : Nat} {a : α} {l : List α} :
      l[i]? = some a ∃ (h : i < l.length), l[i] = a
      theorem List.get_of_eq {α : Type u_1} {l : List α} {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 it 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].

      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
      @[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

      get! #

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

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

      getElem! #

      @[simp]
      theorem List.getElem!_nil {α : Type u_1} [Inhabited α] {n : Nat} :
      [][n]! = default
      @[simp]
      theorem List.getElem!_cons_zero {α : Type u_1} {a : α} [Inhabited α] {l : List α} :
      (a :: l)[0]! = a
      @[simp]
      theorem List.getElem!_cons_succ {α : Type u_1} {a : α} {n : Nat} [Inhabited α] {l : List α} :
      (a :: l)[n + 1]! = l[n]!

      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}, l.length nl[n]? = none
      theorem List.getElem?_eq {α : Type u_1} (l : List α) (i : Nat) :
      l[i]? = if h : i < l.length then some l[i] else 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
      @[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
        @[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?_len_le {α : Type u_1} {l : List α} {n : Nat} :
        l.length nl[n]? = none
        theorem List.getElem_of_eq {α : Type u_1} {l : List α} {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
        @[deprecated List.getElem_singleton]
        theorem List.get_singleton {α : Type u_1} (a : α) (n : Fin 1) :
        [a].get n = a
        theorem List.getElem_zero {α : Type u_1} {l : List α} (h : 0 < l.length) :
        l[0] = l.head
        theorem List.getElem!_of_getElem? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} :
        l[n]? = some al[n]! = a
        theorem List.ext_getElem?_iff {α : Type u_1} {l₁ : List α} {l₂ : List α} :
        l₁ = l₂ ∀ (n : Nat), l₁[n]? = l₂[n]?
        theorem List.ext_getElem? {α : Type u_1} {l₁ : List α} {l₂ : List α} (h : ∀ (n : Nat), l₁[n]? = l₂[n]?) :
        l₁ = l₂
        theorem List.ext_getElem {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁[n] = l₂[n]) :
        l₁ = l₂
        theorem List.ext_get {α : Type u_1} {l₁ : List α} {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₂
        @[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
        @[deprecated List.getElem?_concat_length]
        theorem List.get?_concat_length {α : Type u_1} (l : List α) (a : α) :
        (l ++ [a]).get? l.length = some a

        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.get_of_mem {α : Type u_1} {a : α} {l : List α} (h : a l) :
        ∃ (n : Fin l.length), l.get n = a
        theorem List.getElem?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a l) :
        ∃ (n : Nat), l[n]? = some a
        theorem List.get?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a l) :
        ∃ (n : Nat), l.get? n = some a
        @[simp]
        theorem List.getElem_mem {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) :
        l[n] l
        theorem List.get_mem {α : Type u_1} (l : List α) (n : Nat) (h : n < l.length) :
        l.get n, h l
        theorem List.getElem?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) :
        a l
        theorem List.get?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l.get? 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_get {α : Type u_1} {a : α} {l : List α} :
        a l ∃ (n : Fin l.length), l.get n = a
        theorem List.mem_iff_getElem? {α : Type u_1} {a : α} {l : List α} :
        a l ∃ (n : Nat), l[n]? = some a
        theorem List.mem_iff_get? {α : Type u_1} {a : α} {l : List α} :
        a l ∃ (n : Nat), l.get? 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_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
        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

        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
        @[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
          @[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
          @[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
          @[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
            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 : Nat} {j : Nat} (h : i j) {a : α} (hj : j < (l.set i a).length) :
            (l.set i a)[j] = l[j]
            @[deprecated List.getElem_set_ne]
            theorem List.get_set_ne {α : Type u_1} {l : List α} {i : Nat} {j : Nat} (h : i j) {a : α} (hj : j < (l.set i a).length) :
            (l.set i a).get j, hj = l.get j,
            @[simp]
            theorem List.getElem?_set_ne {α : Type u_1} {l : List α} {i : Nat} {j : Nat} (h : i j) {a : α} :
            (l.set i a)[j]? = l[j]?
            theorem List.getElem_set {α : Type u_1} {l : List α} {m : Nat} {n : Nat} {a : α} (h : n < (l.set m a).length) :
            (l.set m a)[n] = if m = n then a else l[n]
            @[deprecated List.getElem_set]
            theorem List.get_set {α : Type u_1} {l : List α} {m : Nat} {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,
            theorem List.getElem?_set {α : Type u_1} {l : List α} {i : Nat} {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 : Nat} {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 = []
            @[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
              theorem List.set_comm {α : Type u_1} (a : α) (b : α) {n : Nat} {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 α] :

              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₁ : List α} {l₂ : List α} {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₁ : List α} {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 : List α) (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 α) :

              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_map' {α : Type u} {β : Type u} (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} {β : Type u} (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.

                      getLast #

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

                      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.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 : List α) (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} {α_1 : Type u_2} {f : αα_1} {l : List α} {b : α_1}, 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 α} {α_1 : Type u_2} {f g : αα_1}, (∀ (a : α), a lf a = g a)List.map f l = List.map g l
                        theorem List.map_inj :
                        ∀ {α : Type u_1} {α_1 : Type u_2} {f g : αα_1}, List.map f = List.map g 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} {α_1 : Type u_2} {f : αα_1} {l : List α} {g : αα_1}, List.map f l = List.map g l ∀ (a : α), a lf a = g a
                              theorem List.map_eq_iff :
                              ∀ {α : Type u_1} {α_1 : Type u_2} {f : αα_1} {l : List α} {l' : List α_1}, 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 : List α) (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.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₁ : List α) (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 : αBool} {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 : αBool} {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} {α_1 : Type u_2} {f : αOption α_1} {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 : List α) (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} {α_1 : Type u_2} {f : αOption α_1} {xs : List α}, List.filterMap f xs = []∀ (x : α), x xsf x = none
                                          @[simp]
                                          theorem List.filterMap_eq_nil_iff :
                                          ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {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} {α_1 : Type u_2} {f : αOption α_1} {l : List α}, List.filterMap f l = [] ∀ (a : α), a lf a = none
                                          Equations
                                          Instances For
                                            theorem List.filterMap_eq_cons_iff :
                                            ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {l : List α} {b : α_1} {bs : List α_1}, 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} {α_1 : Type u_2} {f : αOption α_1} {l : List α} {b : α_1} {bs : List α_1}, 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₁ : List α} {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₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) :
                                              (l₁ ++ l₂)[n]? = l₁[n]?
                                              theorem List.getElem?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} :
                                              l₁.length n(l₁ ++ l₂)[n]? = l₂[n - l₁.length]?
                                              theorem List.getElem?_append {α : Type u_1} {l₁ : List α} {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₁ : List α} {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₁ : List α} {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₁ : List α} {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₁ : List α} {s₂ : List α} {t₁ : List α} {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 α}, s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengtht₁ = t₂
                                              theorem List.append_inj_left :
                                              ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengths₁ = s₂
                                              theorem List.append_inj' :
                                              ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = 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 α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengtht₁ = 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 α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = 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₁ : List α} {t₂ : List α} (s : List α) :
                                              s ++ t₁ = s ++ t₂ t₁ = t₂
                                              theorem List.append_left_inj {α : Type u_1} {s₁ : List α} {s₂ : List α} (t : List α) :
                                              s₁ ++ t = s₂ ++ t s₁ = s₂
                                              @[simp]
                                              theorem List.append_left_eq_self {α : Type u_1} {x : List α} {y : List α} :
                                              x ++ y = y x = []
                                              @[simp]
                                              theorem List.self_eq_append_left {α : Type u_1} {x : List α} {y : List α} :
                                              y = x ++ y x = []
                                              @[simp]
                                              theorem List.append_right_eq_self {α : Type u_1} {x : List α} {y : List α} :
                                              x ++ y = x y = []
                                              @[simp]
                                              theorem List.self_eq_append_right {α : Type u_1} {x : List α} {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₁ : List α} {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 : List α) (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 : List α) (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₁ : List α} {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' : List α} {l : List α} {w₁ : l ++ l' []} (w₂ : l []) :
                                              (l ++ l').head w₁ = l.head w₂
                                              theorem List.head_append {α : Type u_1} {l₁ : List α} {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₁ : List α} {l₂ : List α} (h : l₁ []) :
                                              (l₁ ++ l₂).head = l₁.head h
                                              theorem List.head_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} (w : l₁ ++ l₂ []) (h : l₁ = []) :
                                              (l₁ ++ l₂).head w = l₂.head
                                              @[simp]
                                              theorem List.head?_append {α : Type u_1} {l' : List α} {l : List α} :
                                              (l ++ l').head? = l.head?.or l'.head?
                                              theorem List.tail?_append {α : Type u_1} {l : List α} {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 : List α} {l' : List α} :
                                              l [](l ++ l').tail? = some (l.tail ++ l')
                                              theorem List.tail_append {α : Type u_1} {l : List α} {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 : List α} {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 : List α} {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 : List α} {b : List α} {c : List α} {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₁ : List α} {s₂ : List α} {t₁ : List α} {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 α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = s₂ t₁ = t₂
                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem List.mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} :
                                                          a s ++ t a s a t
                                                          theorem List.not_mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} (h₁ : ¬a s) (h₂ : ¬a t) :
                                                          ¬a s ++ t
                                                          theorem List.mem_append_eq {α : Type u_1} (a : α) (s : List α) (t : List α) :
                                                          (a s ++ t) = (a s a t)
                                                          theorem List.mem_append_left {α : Type u_1} {a : α} {l₁ : List α} (l₂ : List α) (h : a l₁) :
                                                          a l₁ ++ l₂
                                                          theorem List.mem_append_right {α : Type u_1} {a : α} (l₁ : List α) {l₂ : List α} (h : a l₂) :
                                                          a l₁ ++ l₂
                                                          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₁ : List α} {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 : List α} {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 : List α} {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 : List α} {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 : List α) (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 : List α) (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 : List α) (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₁ : List β} {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₁ : List β} {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₁ : List β} {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₁ : List β} {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 : List α} {L₁ : List α} {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₁ : List α} {L₂ : List α} {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₁ : List α} {L₂ : List α} {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₁ : List α) (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₁ : List β} {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₁ : List β} {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₁ : List β} {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₁ : List β} {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₁ : List α} {l₂ : List α} :
                                                                    l₁.concat a = l₂.concat bl₁ = l₂
                                                                    theorem List.last_eq_of_concat_eq {α : Type u_1} {a : α} {b : α} {l₁ : List α} {l₂ : List α} :
                                                                    l₁.concat a = l₂.concat ba = b
                                                                    theorem List.concat_inj {α : Type u_1} {a : α} {b : α} {l : List α} {l' : List α} :
                                                                    l.concat a = l'.concat b l = l' a = b
                                                                    theorem List.concat_inj_left {α : Type u_1} {l : List α} {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 : List α} {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₁ : List α) (l₂ : List α) :
                                                                      l₁.concat a ++ l₂ = l₁ ++ a :: l₂
                                                                      theorem List.append_concat {α : Type u_1} (a : α) (l₁ : List α) (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

                                                                      join #

                                                                      @[simp]
                                                                      theorem List.length_join {α : Type u_1} (L : List (List α)) :
                                                                      L.join.length = Nat.sum (List.map List.length L)
                                                                      theorem List.join_singleton {α : Type u_1} (l : List α) :
                                                                      [l].join = l
                                                                      @[simp]
                                                                      theorem List.mem_join {α : Type u_1} {a : α} {L : List (List α)} :
                                                                      a L.join ∃ (l : List α), l L a l
                                                                      @[simp]
                                                                      theorem List.join_eq_nil_iff {α : Type u_1} {L : List (List α)} :
                                                                      L.join = [] ∀ (l : List α), l Ll = []
                                                                      @[reducible, inline, deprecated List.join_eq_nil_iff]
                                                                      abbrev List.join_eq_nil {α : Type u_1} {L : List (List α)} :
                                                                      L.join = [] ∀ (l : List α), l Ll = []
                                                                      Equations
                                                                      Instances For
                                                                        theorem List.join_ne_nil_iff {α : Type u_1} {xs : List (List α)} :
                                                                        xs.join [] ∃ (x : List α), x xs x []
                                                                        @[reducible, inline, deprecated List.join_ne_nil_iff]
                                                                        abbrev List.join_ne_nil {α : Type u_1} {xs : List (List α)} :
                                                                        xs.join [] ∃ (x : List α), x xs x []
                                                                        Equations
                                                                        Instances For
                                                                          theorem List.exists_of_mem_join :
                                                                          ∀ {α : Type u_1} {L : List (List α)} {a : α}, a L.join∃ (l : List α), l L a l
                                                                          theorem List.mem_join_of_mem :
                                                                          ∀ {α : Type u_1} {L : List (List α)} {l : List α} {a : α}, l La la L.join
                                                                          theorem List.forall_mem_join {α : Type u_1} {p : αProp} {L : List (List α)} :
                                                                          (∀ (x : α), x L.joinp x) ∀ (l : List α), l L∀ (x : α), x lp x
                                                                          theorem List.join_eq_bind {α : Type u_1} {L : List (List α)} :
                                                                          L.join = L.bind id
                                                                          theorem List.head?_join {α : Type u_1} {L : List (List α)} :
                                                                          L.join.head? = List.findSome? (fun (l : List α) => l.head?) L
                                                                          theorem List.foldl_join {β : Type u_1} {α : Type u_2} (f : βαβ) (b : β) (L : List (List α)) :
                                                                          List.foldl f b L.join = List.foldl (fun (b : β) (l : List α) => List.foldl f b l) b L
                                                                          theorem List.foldr_join {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (L : List (List α)) :
                                                                          List.foldr f b L.join = List.foldr (fun (l : List α) (b : β) => List.foldr f b l) b L
                                                                          @[simp]
                                                                          theorem List.map_join {α : Type u_1} {β : Type u_2} (f : αβ) (L : List (List α)) :
                                                                          List.map f L.join = (List.map (List.map f) L).join
                                                                          @[simp]
                                                                          theorem List.filterMap_join {α : Type u_1} {β : Type u_2} (f : αOption β) (L : List (List α)) :
                                                                          List.filterMap f L.join = (List.map (List.filterMap f) L).join
                                                                          @[simp]
                                                                          theorem List.filter_join {α : Type u_1} (p : αBool) (L : List (List α)) :
                                                                          List.filter p L.join = (List.map (List.filter p) L).join
                                                                          theorem List.join_filter_not_isEmpty {α : Type u_1} {L : List (List α)} :
                                                                          (List.filter (fun (l : List α) => !l.isEmpty) L).join = L.join
                                                                          theorem List.join_filter_ne_nil {α : Type u_1} [DecidablePred fun (l : List α) => l []] {L : List (List α)} :
                                                                          (List.filter (fun (l : List α) => decide (l [])) L).join = L.join
                                                                          @[deprecated List.filter_join]
                                                                          theorem List.join_map_filter {α : Type u_1} (p : αBool) (l : List (List α)) :
                                                                          (List.map (List.filter p) l).join = List.filter p l.join
                                                                          @[simp]
                                                                          theorem List.join_append {α : Type u_1} (L₁ : List (List α)) (L₂ : List (List α)) :
                                                                          (L₁ ++ L₂).join = L₁.join ++ L₂.join
                                                                          theorem List.join_concat {α : Type u_1} (L : List (List α)) (l : List α) :
                                                                          (L ++ [l]).join = L.join ++ l
                                                                          theorem List.join_join {α : Type u_1} {L : List (List (List α))} :
                                                                          L.join.join = (List.map List.join L).join
                                                                          theorem List.join_eq_cons_iff {α : Type u_1} {xs : List (List α)} {y : α} {ys : List α} :
                                                                          xs.join = y :: ys ∃ (as : List (List α)), ∃ (bs : List α), ∃ (cs : List (List α)), xs = as ++ (y :: bs) :: cs (∀ (l : List α), l asl = []) ys = bs ++ cs.join
                                                                          theorem List.join_eq_append_iff {α : Type u_1} {xs : List (List α)} {ys : List α} {zs : List α} :
                                                                          xs.join = ys ++ zs (∃ (as : List (List α)), ∃ (bs : List (List α)), xs = as ++ bs ys = as.join zs = bs.join) ∃ (as : List (List α)), ∃ (bs : List α), ∃ (c : α), ∃ (cs : List α), ∃ (ds : List (List α)), xs = as ++ (bs ++ c :: cs) :: ds ys = as.join ++ bs zs = c :: cs ++ ds.join
                                                                          @[reducible, inline, deprecated List.join_eq_cons_iff]
                                                                          abbrev List.join_eq_cons {α : Type u_1} {xs : List (List α)} {y : α} {ys : List α} :
                                                                          xs.join = y :: ys ∃ (as : List (List α)), ∃ (bs : List α), ∃ (cs : List (List α)), xs = as ++ (y :: bs) :: cs (∀ (l : List α), l asl = []) ys = bs ++ cs.join
                                                                          Equations
                                                                          Instances For
                                                                            @[reducible, inline, deprecated List.join_eq_append_iff]
                                                                            abbrev List.join_eq_append {α : Type u_1} {xs : List (List α)} {ys : List α} {zs : List α} :
                                                                            xs.join = ys ++ zs (∃ (as : List (List α)), ∃ (bs : List (List α)), xs = as ++ bs ys = as.join zs = bs.join) ∃ (as : List (List α)), ∃ (bs : List α), ∃ (c : α), ∃ (cs : List α), ∃ (ds : List (List α)), xs = as ++ (bs ++ c :: cs) :: ds ys = as.join ++ bs zs = c :: cs ++ ds.join
                                                                            Equations
                                                                            Instances For
                                                                              theorem List.eq_iff_join_eq {α : Type u_1} {L : List (List α)} {L' : List (List α)} :
                                                                              L = L' L.join = L'.join List.map List.length L = List.map List.length L'

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

                                                                              bind #

                                                                              theorem List.bind_def {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
                                                                              l.bind f = (List.map f l).join
                                                                              @[simp]
                                                                              theorem List.bind_id {α : Type u_1} (l : List (List α)) :
                                                                              l.bind id = l.join
                                                                              @[simp]
                                                                              theorem List.mem_bind {α : Type u_1} {β : Type u_2} {f : αList β} {b : β} {l : List α} :
                                                                              b l.bind f ∃ (a : α), a l b f a
                                                                              theorem List.exists_of_mem_bind {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : αList β} :
                                                                              b l.bind f∃ (a : α), a l b f a
                                                                              theorem 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.bind f
                                                                              @[simp]
                                                                              theorem List.bind_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                                              l.bind f = [] ∀ (x : α), x lf x = []
                                                                              @[reducible, inline, deprecated List.bind_eq_nil_iff]
                                                                              abbrev List.bind_eq_nil {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                                              l.bind f = [] ∀ (x : α), x lf x = []
                                                                              Equations
                                                                              Instances For
                                                                                theorem List.forall_mem_bind {β : Type u_1} {α : Type u_2} {p : βProp} {l : List α} {f : αList β} :
                                                                                (∀ (x : β), x l.bind fp x) ∀ (a : α), a l∀ (b : β), b f ap b
                                                                                theorem List.bind_singleton {α : Type u_1} {β : Type u_2} (f : αList β) (x : α) :
                                                                                [x].bind f = f x
                                                                                @[simp]
                                                                                theorem List.bind_singleton' {α : Type u_1} (l : List α) :
                                                                                (l.bind fun (x : α) => [x]) = l
                                                                                theorem List.head?_bind {α : Type u_1} {β : Type u_2} {l : List α} {f : αList β} :
                                                                                (l.bind f).head? = List.findSome? (fun (a : α) => (f a).head?) l
                                                                                @[simp]
                                                                                theorem List.bind_append {α : Type u_1} {β : Type u_2} (xs : List α) (ys : List α) (f : αList β) :
                                                                                (xs ++ ys).bind f = xs.bind f ++ ys.bind f
                                                                                @[reducible, inline, deprecated List.bind_append]
                                                                                abbrev List.append_bind {α : Type u_1} {β : Type u_2} (xs : List α) (ys : List α) (f : αList β) :
                                                                                (xs ++ ys).bind f = xs.bind f ++ ys.bind f
                                                                                Equations
                                                                                Instances For
                                                                                  theorem List.bind_assoc {γ : Type u_1} {α : Type u_2} {β : Type u_3} (l : List α) (f : αList β) (g : βList γ) :
                                                                                  (l.bind f).bind g = l.bind fun (x : α) => (f x).bind g
                                                                                  theorem List.map_bind {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : βγ) (g : αList β) (l : List α) :
                                                                                  List.map f (l.bind g) = l.bind fun (a : α) => List.map f (g a)
                                                                                  theorem List.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : βList γ) (l : List α) :
                                                                                  (List.map f l).bind g = l.bind fun (a : α) => g (f a)
                                                                                  theorem List.map_eq_bind {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                                                                                  List.map f l = l.bind fun (x : α) => [f x]
                                                                                  theorem List.filterMap_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : List α) (g : αList β) (f : βOption γ) :
                                                                                  List.filterMap f (l.bind g) = l.bind fun (a : α) => List.filterMap f (g a)
                                                                                  theorem List.filter_bind {α : Type u_1} {β : Type u_2} (l : List α) (g : αList β) (f : βBool) :
                                                                                  List.filter f (l.bind g) = l.bind fun (a : α) => List.filter f (g a)
                                                                                  theorem List.bind_eq_foldl {α : Type u_1} {β : Type u_2} (f : αList β) (l : List α) :
                                                                                  l.bind f = List.foldl (fun (acc : List β) (a : α) => acc ++ f a) [] l

                                                                                  replicate #

                                                                                  @[simp]
                                                                                  theorem List.replicate_one :
                                                                                  ∀ {α : Type u_1} {a : α}, List.replicate 1 a = [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 : Nat} {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}, 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}, List.replicate n a ++ List.replicate m a = List.replicate (n + m) a
                                                                                      theorem List.append_eq_replicate_iff {α : Type u_1} {n : Nat} {l₁ : List α} {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₁ : List α} {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 : α} {α_1 : Type u_2} {f : αα_1}, List.map f (List.replicate n a) = List.replicate n (f a)
                                                                                        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 : α}, p a = trueList.filter p (List.replicate n a) = List.replicate n a
                                                                                        @[simp]
                                                                                        theorem List.filter_replicate_of_neg :
                                                                                        ∀ {α : Type u_1} {p : αBool} {n : Nat} {a : α}, ¬p a = trueList.filter p (List.replicate n a) = []
                                                                                        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.join_replicate_nil {n : Nat} {α : Type u_1} :
                                                                                        (List.replicate n []).join = []
                                                                                        @[simp]
                                                                                        theorem List.join_replicate_singleton {n : Nat} :
                                                                                        ∀ {α : Type u_1} {a : α}, (List.replicate n [a]).join = List.replicate n a
                                                                                        @[simp]
                                                                                        theorem List.join_replicate_replicate {n : Nat} {m : Nat} :
                                                                                        ∀ {α : Type u_1} {a : α}, (List.replicate n (List.replicate m a)).join = List.replicate (n * m) a
                                                                                        theorem List.bind_replicate {α : Type u_1} {n : Nat} {a : α} {β : Type u_2} (f : αList β) :
                                                                                        (List.replicate n a).bind f = (List.replicate n (f a)).join
                                                                                        @[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 : List α} {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 : Nat) (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 : Nat) (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 : List α) (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 : List α} {bs : List α} :
                                                                                        as.reverse = bs as = bs.reverse
                                                                                        @[simp]
                                                                                        theorem List.reverse_inj {α : Type u_1} {xs : List α} {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 : List α) (bs : List α) :
                                                                                          (as ++ bs).reverse = bs.reverse ++ as.reverse
                                                                                          @[simp]
                                                                                          theorem List.reverse_eq_append_iff {α : Type u_1} {xs : List α} {ys : List α} {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 : List α} {ys : List α} {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 : List α} {ys : List α} {a : α} :
                                                                                            xs.reverse = ys ++ [a] xs = a :: ys.reverse
                                                                                            theorem List.reverse_join {α : Type u_1} (L : List (List α)) :
                                                                                            L.join.reverse = (List.map List.reverse L).reverse.join

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

                                                                                            theorem List.join_reverse {α : Type u_1} (L : List (List α)) :
                                                                                            L.reverse.join = (List.map List.reverse L).join.reverse

                                                                                            Joining a reverse is the same as reversing all parts and reversing the joined result.

                                                                                            theorem List.reverse_bind {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
                                                                                            (l.bind f).reverse = l.reverse.bind (List.reverse f)
                                                                                            theorem List.bind_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
                                                                                            l.reverse.bind f = (l.bind (List.reverse f)).reverse
                                                                                            @[simp]
                                                                                            theorem List.reverseAux_eq {α : Type u_1} (as : List α) (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
                                                                                            @[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' : List α} {l : List α} {h₁ : l ++ l' []} (h₂ : l' []) :
                                                                                            (l ++ l').getLast h₁ = l'.getLast h₂
                                                                                            theorem List.getLast_append {α : Type u_1} {l' : List α} {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' : List α} {l : List α} (h : l' []) :
                                                                                            (l ++ l').getLast = l'.getLast h
                                                                                            theorem List.getLast_append_left {α : Type u_1} {l' : List α} {l : List α} (w : l ++ l' []) (h : l' = []) :
                                                                                            (l ++ l').getLast w = l.getLast
                                                                                            @[simp]
                                                                                            theorem List.getLast?_append {α : Type u_1} {l : List α} {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?_bind {α : Type u_1} {β : Type u_2} {L : List α} {f : αList β} :
                                                                                            (L.bind f).getLast? = List.findSome? (fun (a : α) => (f a).getLast?) L.reverse
                                                                                            theorem List.getLast?_join {α : Type u_1} {L : List (List α)} :
                                                                                            L.join.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

                                                                                            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 : List α} {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₁ : List α} {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 : List α) (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₁ : List α} {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₁ : List α} {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₁ : List α} {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₁ : List α} {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₁ : List α} {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₁ : List α} {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} {f : αα} {l : List α} {p : αBool} :
                                                                                            (List.map f l).any p = l.any (p f)
                                                                                            @[simp]
                                                                                            theorem List.all_map {α : Type u_1} {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 : αBool} {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 : αBool} {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 : List α} {y : List α} :
                                                                                            (x ++ y).any f = (x.any f || y.any f)
                                                                                            @[simp]
                                                                                            theorem List.all_append {α : Type u_1} {f : αBool} {x : List α} {y : List α} :
                                                                                            (x ++ y).all f = (x.all f && y.all f)
                                                                                            @[simp]
                                                                                            theorem List.any_join {α : Type u_1} {f : αBool} {l : List (List α)} :
                                                                                            l.join.any f = l.any fun (x : List α) => x.any f
                                                                                            @[simp]
                                                                                            theorem List.all_join {α : Type u_1} {f : αBool} {l : List (List α)} :
                                                                                            l.join.all f = l.all fun (x : List α) => x.all f
                                                                                            @[simp]
                                                                                            theorem List.any_bind {α : Type u_1} {β : Type u_2} {p : βBool} {l : List α} {f : αList β} :
                                                                                            (l.bind f).any p = l.any fun (a : α) => (f a).any p
                                                                                            @[simp]
                                                                                            theorem List.all_bind {α : Type u_1} {β : Type u_2} {p : βBool} {l : List α} {f : αList β} :
                                                                                            (l.bind 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)