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:

Preliminaries #

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

    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
      @[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_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]? #

      @[simp]
      theorem List.get_cons_zero :
      ∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).get 0 = a
      @[simp]
      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,
      @[simp]
      theorem List.get_cons_succ' {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} :
      (a :: as).get i.succ = as.get i
      theorem List.get?_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]
      @[simp]
      theorem List.getElem?_nil {α : Type u_1} {n : Nat} :
      [][n]? = none
      @[simp]
      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?_len_le {α : Type u_1} {l : List α} {n : Nat} :
      l.length nl[n]? = none
      @[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 {α : Type u_1} {n : Nat} {a : α} {l : List α} :
      l[n]? = some a ∃ (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
      theorem List.getElem?_eq_none :
      ∀ {α : Type u_1} {l : List α} {n : Nat}, l.length nl[n]? = none
      @[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]!
      @[simp]
      theorem List.get_cons_cons_one :
      ∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, (a₁ :: a₂ :: as).get 1 = a₂
      theorem List.get!_len_le {α : Type u_1} [Inhabited α] {l : List α} {n : Nat} :
      l.length nl.get! n = default
      theorem List.get?_zero {α : Type u_1} (l : List α) :
      l.get? 0 = l.head?
      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].

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

      @[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.get_mk_zero {α : Type u_1} {l : List α} (h : 0 < l.length) :
      l.get 0, h = l.head
      theorem List.getElem!_of_getElem? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} :
      l[n]? = some al[n]! = a
      theorem List.get!_of_get? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} :
      l.get? n = some al.get! n = a
      @[simp]
      theorem List.get!_eq_getD {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) :
      l.get! n = l.getD n default
      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} {a b : α} {l : List α}, a b :: l a = b a l
      theorem List.mem_cons_self {α : Type u_1} (a : α) (l : List α) :
      a a :: l
      theorem List.mem_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
      theorem List.eq_of_mem_singleton :
      ∀ {α : Type u_1} {a b : α}, 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.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.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)
      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_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.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.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
      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), l[n]? = some a
      theorem List.mem_iff_get? {α : Type u_1} {a : α} {l : List α} :
      a l ∃ (n : Nat), l.get? n = some a
      @[simp]
      theorem List.decide_mem_cons {α : Type u_1} {y : α} {a : α} [BEq α] [LawfulBEq α] {l : List α} :
      decide (y a :: l) = (y == a || decide (y l))

      any / all #

      theorem List.any_eq {α : Type u_1} {p : αBool} {l : List α} :
      l.any p = decide (∃ (x : α), x l p x = true)
      theorem List.all_eq {α : Type u_1} {p : αBool} {l : List α} :
      l.all p = decide (∀ (x : α), x lp x = true)
      @[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

      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_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
      (l.set i a)[i] = a
      @[deprecated List.getElem_set_eq]
      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_eq {α : Type u_1} {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
      (l.set i a)[i]? = some a
      @[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.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 {α : Type u_1} (l : List α) (n : Nat) (a : α) :
      l.set n a = [] l = []
      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

      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.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
      @[simp]
      theorem List.foldr_self_append {α : Type u_1} {l' : List α} (l : List α) :
      List.foldr List.cons l' l = l ++ l'
      theorem List.foldr_self {α : Type u_1} (l : List α) :
      List.foldr List.cons [] l = l
      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)

      getD #

      @[simp]
      theorem List.getD_eq_getElem? {α : Type u_1} (l : List α) (n : Nat) (a : α) :
      l.getD n a = l[n]?.getD a
      @[deprecated List.getD_eq_getElem?]
      theorem List.getD_eq_get? {α : Type u_1} (l : List α) (n : Nat) (a : α) :
      l.getD n a = (l.get? n).getD a

      getLast #

      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₁ : a :: l []) (h₂ : l []) :
      (a :: l).getLast h₁ = l.getLast h₂
      theorem List.getLast_eq_getLastD {α : Type u_1} (a : α) (l : List α) (h : a :: l []) :
      (a :: l).getLast h = l.getLastD a
      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
      theorem List.getLast_mem {α : Type u_1} {l : List α} (h : l []) :
      l.getLast h l
      theorem List.getLastD_mem_cons {α : Type u_1} (l : List α) (a : α) :
      l.getLastD a a :: l
      theorem List.getElem_cons_length {α : Type u_1} (x : α) (xs : List α) (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? #

      theorem List.getLast?_cons {α : Type u_1} {a : α} {l : List α} :
      (a :: l).getLast? = some (l.getLastD a)
      @[simp]
      theorem List.getLast?_singleton {α : Type u_1} (a : α) :
      [a].getLast? = some a
      theorem List.getLast?_eq_getLast {α : Type u_1} (l : List α) (h : l []) :
      l.getLast? = some (l.getLast h)
      theorem List.getLast?_eq_get? {α : Type u_1} (l : List α) :
      l.getLast? = l.get? (l.length - 1)
      @[simp]
      theorem List.getLast?_concat {α : Type u_1} {a : α} (l : List α) :
      (l ++ [a]).getLast? = some a
      @[simp]
      theorem List.getLastD_concat {α : Type u_1} (a : α) (b : α) (l : List α) :
      (l ++ [b]).getLastD a = b

      Head and tail #

      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)

      tail #

      @[simp]
      theorem List.tailD_eq_tail? {α : Type u_1} (l : List α) (l' : List α) :
      l.tailD l' = l.tail?.getD l'

      Basic operations #

      map #

      @[simp]
      theorem List.map_id {α : Type u_1} (l : List α) :
      List.map id l = l
      @[simp]
      theorem List.map_id' {α : Type u_1} (l : List α) :
      List.map (fun (a : α) => a) l = l
      theorem List.map_id'' {α : Type u_1} {f : αα} (h : ∀ (x : α), f x = x) (l : List α) :
      List.map f l = l
      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} {b : α} {α_1 : Type u_2} {f : α_1α} {l : List α_1}, b List.map f l∃ (a : α_1), a l f a = b
      theorem List.mem_map_of_mem {α : Type u_1} {β : Type u_2} {a : α} {l : List α} (f : αβ) (h : a l) :
      f a List.map f l
      @[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 {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} :
      List.map f l = [] l = []
      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 {α : 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₂
      theorem 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₂
      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.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.headD_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (a : α) :
      (List.map f l).headD (f a) = f (l.headD a)
      @[simp]
      theorem List.tail?_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
      (List.map f l).tail? = Option.map (List.map f) l.tail?
      @[simp]
      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?
      @[simp]
      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_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₂
      @[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
      theorem 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)

      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
      theorem List.mem_filter :
      ∀ {α : Type u_1} {x : α} {p : αBool} {as : List α}, x List.filter p as x as p x = true
      theorem List.filter_eq_nil :
      ∀ {α : Type u_1} {p : αBool} {l : List α}, List.filter p l = [] ∀ (a : α), a l¬p a = true
      @[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 : α) => decide (p a = true q a = true)) 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_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

          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 {α : Type u_1} (l : List α) :
          List.filterMap some l = l
          theorem List.map_filterMap_some_eq_filter_map_is_some {α : 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.filterMap_append {α : Type u_1} {β : Type u_2} (l : List α) (l' : List α) (f : αOption β) :
          @[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
          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 α) :

          append #

          theorem List.getElem?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} :
          l₁.length n(l₁ ++ l₂)[n]? = 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_right' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
          (l₁ ++ l₂)[n] = l₂[n - l₁.length]
          @[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
          @[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₂
          theorem List.append_inj_right' :
          ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengtht₁ = t₂
          theorem List.append_inj_left' :
          ∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = s₂
          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_eq_nil :
          ∀ {α : Type u_1} {p q : List α}, p ++ q = [] p = [] q = []
          @[simp]
          theorem List.getLast_append {α : Type u_1} {a : α} (l : List α) (h : l ++ [a] []) :
          (l ++ [a]).getLast h = a
          theorem List.getLast_concat :
          ∀ {α : Type u_1} {l : List α} {a : α} {h : l.concat a []}, (l.concat a).getLast h = a
          theorem List.getElem_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (n : Nat) (h : n < l₁.length) :
          (l₁ ++ l₂)[n] = l₁[n]
          @[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 : ¬i < as.length) {h' : i < (as ++ bs).length} {h'' : i - as.length < bs.length} :
          (as ++ bs).get i, h' = bs.get i - as.length, h''
          theorem List.getElem?_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) :
          (l₁ ++ l₂)[n]? = l₁[n]?
          @[deprecated]
          theorem List.get?_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) :
          (l₁ ++ l₂).get? n = l₁.get? n
          theorem List.append_eq_append :
          ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.append l₂ = l₁ ++ l₂
          theorem List.append_ne_nil_of_ne_nil_left {α : Type u_1} (s : List α) (t : List α) :
          s []s ++ t []
          theorem List.append_ne_nil_of_ne_nil_right {α : Type u_1} (s : List α) (t : List α) :
          t []s ++ t []
          @[simp]
          theorem List.nil_eq_append :
          ∀ {α : Type u_1} {a b : List α}, [] = a ++ b a = [] b = []
          theorem List.append_ne_nil_of_left_ne_nil {α : Type u_1} (a : List α) (b : List α) (h0 : a []) :
          a ++ b []
          theorem 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
          theorem 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
          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
          @[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

          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_left {α : Type u_1} {l : List α} {l' : List α} (a : α) :
          l.concat a = l'.concat a l = l'
          theorem List.concat_eq_concat {α : Type u_1} {l : List α} {l' : List α} {a : α} {b : α} :
          l.concat a = l'.concat b l = l' a = b
          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.mem_join {α : Type u_1} {a : α} {L : List (List α)} :
          a L.join ∃ (l : List α), l L a l
          theorem List.exists_of_mem_join :
          ∀ {α : Type u_1} {a : α} {L : List (List α)}, a L.join∃ (l : List α), l L a l
          theorem List.mem_join_of_mem :
          ∀ {α : Type u_1} {l : List α} {L : List (List α)} {a : α}, l La la L.join
          @[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

          bind #

          @[simp]
          theorem 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
          @[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
          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.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]

          replicate #

          @[simp]
          theorem List.replicate_one :
          ∀ {α : Type u_1} {a : α}, List.replicate 1 a = [a]
          @[simp]
          theorem List.contains_replicate {α : Type u_1} [BEq α] {n : Nat} {a : α} {b : α} :
          (List.replicate n b).contains a = (a == b && !n == 0)
          @[simp]
          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)
          @[simp]
          theorem List.mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} :
          b List.replicate n a n 0 b = a
          theorem List.eq_of_mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} (h : b List.replicate n a) :
          b = a
          @[simp]
          theorem List.replicate_succ_ne_nil {α : Type u_1} (n : Nat) (a : α) :
          List.replicate (n + 1) a []
          @[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
          @[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 {α : Type u_1} {a : α} {n : Nat} {l : List α} :
          l = List.replicate n a l.length = n ∀ (b : α), b lb = a
          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 : β) :
          theorem List.map_const' {α : Type u_1} {β : Type u_2} (l : List α) (b : β) :
          List.map (fun (x : α) => b) l = List.replicate l.length b
          @[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
          @[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)

          reverse #

          @[simp]
          theorem List.length_reverse {α : Type u_1} (as : List α) :
          as.reverse.length = as.length
          theorem List.getElem?_reverse' {α : Type u_1} {l : List α} (i : Nat) (j : Nat) :
          i + j + 1 = l.lengthl.reverse[i]? = l[j]?
          @[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
          theorem List.getElem?_reverse {α : Type u_1} {l : List α} {i : Nat} (h : i < l.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
          @[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?
          @[simp]
          theorem List.reverse_append {α : Type u_1} (as : List α) (bs : List α) :
          (as ++ bs).reverse = bs.reverse ++ as.reverse
          @[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.reverse_eq_nil_iff {α : Type u_1} {xs : List α} :
          xs.reverse = [] xs = []
          @[simp]
          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
          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

          List membership #

          elem / contains #

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

          Sublists #

          take and drop #

          Further results on List.take and List.drop, which rely on stronger automation in Nat, are given in Init.Data.List.TakeDrop.

          @[simp]
          theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) :
          @[simp]
          theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) :
          (List.drop i l).length = l.length - i
          theorem List.drop_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length i) :
          List.drop i l = []
          theorem List.take_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length i) :
          List.take i l = l
          @[simp]
          theorem List.drop_length {α : Type u_1} (l : List α) :
          List.drop l.length l = []
          @[simp]
          theorem List.take_length {α : Type u_1} (l : List α) :
          List.take l.length l = l
          theorem List.take_concat_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) :
          (List.take i l).concat l[i] = List.take (i + 1) l
          theorem List.reverse_concat {α : Type u_1} (l : List α) (a : α) :
          (l.concat a).reverse = a :: l.reverse
          @[reducible, inline]
          abbrev List.take_succ_cons :
          ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as
          Equations
          Instances For
            theorem List.take_all_of_le {α : Type u_1} {n : Nat} {l : List α} (h : l.length n) :
            List.take n l = l
            @[simp]
            theorem List.take_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
            List.take l₁.length (l₁ ++ l₂) = l₁
            theorem List.take_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) :
            List.take n (l₁ ++ l₂) = l₁
            @[simp]
            theorem List.map_take {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : Nat) :
            theorem List.getElem?_take {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) :
            (List.take n l)[m]? = l[m]?
            @[deprecated List.getElem?_take]
            theorem List.get?_take {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) :
            (List.take n l).get? m = l.get? m
            @[simp]
            theorem List.get?_take_of_succ {α : Type u_1} {l : List α} {n : Nat} :
            (List.take (n + 1) l)[n]? = l[n]?
            theorem List.take_succ {α : Type u_1} {l : List α} {n : Nat} :
            List.take (n + 1) l = List.take n l ++ l[n]?.toList
            @[simp]
            theorem List.take_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} :
            List.take k l = [] l = [] k = 0
            theorem List.take_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} :
            as = []List.take i as = []
            theorem List.ne_nil_of_take_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.take i as []) :
            as []
            theorem List.dropLast_eq_take {α : Type u_1} (l : List α) :
            l.dropLast = List.take l.length.pred l
            @[simp]
            theorem List.drop_eq_nil_iff_le {α : Type u_1} {l : List α} {k : Nat} :
            List.drop k l = [] l.length k
            theorem List.drop_sizeOf_le {α : Type u_1} [SizeOf α] (l : List α) (n : Nat) :
            @[simp]
            theorem List.drop_drop {α : Type u_1} (n : Nat) (m : Nat) (l : List α) :
            List.drop n (List.drop m l) = List.drop (n + m) l
            theorem List.take_drop {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :
            @[simp]
            theorem List.map_drop {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : Nat) :
            @[simp]
            theorem List.getElem_cons_drop {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) :
            l[i] :: List.drop (i + 1) l = List.drop i l
            @[deprecated List.getElem_cons_drop]
            theorem List.get_cons_drop {α : Type u_1} (l : List α) (i : Fin l.length) :
            l.get i :: List.drop (i + 1) l = List.drop (i) l
            theorem List.drop_eq_getElem_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) :
            List.drop n l = l[n] :: List.drop (n + 1) l
            @[deprecated List.drop_eq_getElem_cons]
            theorem List.drop_eq_get_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) :
            List.drop n l = l.get n, h :: List.drop (n + 1) l
            theorem List.drop_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} :
            as = []List.drop i as = []
            theorem List.ne_nil_of_drop_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.drop i as []) :
            as []
            @[deprecated List.drop_drop]
            theorem List.drop_add {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :
            List.drop (m + n) l = List.drop m (List.drop n l)
            @[simp]
            theorem List.drop_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
            List.drop l₁.length (l₁ ++ l₂) = l₂
            theorem List.drop_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) :
            List.drop n (l₁ ++ l₂) = l₂

            takeWhile and dropWhile #

            theorem List.takeWhile_cons {α : Type u_1} (p : αBool) (a : α) (l : List α) :
            List.takeWhile p (a :: l) = if p a = true then a :: List.takeWhile p l else []
            theorem List.dropWhile_cons {α : Type u_1} {x : α} {xs : List α} {p : αBool} :
            List.dropWhile p (x :: xs) = if p x = true then List.dropWhile p xs else x :: xs
            theorem List.takeWhile_map {α : Type u_1} {β : Type u_2} (f : αβ) (p : βBool) (l : List α) :
            theorem List.dropWhile_map {α : Type u_1} {β : Type u_2} (f : αβ) (p : βBool) (l : List α) :
            @[simp]
            theorem List.takeWhile_append_dropWhile {α : Type u_1} (p : αBool) (l : List α) :
            theorem List.dropWhile_append {α : Type u_1} {p : αBool} {xs : List α} {ys : List α} :
            List.dropWhile p (xs ++ ys) = if (List.dropWhile p xs).isEmpty = true then List.dropWhile p ys else List.dropWhile p xs ++ ys
            @[simp]
            theorem List.takeWhile_replicate_eq_filter {α : Type u_1} {n : Nat} {a : α} (p : αBool) :
            theorem List.takeWhile_replicate {α : Type u_1} {n : Nat} {a : α} (p : αBool) :
            List.takeWhile p (List.replicate n a) = if p a = true then List.replicate n a else []
            @[simp]
            theorem List.dropWhile_replicate_eq_filter_not {α : Type u_1} {n : Nat} {a : α} (p : αBool) :
            List.dropWhile p (List.replicate n a) = List.filter (fun (a : α) => !p a) (List.replicate n a)
            theorem List.dropWhile_replicate {α : Type u_1} {n : Nat} {a : α} (p : αBool) :
            List.dropWhile p (List.replicate n a) = if p a = true then [] else List.replicate n a

            partition #

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

            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.dropLast_cons_of_ne_nil {α : Type u} {x : α} {l : List α} (h : l []) :
            (x :: l).dropLast = x :: 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_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.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_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

            isPrefixOf #

            @[simp]
            theorem List.isPrefixOf_cons₂_self {α : Type u_1} [BEq α] {as : List α} {bs : List α} [LawfulBEq α] {a : α} :
            (a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs
            @[simp]
            theorem List.isPrefixOf_length_pos_nil {α : Type u_1} [BEq α] {L : List α} (h : 0 < L.length) :
            L.isPrefixOf [] = false
            @[simp]
            theorem List.isPrefixOf_replicate {α : Type u_1} [BEq α] {l : List α} {n : Nat} {a : α} :
            l.isPrefixOf (List.replicate n a) = (decide (l.length n) && l.all fun (x : α) => x == a)

            isSuffixOf #

            @[simp]
            theorem List.isSuffixOf_cons_nil {α : Type u_1} [BEq α] {a : α} {as : List α} :
            (a :: as).isSuffixOf [] = false
            @[simp]
            theorem List.isSuffixOf_replicate {α : Type u_1} [BEq α] {l : List α} {n : Nat} {a : α} :
            l.isSuffixOf (List.replicate n a) = (decide (l.length n) && l.all fun (x : α) => x == a)

            rotateLeft #

            @[simp]
            theorem List.rotateLeft_zero {α : Type u_1} (l : List α) :
            l.rotateLeft 0 = l

            rotateRight #

            @[simp]
            theorem List.rotateRight_zero {α : Type u_1} (l : List α) :
            l.rotateRight 0 = 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.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 α] [LawfulBEq α] (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 α] {a : α} {b : α} {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 α] {a : α} {b : α} {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
            @[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) :

            erase #

            @[simp]
            theorem List.erase_cons_head {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
            (a :: l).erase a = l
            @[simp]
            theorem List.erase_cons_tail {α : Type u_1} [BEq α] {a : α} {b : α} (l : List α) (h : ¬(b == a) = true) :
            (b :: l).erase a = b :: l.erase a
            theorem List.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
            ¬a ll.erase a = l
            @[simp]
            theorem List.erase_replicate_self {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a : α} :
            (List.replicate n a).erase a = List.replicate (n - 1) a
            @[simp]
            theorem List.erase_replicate_ne {α : Type u_1} [BEq α] {n : Nat} [LawfulBEq α] {a : α} {b : α} (h : (!b == a) = true) :
            (List.replicate n a).erase b = List.replicate n a

            find? #

            @[simp]
            theorem List.find?_cons_of_pos :
            ∀ {α : Type u_1} {p : αBool} {a : α} (l : List α), p a = trueList.find? p (a :: l) = some a
            @[simp]
            theorem List.find?_cons_of_neg :
            ∀ {α : Type u_1} {p : αBool} {a : α} (l : List α), ¬p a = trueList.find? p (a :: l) = List.find? p l
            @[simp]
            theorem List.find?_eq_none :
            ∀ {α : Type u_1} {p : αBool} {l : List α}, List.find? p l = none ∀ (x : α), x l¬p x = true
            theorem List.find?_some :
            ∀ {α : Type u_1} {p : αBool} {a : α} {l : List α}, List.find? p l = some ap a = true
            @[simp]
            theorem List.mem_of_find?_eq_some :
            ∀ {α : Type u_1} {p : αBool} {a : α} {l : List α}, List.find? p l = some aa l
            @[simp]
            theorem List.find?_map {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) :
            theorem List.find?_replicate :
            ∀ {α : Type u_1} {p : αBool} {n : Nat} {a : α}, List.find? p (List.replicate n a) = if n = 0 then none else if p a = true then some a else none
            @[simp]
            theorem List.find?_replicate_of_length_pos {n : Nat} :
            ∀ {α : Type u_1} {p : αBool} {a : α}, 0 < nList.find? p (List.replicate n a) = if p a = true then some a else none
            @[simp]
            theorem List.find?_replicate_of_pos :
            ∀ {α : Type u_1} {p : αBool} {n : Nat} {a : α}, p a = trueList.find? p (List.replicate n a) = if n = 0 then none else some a
            @[simp]
            theorem List.find?_replicate_of_neg :
            ∀ {α : Type u_1} {p : αBool} {n : Nat} {a : α}, ¬p a = trueList.find? p (List.replicate n a) = none

            findSome? #

            @[simp]
            theorem List.findSome?_cons_of_isSome :
            ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {a : α} (l : List α), (f a).isSome = trueList.findSome? f (a :: l) = f a
            @[simp]
            theorem List.findSome?_cons_of_isNone :
            ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {a : α} (l : List α), (f a).isNone = trueList.findSome? f (a :: l) = List.findSome? f l
            theorem List.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αOption β} (w : List.findSome? f l = some b) :
            ∃ (a : α), a l f a = some b
            @[simp]
            theorem List.findSome?_map {β : Type u_1} {γ : Type u_2} :
            ∀ {α : Type u_3} {p : γOption α} (f : βγ) (l : List β), List.findSome? p (List.map f l) = List.findSome? (p f) l
            theorem List.findSome?_replicate :
            ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {n : Nat} {a : α}, List.findSome? f (List.replicate n a) = if n = 0 then none else f a
            @[simp]
            theorem List.findSome?_replicate_of_pos {n : Nat} :
            ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {a : α}, 0 < nList.findSome? f (List.replicate n a) = f a
            @[simp]
            theorem List.find?_replicate_of_isSome :
            ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {n : Nat} {a : α}, (f a).isSome = trueList.findSome? f (List.replicate n a) = if n = 0 then none else f a
            @[simp]
            theorem List.find?_replicate_of_isNone :
            ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {n : Nat} {a : α}, (f a).isNone = trueList.findSome? f (List.replicate n a) = none

            lookup #

            @[simp]
            theorem List.lookup_cons_self {α : Type u_2} [BEq α] [LawfulBEq α] :
            ∀ {β : Type u_1} {b : β} {es : List (α × β)} {k : α}, List.lookup k ((k, b) :: es) = some b
            theorem List.lookup_replicate {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} {a : α} :
            ∀ {α_1 : Type u_1} {b : α_1} {k : α}, List.lookup k (List.replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
            theorem List.lookup_replicate_of_pos {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} {a : α} :
            ∀ {α_1 : Type u_1} {b : α_1} {k : α}, 0 < nList.lookup k (List.replicate n (a, b)) = if (k == a) = true then some b else none
            theorem List.lookup_replicate_self {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} :
            ∀ {α_1 : Type u_1} {b : α_1} {a : α}, List.lookup a (List.replicate n (a, b)) = if n = 0 then none else some b
            @[simp]
            theorem List.lookup_replicate_self_of_pos {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} :
            ∀ {α_1 : Type u_1} {b : α_1} {a : α}, 0 < nList.lookup a (List.replicate n (a, b)) = some b
            @[simp]
            theorem List.lookup_replicate_ne {α : Type u_2} [BEq α] [LawfulBEq α] {a : α} {n : Nat} :
            ∀ {α_1 : Type u_1} {b : α_1} {k : α}, (!k == a) = trueList.lookup k (List.replicate n (a, b)) = none

            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
            theorem List.any_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (p : βBool) :
            (List.map f l).any p = l.any (p f)
            theorem List.all_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (p : βBool) :
            (List.map f l).all p = l.all (p f)

            Zippers #

            zip #

            theorem List.zip_map {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (f : αγ) (g : βδ) (l₁ : List α) (l₂ : List β) :
            (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)
            theorem List.zip_map_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : αγ) (l₁ : List α) (l₂ : List β) :
            (List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)
            theorem List.zip_map_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : βγ) (l₁ : List α) (l₂ : List β) :
            l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)
            theorem List.zip_append {α : Type u_1} {β : Type u_2} {l₁ : List α} {r₁ : List α} {l₂ : List β} {r₂ : List β} (_h : l₁.length = l₂.length) :
            (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂
            theorem List.zip_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) (l : List α) :
            (List.map f l).zip (List.map g l) = List.map (fun (a : α) => (f a, g a)) l
            theorem List.of_mem_zip {α : Type u_1} {β : Type u_2} {a : α} {b : β} {l₁ : List α} {l₂ : List β} :
            (a, b) l₁.zip l₂a l₁ b l₂
            theorem List.map_fst_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
            l₁.length l₂.lengthList.map Prod.fst (l₁.zip l₂) = l₁
            theorem List.map_snd_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
            l₂.length l₁.lengthList.map Prod.snd (l₁.zip l₂) = l₂
            @[simp]
            theorem List.zip_replicate' {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : Nat} :

            See also List.zip_replicate in Init.Data.List.TakeDrop for a generalization with different lengths.

            zipWith #

            theorem List.getElem?_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : αβγ} {i : Nat} :
            (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with | some a, some b => some (f a b) | x, x_1 => none
            @[deprecated List.getElem?_zipWith]
            theorem List.get?_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : αβγ} :
            (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | x, x_1 => none
            @[reducible, inline, deprecated List.getElem?_zipWith]
            abbrev List.zipWith_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : αβγ} :
            (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | x, x_1 => none
            Equations
            Instances For
              @[simp]
              theorem List.zipWith_map {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} (f : γδμ) (g : αγ) (h : βδ) (l₁ : List α) (l₂ : List β) :
              List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun (a : α) (b : β) => f (g a) (h b)) l₁ l₂
              theorem List.zipWith_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : αα') (g : α'βγ) :
              List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun (a : α) (b : β) => g (f a) b) l₁ l₂
              theorem List.zipWith_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : ββ') (g : αβ'γ) :
              List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun (a : α) (b : β) => g a (f b)) l₁ l₂
              theorem List.zipWith_foldr_eq_zip_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : γδδ} {f : αβγ} (i : δ) :
              List.foldr g i (List.zipWith f l₁ l₂) = List.foldr (fun (p : α × β) (r : δ) => g (f p.fst p.snd) r) i (l₁.zip l₂)
              theorem List.zipWith_foldl_eq_zip_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : δγδ} {f : αβγ} (i : δ) :
              List.foldl g i (List.zipWith f l₁ l₂) = List.foldl (fun (r : δ) (p : α × β) => g r (f p.fst p.snd)) i (l₁.zip l₂)
              @[simp]
              theorem List.zipWith_eq_nil_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {l : List α} {l' : List β} :
              List.zipWith f l l' = [] l = [] l' = []
              theorem List.map_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδα) (l : List γ) (l' : List δ) :
              List.map f (List.zipWith g l l') = List.zipWith (fun (x : γ) (y : δ) => f (g x y)) l l'
              theorem List.zipWith_distrib_take :
              ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.take n (List.zipWith f l l') = List.zipWith f (List.take n l) (List.take n l')
              theorem List.zipWith_distrib_drop :
              ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.drop n (List.zipWith f l l') = List.zipWith f (List.drop n l) (List.drop n l')
              theorem List.zipWith_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (l : List α) (la : List α) (l' : List β) (lb : List β) (h : l.length = l'.length) :
              List.zipWith f (l ++ la) (l' ++ lb) = List.zipWith f l l' ++ List.zipWith f la lb
              @[simp]
              theorem List.zipWith_replicate' {α : Type u_1} {β : Type u_2} :
              ∀ {α_1 : Type u_3} {f : αβα_1} {a : α} {b : β} {n : Nat}, List.zipWith f (List.replicate n a) (List.replicate n b) = List.replicate n (f a b)

              See also List.zipWith_replicate in Init.Data.List.TakeDrop for a generalization with different lengths.

              zipWithAll #

              theorem List.getElem?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option αOption βγ} {i : Nat} :
              (List.zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with | none, none => none | a?, b? => some (f a? b?)
              @[deprecated List.getElem?_zipWithAll]
              theorem List.get?_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : Option αOption βγ} :
              (List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => none | a?, b? => some (f a? b?)
              @[reducible, inline, deprecated List.getElem?_zipWithAll]
              abbrev List.zipWithAll_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : Option αOption βγ} :
              (List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => none | a?, b? => some (f a? b?)
              Equations
              Instances For
                theorem List.zipWithAll_map {γ : Type u_1} {δ : Type u_2} {α : Type u_1} {β : Type u_2} {μ : Type u_3} (f : Option γOption δμ) (g : αγ) (h : βδ) (l₁ : List α) (l₂ : List β) :
                List.zipWithAll f (List.map g l₁) (List.map h l₂) = List.zipWithAll (fun (a : Option α) (b : Option β) => f (g <$> a) (h <$> b)) l₁ l₂
                theorem List.zipWithAll_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} (l₁ : List α) (l₂ : List β) (f : αα') (g : Option α'Option βγ) :
                List.zipWithAll g (List.map f l₁) l₂ = List.zipWithAll (fun (a : Option α) (b : Option β) => g (f <$> a) b) l₁ l₂
                theorem List.zipWithAll_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_2} {γ : Type u_3} (l₁ : List α) (l₂ : List β) (f : ββ') (g : Option αOption β'γ) :
                List.zipWithAll g l₁ (List.map f l₂) = List.zipWithAll (fun (a : Option α) (b : Option β) => g a (f <$> b)) l₁ l₂
                theorem List.map_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : Option γOption δα) (l : List γ) (l' : List δ) :
                List.map f (List.zipWithAll g l l') = List.zipWithAll (fun (x : Option γ) (y : Option δ) => f (g x y)) l l'
                @[simp]
                theorem List.zipWithAll_replicate {α : Type u_1} {β : Type u_2} :
                ∀ {α_1 : Type u_3} {f : Option αOption βα_1} {a : α} {b : β} {n : Nat}, List.zipWithAll f (List.replicate n a) (List.replicate n b) = List.replicate n (f (some a) (some b))

                unzip #

                @[simp]
                theorem List.unzip_replicate {α : Type u_1} {β : Type u_2} {n : Nat} {a : α} {b : β} :
                (List.replicate n (a, b)).unzip = (List.replicate n a, List.replicate n b)

                Ranges and enumeration #

                enumFrom #

                @[simp]
                theorem List.enumFrom_length {α : Type u_1} {n : Nat} {l : List α} :
                (List.enumFrom n l).length = l.length
                theorem List.map_enumFrom {α : Type u_1} {β : Type u_2} (f : αβ) (n : Nat) (l : List α) :

                enum #

                @[simp]
                theorem List.enum_length :
                ∀ {α : Type u_1} {l : List α}, l.enum.length = l.length
                theorem List.enum_cons :
                ∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).enum = (0, a) :: List.enumFrom 1 as
                theorem List.map_enum {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
                List.map (Prod.map id f) l.enum = (List.map f l).enum

                Minima and maxima #

                minimum? #

                @[simp]
                theorem List.minimum?_nil {α : Type u_1} [Min α] :
                [].minimum? = none
                theorem List.minimum?_cons {α : Type u_1} {x : α} [Min α] {xs : List α} :
                (x :: xs).minimum? = some (List.foldl min x xs)
                @[simp]
                theorem List.minimum?_eq_none_iff {α : Type u_1} {xs : List α} [Min α] :
                xs.minimum? = none xs = []
                theorem List.minimum?_mem {α : Type u_1} {a : α} [Min α] (min_eq_or : ∀ (a b : α), min a b = a min a b = b) {xs : List α} :
                xs.minimum? = some aa xs
                theorem List.le_minimum?_iff {α : Type u_1} {a : α} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a min b c a b a c) {xs : List α} :
                xs.minimum? = some a∀ (x : α), x a ∀ (b : α), b xsx b
                theorem List.minimum?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] [anti : Antisymm fun (x x_1 : α) => x x_1] (le_refl : ∀ (a : α), a a) (min_eq_or : ∀ (a b : α), min a b = a min a b = b) (le_min_iff : ∀ (a b c : α), a min b c a b a c) {xs : List α} :
                xs.minimum? = some a a xs ∀ (b : α), b xsa b
                theorem List.minimum?_replicate {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) :
                (List.replicate n a).minimum? = if n = 0 then none else some a
                @[simp]
                theorem List.minimum?_replicate_of_pos {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
                (List.replicate n a).minimum? = some a

                maximum? #

                @[simp]
                theorem List.maximum?_nil {α : Type u_1} [Max α] :
                [].maximum? = none
                theorem List.maximum?_cons {α : Type u_1} {x : α} [Max α] {xs : List α} :
                (x :: xs).maximum? = some (List.foldl max x xs)
                @[simp]
                theorem List.maximum?_eq_none_iff {α : Type u_1} {xs : List α} [Max α] :
                xs.maximum? = none xs = []
                theorem List.maximum?_mem {α : Type u_1} {a : α} [Max α] (min_eq_or : ∀ (a b : α), max a b = a max a b = b) {xs : List α} :
                xs.maximum? = some aa xs
                theorem List.maximum?_le_iff {α : Type u_1} {a : α} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max b c a b a c a) {xs : List α} :
                xs.maximum? = some a∀ (x : α), a x ∀ (b : α), b xsb x
                theorem List.maximum?_eq_some_iff {α : Type u_1} {a : α} [Max α] [LE α] [anti : Antisymm fun (x x_1 : α) => x x_1] (le_refl : ∀ (a : α), a a) (max_eq_or : ∀ (a b : α), max a b = a max a b = b) (max_le_iff : ∀ (a b c : α), max b c a b a c a) {xs : List α} :
                xs.maximum? = some a a xs ∀ (b : α), b xsb a
                theorem List.maximum?_replicate {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) :
                (List.replicate n a).maximum? = if n = 0 then none else some a
                @[simp]
                theorem List.maximum?_replicate_of_pos {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
                (List.replicate n a).maximum? = some a

                Monadic operations #

                mapM #

                def List.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm β) :
                List αm (List β)

                Alternate (non-tail-recursive) form of mapM for proofs.

                Equations
                Instances For
                  @[simp]
                  theorem List.mapM'_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : αm β} :
                  List.mapM' f [] = pure []
                  @[simp]
                  theorem List.mapM'_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] {f : αm β} :
                  List.mapM' f (a :: l) = do let __do_liftf a let __do_lift_1List.mapM' f l pure (__do_lift :: __do_lift_1)
                  theorem List.mapM'_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αm β) (l : List α) :
                  theorem List.mapM'_eq_mapM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αm β) (l : List α) (acc : List β) :
                  List.mapM.loop f l acc = do let __do_liftList.mapM' f l pure (acc.reverse ++ __do_lift)
                  @[simp]
                  theorem List.mapM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : αm β) :
                  List.mapM f [] = pure []
                  @[simp]
                  theorem List.mapM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [Monad m] [LawfulMonad m] (f : αm β) :
                  List.mapM f (a :: l) = do let __do_liftf a let __do_lift_1List.mapM f l pure (__do_lift :: __do_lift_1)
                  @[simp]
                  theorem List.mapM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αm β) {l₁ : List α} {l₂ : List α} :
                  List.mapM f (l₁ ++ l₂) = do let __do_liftList.mapM f l₁ let __do_lift_1List.mapM f l₂ pure (__do_lift ++ __do_lift_1)

                  forM #

                  @[simp]
                  theorem List.forM_nil' {m : Type u_1 → Type u_2} {α : Type u_3} {f : αm PUnit} [Monad m] :
                  [].forM f = pure PUnit.unit
                  @[simp]
                  theorem List.forM_cons' {m : Type u_1 → Type u_2} :
                  ∀ {α : Type u_3} {a : α} {as : List α} {f : αm PUnit} [inst : Monad m], (a :: as).forM f = do f a as.forM f