# Basic properties of lists #

instance List.uniqueOfIsEmpty {α : Type u} [] :

There is only one list of an empty type

Equations
• List.uniqueOfIsEmpty = let __src := instInhabitedList; { toInhabited := __src, uniq := }
Equations
• =
Equations
• =
@[simp]
theorem List.cons_injective {α : Type u} {a : α} :
theorem List.singleton_injective {α : Type u} :
Function.Injective fun (a : α) => [a]
theorem List.singleton_inj {α : Type u} {a : α} {b : α} :
[a] = [b] a = b
theorem List.set_of_mem_cons {α : Type u} (l : List α) (a : α) :
{x : α | x a :: l} = insert a {x : α | x l}

### mem #

theorem Decidable.List.eq_or_ne_mem_of_mem {α : Type u} [] {a : α} {b : α} {l : List α} (h : a b :: l) :
a = b a b a l
theorem List.mem_pair {α : Type u} {a : α} {b : α} {c : α} :
a [b, c] a = b a = c
@[deprecated List.append_of_mem]
theorem List.mem_split {α : Type u_1} {a : α} {l : List α} :
a l∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

Alias of List.append_of_mem.

@[simp]
theorem List.mem_map_of_injective {α : Type u} {β : Type v} {f : αβ} (H : ) {a : α} {l : List α} :
f a List.map f l a l
@[simp]
theorem Function.Involutive.exists_mem_and_apply_eq_iff {α : Type u} {f : αα} (hf : ) (x : α) (l : List α) :
(∃ (y : α), y l f y = x) f x l
theorem List.mem_map_of_involutive {α : Type u} {f : αα} (hf : ) {a : α} {l : List α} :
a List.map f l f a l
theorem List.map_bind {α : Type u} {β : Type v} {γ : Type w} (g : βList γ) (f : αβ) (l : List α) :
(List.map f l).bind g = l.bind fun (a : α) => g (f a)

### length #

theorem List.length_pos_of_ne_nil {α : Type u_1} {l : List α} :
l []0 < l.length

Alias of the reverse direction of List.length_pos.

theorem List.ne_nil_of_length_pos {α : Type u_1} {l : List α} :
0 < l.lengthl []

Alias of the forward direction of List.length_pos.

theorem List.length_pos_iff_ne_nil {α : Type u} {l : List α} :
0 < l.length l []
theorem List.exists_of_length_succ {α : Type u} {n : } (l : List α) :
l.length = n + 1∃ (h : α), ∃ (t : List α), l = h :: t
@[simp]
theorem List.length_injective_iff {α : Type u} :
Function.Injective List.length
@[simp]
theorem List.length_injective {α : Type u} [] :
Function.Injective List.length
theorem List.length_eq_two {α : Type u} {l : List α} :
l.length = 2 ∃ (a : α), ∃ (b : α), l = [a, b]
theorem List.length_eq_three {α : Type u} {l : List α} :
l.length = 3 ∃ (a : α), ∃ (b : α), ∃ (c : α), l = [a, b, c]

### set-theoretic notation of lists #

instance List.instSingletonList {α : Type u} :
Singleton α (List α)
Equations
• List.instSingletonList = { singleton := fun (x : α) => [x] }
Equations
• List.instInsertOfDecidableEq_mathlib = { insert := List.insert }
Equations
• =
theorem List.singleton_eq {α : Type u} (x : α) :
{x} = [x]
theorem List.insert_neg {α : Type u} [] {x : α} {l : List α} (h : ¬x l) :
insert x l = x :: l
theorem List.insert_pos {α : Type u} [] {x : α} {l : List α} (h : x l) :
insert x l = l
theorem List.doubleton_eq {α : Type u} [] {x : α} {y : α} (h : x y) :
{x, y} = [x, y]

### bounded quantifiers over lists #

theorem List.forall_mem_of_forall_mem_cons {α : Type u} {p : αProp} {a : α} {l : List α} (h : ∀ (x : α), x a :: lp x) (x : α) :
x lp x
theorem List.exists_mem_cons_of {α : Type u} {p : αProp} {a : α} (l : List α) (h : p a) :
∃ (x : α), x a :: l p x
theorem List.exists_mem_cons_of_exists {α : Type u} {p : αProp} {a : α} {l : List α} :
(∃ (x : α), x l p x)∃ (x : α), x a :: l p x
theorem List.or_exists_of_exists_mem_cons {α : Type u} {p : αProp} {a : α} {l : List α} :
(∃ (x : α), x a :: l p x)p a ∃ (x : α), x l p x
theorem List.exists_mem_cons_iff {α : Type u} (p : αProp) (a : α) (l : List α) :
(∃ (x : α), x a :: l p x) p a ∃ (x : α), x l p x

### list subset #

instance List.instIsTransSubset {α : Type u} :
IsTrans (List α) Subset
Equations
• =
theorem List.cons_subset_of_subset_of_mem {α : Type u} {a : α} {l : List α} {m : List α} (ainm : a m) (lsubm : l m) :
a :: l m
theorem List.append_subset_of_subset_of_subset {α : Type u} {l₁ : List α} {l₂ : List α} {l : List α} (l₁subl : l₁ l) (l₂subl : l₂ l) :
l₁ ++ l₂ l
theorem List.eq_nil_of_subset_nil {α : Type u_1} {l : List α} :
l []l = []

Alias of the forward direction of List.subset_nil.

theorem List.map_subset_iff {α : Type u} {β : Type v} {l₁ : List α} {l₂ : List α} (f : αβ) (h : ) :
List.map f l₁ List.map f l₂ l₁ l₂

### append #

theorem List.append_eq_has_append {α : Type u} {L₁ : List α} {L₂ : List α} :
L₁.append L₂ = L₁ ++ L₂
@[deprecated List.append_eq_cons]
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

Alias of List.append_eq_cons.

@[deprecated List.cons_eq_append]
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

Alias of List.cons_eq_append.

@[deprecated List.append_cancel_left]
theorem List.append_left_cancel {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = as ++ cs) :
bs = cs

Alias of List.append_cancel_left.

@[deprecated List.append_cancel_right]
theorem List.append_right_cancel {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = cs ++ bs) :
as = cs

Alias of List.append_cancel_right.

@[simp]
theorem List.append_left_eq_self {α : Type u} {x : List α} {y : List α} :
x ++ y = y x = []
@[simp]
theorem List.self_eq_append_left {α : Type u} {x : List α} {y : List α} :
y = x ++ y x = []
@[simp]
theorem List.append_right_eq_self {α : Type u} {x : List α} {y : List α} :
x ++ y = x y = []
@[simp]
theorem List.self_eq_append_right {α : Type u} {x : List α} {y : List α} :
x = x ++ y y = []
theorem List.append_right_injective {α : Type u} (s : List α) :
Function.Injective fun (t : List α) => s ++ t
theorem List.append_left_injective {α : Type u} (t : List α) :
Function.Injective fun (s : List α) => s ++ t

### replicate #

@[simp]
theorem List.replicate_zero {α : Type u} (a : α) :
= []
theorem List.replicate_one {α : Type u} (a : α) :
= [a]
theorem List.eq_replicate_length {α : Type u} {a : α} {l : List α} :
l = List.replicate l.length a ∀ (b : α), b lb = a
theorem List.replicate_add {α : Type u} (m : ) (n : ) (a : α) :
List.replicate (m + n) a = ++
theorem List.replicate_succ' {α : Type u} (n : ) (a : α) :
List.replicate (n + 1) a = ++ [a]
theorem List.replicate_subset_singleton {α : Type u} (n : ) (a : α) :
[a]
theorem List.subset_singleton_iff {α : Type u} {a : α} {L : List α} :
L [a] ∃ (n : ), L =
@[simp]
theorem List.map_replicate {α : Type u} {β : Type v} (f : αβ) (n : ) (a : α) :
@[simp]
theorem List.tail_replicate {α : Type u} (a : α) (n : ) :
().tail = List.replicate (n - 1) a
@[simp]
theorem List.join_replicate_nil {α : Type u} (n : ) :
().join = []
theorem List.replicate_right_injective {α : Type u} {n : } (hn : n 0) :
theorem List.replicate_right_inj {α : Type u} {a : α} {b : α} {n : } (hn : n 0) :
= a = b
@[simp]
theorem List.replicate_right_inj' {α : Type u} {a : α} {b : α} {n : } :
= n = 0 a = b
theorem List.replicate_left_injective {α : Type u} (a : α) :
Function.Injective fun (x : ) =>
@[simp]
theorem List.replicate_left_inj {α : Type u} {a : α} {n : } {m : } :
= n = m
@[simp]
theorem List.head_replicate {α : Type u} (n : ) (a : α) (h : []) :

### pure #

theorem List.mem_pure {α : Type u} (x : α) (y : α) :
x pure y x = y

### bind #

@[simp]
theorem List.bind_eq_bind {α : Type u_2} {β : Type u_2} (f : αList β) (l : List α) :
l >>= f = l.bind f

### reverse #

theorem List.reverse_cons' {α : Type u} (a : α) (l : List α) :
(a :: l).reverse = l.reverse.concat a
theorem List.reverse_concat' {α : Type u} (l : List α) (a : α) :
(l ++ [a]).reverse = a :: l.reverse
theorem List.reverse_singleton {α : Type u} (a : α) :
[a].reverse = [a]
@[simp]
theorem List.reverse_involutive {α : Type u} :
Function.Involutive List.reverse
@[simp]
theorem List.reverse_injective {α : Type u} :
Function.Injective List.reverse
@[simp]
theorem List.reverse_inj {α : Type u} {l₁ : List α} {l₂ : List α} :
l₁.reverse = l₂.reverse l₁ = l₂
theorem List.reverse_eq_iff {α : Type u} {l : List α} {l' : List α} :
l.reverse = l' l = l'.reverse
theorem List.concat_eq_reverse_cons {α : Type u} (a : α) (l : List α) :
l.concat a = (a :: l.reverse).reverse
theorem List.map_reverse {α : Type u} {β : Type v} (f : αβ) (l : List α) :
List.map f l.reverse = (List.map f l).reverse
theorem List.map_reverseAux {α : Type u} {β : Type v} (f : αβ) (l₁ : List α) (l₂ : List α) :
List.map f (l₁.reverseAux l₂) = (List.map f l₁).reverseAux (List.map f l₂)
@[simp]
theorem List.reverse_replicate {α : Type u} (n : ) (a : α) :
().reverse =

### empty #

theorem List.isEmpty_iff_eq_nil {α : Type u} {l : List α} :
l.isEmpty = true l = []

### getLast #

@[simp]
theorem List.getLast_cons {α : Type u} {a : α} {l : List α} (h : l []) :
(a :: l).getLast = l.getLast h
theorem List.getLast_append_singleton {α : Type u} {a : α} (l : List α) :
(l ++ [a]).getLast = a
theorem List.getLast_append' {α : Type u} (l₁ : List α) (l₂ : List α) (h : l₂ []) :
(l₁ ++ l₂).getLast = l₂.getLast h
theorem List.getLast_concat' {α : Type u} {a : α} (l : List α) :
(l.concat a).getLast = a
@[simp]
theorem List.getLast_singleton' {α : Type u} (a : α) :
[a].getLast = a
theorem List.getLast_cons_cons {α : Type u} (a₁ : α) (a₂ : α) (l : List α) :
(a₁ :: a₂ :: l).getLast = (a₂ :: l).getLast
theorem List.dropLast_append_getLast {α : Type u} {l : List α} (h : l []) :
l.dropLast ++ [l.getLast h] = l
theorem List.getLast_congr {α : Type u} {l₁ : List α} {l₂ : List α} (h₁ : l₁ []) (h₂ : l₂ []) (h₃ : l₁ = l₂) :
l₁.getLast h₁ = l₂.getLast h₂
theorem List.getLast_replicate_succ {α : Type u} (m : ) (a : α) :
(List.replicate (m + 1) a).getLast = a

### getLast? #

@[simp]
theorem List.getLast?_cons_cons {α : Type u} (a : α) (b : α) (l : List α) :
(a :: b :: l).getLast? = (b :: l).getLast?
@[simp]
theorem List.getLast?_isNone {α : Type u} {l : List α} :
l.getLast?.isNone = true l = []
@[simp]
theorem List.getLast?_isSome {α : Type u} {l : List α} :
l.getLast?.isSome = true l []
theorem List.mem_getLast?_eq_getLast {α : Type u} {l : List α} {x : α} :
x l.getLast?∃ (h : l []), x = l.getLast h
theorem List.getLast?_eq_getLast_of_ne_nil {α : Type u} {l : List α} (h : l []) :
l.getLast? = some (l.getLast h)
theorem List.mem_getLast?_cons {α : Type u} {x : α} {y : α} {l : List α} :
x l.getLast?x (y :: l).getLast?
theorem List.mem_of_mem_getLast? {α : Type u} {l : List α} {a : α} (ha : a l.getLast?) :
a l
theorem List.dropLast_append_getLast? {α : Type u} {l : List α} (a : α) :
a l.getLast?l.dropLast ++ [a] = l
theorem List.getLastI_eq_getLast? {α : Type u} [] (l : List α) :
l.getLastI = l.getLast?.iget
@[simp]
theorem List.getLast?_append_cons {α : Type u} (l₁ : List α) (a : α) (l₂ : List α) :
(l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
theorem List.getLast?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} :
l₂ [](l₁ ++ l₂).getLast? = l₂.getLast?
theorem List.getLast?_append {α : Type u} {l₁ : List α} {l₂ : List α} {x : α} (h : x l₂.getLast?) :
x (l₁ ++ l₂).getLast?

@[simp]
theorem List.head!_nil {α : Type u} [] :
@[simp]
theorem List.head_cons_tail {α : Type u} (x : List α) (h : x []) :
x.head h :: x.tail = x
theorem List.head!_eq_head? {α : Type u} [] (l : List α) :
theorem List.surjective_head! {α : Type u} [] :
theorem List.eq_cons_of_mem_head? {α : Type u} {x : α} {l : List α} :
x l.head?l = x :: l.tail
theorem List.mem_of_mem_head? {α : Type u} {x : α} {l : List α} (h : x l.head?) :
x l
@[simp]
theorem List.head!_cons {α : Type u} [] (a : α) (l : List α) :
@[simp]
theorem List.head!_append {α : Type u} [] (t : List α) {s : List α} (h : s []) :
theorem List.head?_append {α : Type u} {s : List α} {t : List α} {x : α} (h : x s.head?) :
theorem List.head?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} :
theorem List.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : List α} (h : l []) :
(l ++ [a]).tail = l.tail ++ [a]
theorem List.cons_head?_tail {α : Type u} {l : List α} {a : α} :
a l.head?a :: l.tail = l
theorem List.head!_mem_head? {α : Type u} [] {l : List α} :
theorem List.cons_head!_tail {α : Type u} [] {l : List α} (h : l []) :
theorem List.head!_mem_self {α : Type u} [] {l : List α} (h : l []) :
theorem List.head_mem {α : Type u} {l : List α} (h : l []) :
@[simp]
theorem List.head?_map {α : Type u} {β : Type v} (f : αβ) (l : List α) :
theorem List.tail_append_of_ne_nil {α : Type u} (l : List α) (l' : List α) (h : l []) :
(l ++ l').tail = l.tail ++ l'
theorem List.get_eq_get? {α : Type u} (l : List α) (i : Fin l.length) :
l.get i = (l.get? i).get
@[deprecated List.get]
def List.nthLe {α : Type u} (l : List α) (n : ) (h : n < l.length) :
α

nth element of a list l given n < l.length.

Equations
• l.nthLe n h = l.get n, h
Instances For
@[simp]
theorem List.nthLe_tail {α : Type u} (l : List α) (i : ) (h : i < l.tail.length) (h' : optParam (i + 1 < l.length) ) :
l.tail.nthLe i h = l.nthLe (i + 1) h'
theorem List.nthLe_cons_aux {α : Type u} {l : List α} {a : α} {n : } (hn : n 0) (h : n < (a :: l).length) :
n - 1 < l.length
theorem List.nthLe_cons {α : Type u} {l : List α} {a : α} {n : } (hl : n < (a :: l).length) :
(a :: l).nthLe n hl = if hn : n = 0 then a else l.nthLe (n - 1)
@[simp]
theorem List.modifyHead_modifyHead {α : Type u} (l : List α) (f : αα) (g : αα) :

### Induction from the right #

@[irreducible]
def List.reverseRecOn {α : Type u} {motive : List αSort u_2} (l : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive lmotive (l ++ [a])) :
motive l

Induction principle from the right for lists: if a property holds for the empty list, and for l ++ [a] if it holds for l, then it holds for all lists. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem List.reverseRecOn_nil {α : Type u} {motive : List αSort u_2} (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive lmotive (l ++ [a])) :
List.reverseRecOn [] nil append_singleton = nil
@[simp]
theorem List.reverseRecOn_concat {α : Type u} {motive : List αSort u_2} (x : α) (xs : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive lmotive (l ++ [a])) :
List.reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (List.reverseRecOn xs nil append_singleton)
@[irreducible]
def List.bidirectionalRec {α : Type u} {motive : List αSort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive lmotive (a :: (l ++ [b]))) (l : List α) :
motive l

Bidirectional induction principle for lists: if a property holds for the empty list, the singleton list, and a :: (l ++ [b]) from l, then it holds for all lists. This can be used to prove statements about palindromes. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
Instances For
@[simp]
theorem List.bidirectionalRec_nil {α : Type u} {motive : List αSort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive lmotive (a :: (l ++ [b]))) :
List.bidirectionalRec nil singleton cons_append [] = nil
@[simp]
theorem List.bidirectionalRec_singleton {α : Type u} {motive : List αSort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive lmotive (a :: (l ++ [b]))) (a : α) :
List.bidirectionalRec nil singleton cons_append [a] = singleton a
@[simp]
theorem List.bidirectionalRec_cons_append {α : Type u} {motive : List αSort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive lmotive (a :: (l ++ [b]))) (a : α) (l : List α) (b : α) :
List.bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) = cons_append a l b (List.bidirectionalRec nil singleton cons_append l)
@[reducible, inline]
abbrev List.bidirectionalRecOn {α : Type u} {C : List αSort u_2} (l : List α) (H0 : C []) (H1 : (a : α) → C [a]) (Hn : (a : α) → (l : List α) → (b : α) → C lC (a :: (l ++ [b]))) :
C l

Like bidirectionalRec, but with the list parameter placed first.

Equations
Instances For

### sublists #

theorem List.Sublist.cons_cons {α : Type u} {l₁ : List α} {l₂ : List α} (a : α) (s : l₁.Sublist l₂) :
(a :: l₁).Sublist (a :: l₂)
theorem List.sublist_cons_of_sublist {α : Type u} {l₁ : List α} {l₂ : List α} (a : α) (h : l₁.Sublist l₂) :
l₁.Sublist (a :: l₂)
theorem List.tail_sublist {α : Type u} (l : List α) :
l.tail.Sublist l
theorem List.Sublist.tail {α : Type u} {l₁ : List α} {l₂ : List α} :
l₁.Sublist l₂l₁.tail.Sublist l₂.tail
theorem List.Sublist.of_cons_cons {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} {b : α} (h : (a :: l₁).Sublist (b :: l₂)) :
l₁.Sublist l₂
@[deprecated]
theorem List.sublist_of_cons_sublist_cons {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} (h : (a :: l₁).Sublist (a :: l₂)) :
l₁.Sublist l₂
@[deprecated List.cons_sublist_cons]
theorem List.cons_sublist_cons_iff :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist (a :: l₂) l₁.Sublist l₂

Alias of List.cons_sublist_cons.

theorem List.eq_nil_of_sublist_nil {α : Type u} {l : List α} (s : l.Sublist []) :
l = []
theorem List.sublist_nil_iff_eq_nil {α : Type u_1} {l : List α} :
l.Sublist [] l = []

Alias of List.sublist_nil.

@[simp]
theorem List.sublist_singleton {α : Type u} {l : List α} {a : α} :
l.Sublist [a] l = [] l = [a]
theorem List.sublist_replicate_iff {α : Type u} {l : List α} {a : α} {n : } :
l.Sublist () ∃ (k : ), k n l =
theorem List.Sublist.antisymm {α : Type u} {l₁ : List α} {l₂ : List α} (s₁ : l₁.Sublist l₂) (s₂ : l₂.Sublist l₁) :
l₁ = l₂
instance List.decidableSublist {α : Type u} [] (l₁ : List α) (l₂ : List α) :
Decidable (l₁.Sublist l₂)
Equations
• [].decidableSublist x =
• (head :: tail).decidableSublist [] =
• (a :: l₁).decidableSublist (b :: l₂) = if h : a = b then else

### indexOf #

@[simp]
theorem List.indexOf_cons_self {α : Type u} [] (a : α) (l : List α) :
List.indexOf a (a :: l) = 0
theorem List.indexOf_cons_eq {α : Type u} [] {a : α} {b : α} (l : List α) :
b = aList.indexOf a (b :: l) = 0
@[simp]
theorem List.indexOf_cons_ne {α : Type u} [] {a : α} {b : α} (l : List α) :
b aList.indexOf a (b :: l) = ().succ
theorem List.indexOf_eq_length {α : Type u} [] {a : α} {l : List α} :
= l.length ¬a l
@[simp]
theorem List.indexOf_of_not_mem {α : Type u} [] {l : List α} {a : α} :
¬a l = l.length
theorem List.indexOf_le_length {α : Type u} [] {a : α} {l : List α} :
l.length
theorem List.indexOf_lt_length {α : Type u} [] {a : α} {l : List α} :
< l.length a l
theorem List.indexOf_append_of_mem {α : Type u} {l₁ : List α} {l₂ : List α} [] {a : α} (h : a l₁) :
List.indexOf a (l₁ ++ l₂) = List.indexOf a l₁
theorem List.indexOf_append_of_not_mem {α : Type u} {l₁ : List α} {l₂ : List α} [] {a : α} (h : ¬a l₁) :
List.indexOf a (l₁ ++ l₂) = l₁.length + List.indexOf a l₂

### nth element #

@[deprecated List.get_of_mem]
theorem List.nthLe_of_mem {α : Type u} {a : α} {l : List α} (h : a l) :
∃ (n : ), ∃ (h : n < l.length), l.nthLe n h = a
@[deprecated List.get?_eq_get]
theorem List.nthLe_get? {α : Type u} {l : List α} {n : } (h : n < l.length) :
l.get? n = some (l.nthLe n h)
@[simp]
theorem List.get?_length {α : Type u} (l : List α) :
l.get? l.length = none
@[deprecated List.get_mem]
theorem List.nthLe_mem {α : Type u} (l : List α) (n : ) (h : n < l.length) :
l.nthLe n h l
@[deprecated List.mem_iff_get]
theorem List.mem_iff_nthLe {α : Type u} {a : α} {l : List α} :
a l ∃ (n : ), ∃ (h : n < l.length), l.nthLe n h = a
@[deprecated List.get?_inj]
theorem List.get?_injective {i : } :
∀ {α : Type u_1} {xs : List α} {j : }, i < xs.lengthxs.Nodupxs.get? i = xs.get? ji = j

Alias of List.get?_inj.

@[deprecated List.get_map]
theorem List.nthLe_map {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : } (H1 : n < (List.map f l).length) (H2 : n < l.length) :
(List.map f l).nthLe n H1 = f (l.nthLe n H2)
theorem List.get_map_rev {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : Fin l.length} :
f (l.get n) = (List.map f l).get n,

A version of get_map that can be used for rewriting.

@[deprecated List.get_map_rev]
theorem List.nthLe_map_rev {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : } (H : n < l.length) :
f (l.nthLe n H) = (List.map f l).nthLe n

A version of nthLe_map that can be used for rewriting.

@[simp, deprecated List.get_map]
theorem List.nthLe_map' {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : } (H : n < (List.map f l).length) :
(List.map f l).nthLe n H = f (l.nthLe n )
@[simp, deprecated List.get_singleton]
theorem List.nthLe_singleton {α : Type u} (a : α) {n : } (hn : n < 1) :
[a].nthLe n hn = a
@[deprecated List.get_append_right']
theorem List.nthLe_append_right {α : Type u} {l₁ : List α} {l₂ : List α} {n : } (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
(l₁ ++ l₂).nthLe n h₂ = l₂.nthLe (n - l₁.length)
theorem List.get_length_sub_one {α : Type u} {l : List α} (h : l.length - 1 < l.length) :
l.get l.length - 1, h = l.getLast
@[deprecated List.get_cons_length]
theorem List.nthLe_cons_length {α : Type u} (x : α) (xs : List α) (n : ) (h : n = xs.length) :
(x :: xs).nthLe n = (x :: xs).getLast
theorem List.take_one_drop_eq_of_lt_length {α : Type u} {l : List α} {n : } (h : n < l.length) :
List.take 1 () = [l.get n, h]
theorem List.ext_get? {α : Type u_1} {l₁ : List α} {l₂ : List α} :
(∀ (n : ), l₁.get? n = l₂.get? n)l₁ = l₂

Alias of List.ext.

theorem List.ext_get?' {α : Type u} {l₁ : List α} {l₂ : List α} (h' : ∀ (n : ), n < max l₁.length l₂.lengthl₁.get? n = l₂.get? n) :
l₁ = l₂
theorem List.ext_get?_iff {α : Type u} {l₁ : List α} {l₂ : List α} :
l₁ = l₂ ∀ (n : ), l₁.get? n = l₂.get? n
theorem List.ext_get_iff {α : Type u} {l₁ : List α} {l₂ : List α} :
l₁ = l₂ l₁.length = l₂.length ∀ (n : ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get n, h₁ = l₂.get n, h₂
theorem List.ext_get?_iff' {α : Type u} {l₁ : List α} {l₂ : List α} :
l₁ = l₂ ∀ (n : ), n < max l₁.length l₂.lengthl₁.get? n = l₂.get? n
@[deprecated List.ext_get]
theorem List.ext_nthLe {α : Type u} {l₁ : List α} {l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.nthLe n h₁ = l₂.nthLe n h₂) :
l₁ = l₂
@[simp]
theorem List.indexOf_get {α : Type u} [] {a : α} {l : List α} (h : < l.length) :
l.get , h = a
@[simp]
theorem List.indexOf_get? {α : Type u} [] {a : α} {l : List α} (h : a l) :
l.get? () = some a
@[deprecated]
theorem List.get_reverse_aux₁ {α : Type u} (l : List α) (r : List α) (i : ) (h1 : i + l.length < (l.reverseAux r).length) (h2 : i < r.length) :
(l.reverseAux r).get i + l.length, h1 = r.get i, h2
theorem List.indexOf_inj {α : Type u} [] {l : List α} {x : α} {y : α} (hx : x l) (hy : y l) :
= x = y
theorem List.get_reverse_aux₂ {α : Type u} (l : List α) (r : List α) (i : ) (h1 : l.length - 1 - i < (l.reverseAux r).length) (h2 : i < l.length) :
(l.reverseAux r).get l.length - 1 - i, h1 = l.get i, h2
@[simp]
theorem List.get_reverse {α : Type u} (l : List α) (i : ) (h1 : l.length - 1 - i < l.reverse.length) (h2 : i < l.length) :
l.reverse.get l.length - 1 - i, h1 = l.get i, h2
@[simp, deprecated List.get_reverse]
theorem List.nthLe_reverse {α : Type u} (l : List α) (i : ) (h1 : l.length - 1 - i < l.reverse.length) (h2 : i < l.length) :
l.reverse.nthLe (l.length - 1 - i) h1 = l.nthLe i h2
@[deprecated List.get_reverse']
theorem List.nthLe_reverse' {α : Type u} (l : List α) (n : ) (hn : n < l.reverse.length) (hn' : l.length - 1 - n < l.length) :
l.reverse.nthLe n hn = l.nthLe (l.length - 1 - n) hn'
theorem List.get_reverse' {α : Type u} (l : List α) (n : Fin l.reverse.length) (hn' : l.length - 1 - n < l.length) :
l.reverse.get n = l.get l.length - 1 - n, hn'
theorem List.eq_cons_of_length_one {α : Type u} {l : List α} (h : l.length = 1) :
l = [l.nthLe 0 ]
theorem List.modifyNthTail_modifyNthTail {α : Type u} {f : List αList α} {g : List αList α} (m : ) (n : ) (l : List α) :
List.modifyNthTail g (m + n) () = List.modifyNthTail (fun (l : List α) => List.modifyNthTail g m (f l)) n l
theorem List.modifyNthTail_modifyNthTail_le {α : Type u} {f : List αList α} {g : List αList α} (m : ) (n : ) (l : List α) (h : n m) :
List.modifyNthTail g m () = List.modifyNthTail (fun (l : List α) => List.modifyNthTail g (m - n) (f l)) n l
theorem List.modifyNthTail_modifyNthTail_same {α : Type u} {f : List αList α} {g : List αList α} (n : ) (l : List α) :
@[deprecated List.eraseIdx_eq_modifyNthTail]
theorem List.removeNth_eq_nthTail {α : Type u_1} (n : ) (l : List α) :
l.eraseIdx n = List.modifyNthTail List.tail n l

Alias of List.eraseIdx_eq_modifyNthTail.

theorem List.modifyNth_eq_set {α : Type u} (f : αα) (n : ) (l : List α) :
= ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l theorem List.length_modifyNthTail {α : Type u} (f : List αList α) (H : ∀ (l : List α), (f l).length = l.length) (n : ) (l : List α) : ().length = l.length theorem List.length_modifyNth {α : Type u} (f : αα) (n : ) (l : List α) : ().length = l.length @[simp] theorem List.get_set_of_ne {α : Type u} {l : List α} {i : } {j : } (h : i j) (a : α) (hj : j < (l.set i a).length) : (l.set i a).get j, hj = l.get j, ### map # theorem List.map_eq_foldr {α : Type u} {β : Type v} (f : αβ) (l : List α) : List.map f l = List.foldr (fun (a : α) (bs : List β) => f a :: bs) [] l theorem List.map_congr {α : Type u} {β : Type v} {f : αβ} {g : αβ} {l : List α} : (∀ (x : α), x lf x = g x)List.map f l = List.map g l theorem List.map_eq_map_iff {α : Type u} {β : Type v} {f : αβ} {g : αβ} {l : List α} : List.map f l = List.map g l ∀ (x : α), x lf x = g x theorem List.map_concat {α : Type u} {β : Type v} (f : αβ) (a : α) (l : List α) : List.map f (l.concat a) = (List.map f l).concat (f a) theorem List.map_id'' {α : Type u} {f : αα} (h : ∀ (x : α), f x = x) (l : List α) : List.map f l = l theorem List.eq_nil_of_map_eq_nil {α : Type u} {β : Type v} {f : αβ} {l : List α} (h : List.map f l = []) : l = [] @[simp] theorem List.map_join {α : Type u} {β : Type v} (f : αβ) (L : List (List α)) : List.map f L.join = (List.map () L).join theorem List.bind_pure_eq_map {α : Type u} {β : Type v} (f : αβ) (l : List α) : l.bind (pure f) = List.map f l @[deprecated List.bind_pure_eq_map] theorem List.bind_ret_eq_map {α : Type u} {β : Type v} (f : αβ) (l : List α) : l.bind (List.ret f) = List.map f l theorem List.bind_congr {α : Type u} {β : Type v} {l : List α} {f : αList β} {g : αList β} (h : ∀ (x : α), x lf x = g x) : l.bind f = l.bind g theorem List.infix_bind_of_mem {α : Type u} {a : α} {as : List α} (h : a as) (f : αList α) : f a <:+: as.bind f @[simp] theorem List.map_eq_map {α : Type u_2} {β : Type u_2} (f : αβ) (l : List α) : f <$> l = List.map f l
@[simp]
theorem List.map_tail {α : Type u} {β : Type v} (f : αβ) (l : List α) :
List.map f l.tail = (List.map f l).tail
theorem List.comp_map {α : Type u} {β : Type v} {γ : Type w} (h : βγ) (g : αβ) (l : List α) :
List.map (h g) l = List.map h (List.map g l)

A single List.map of a composition of functions is equal to composing a List.map with another List.map, fully applied. This is the reverse direction of List.map_map.

@[simp]
theorem List.map_comp_map {α : Type u} {β : Type v} {γ : Type w} (g : βγ) (f : αβ) :
= List.map (g f)

Composing a List.map with another List.map is equal to a single List.map of composed functions.

theorem Function.LeftInverse.list_map {α : Type u} {β : Type v} {f : αβ} {g : βα} (h : ) :
theorem Function.RightInverse.list_map {α : Type u} {β : Type v} {f : αβ} {g : βα} (h : ) :
theorem Function.Involutive.list_map {α : Type u} {f : αα} (h : ) :
@[simp]
theorem List.map_leftInverse_iff {α : Type u} {β : Type v} {f : αβ} {g : βα} :
@[simp]
theorem List.map_rightInverse_iff {α : Type u} {β : Type v} {f : αβ} {g : βα} :
@[simp]
theorem List.map_involutive_iff {α : Type u} {f : αα} :
theorem Function.Injective.list_map {α : Type u} {β : Type v} {f : αβ} (h : ) :
@[simp]
theorem List.map_injective_iff {α : Type u} {β : Type v} {f : αβ} :
theorem Function.Surjective.list_map {α : Type u} {β : Type v} {f : αβ} (h : ) :
@[simp]
theorem List.map_surjective_iff {α : Type u} {β : Type v} {f : αβ} :
theorem Function.Bijective.list_map {α : Type u} {β : Type v} {f : αβ} (h : ) :
@[simp]
theorem List.map_bijective_iff {α : Type u} {β : Type v} {f : αβ} :
theorem List.map_filter_eq_foldr {α : Type u} {β : Type v} (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
theorem List.getLast_map {α : Type u} {β : Type v} (f : αβ) {l : List α} (hl : l []) :
(List.map f l).getLast = f (l.getLast hl)
theorem List.map_eq_replicate_iff {α : Type u} {β : Type v} {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} {β : Type v} (l : List α) (b : β) :
List.map () l = List.replicate l.length b
@[simp]
theorem List.map_const' {α : Type u} {β : Type v} (l : List α) (b : β) :
List.map (fun (x : α) => b) l = List.replicate l.length b
theorem List.eq_of_mem_map_const {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {l : List α} (h : b₁ List.map () l) :
b₁ = b₂

### zipWith #

theorem List.nil_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (l : List β) :
List.zipWith f [] l = []
theorem List.zipWith_nil {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (l : List α) :
List.zipWith f l [] = []
@[simp]
theorem List.zipWith_flip {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (as : List α) (bs : List β) :
List.zipWith (flip f) bs as = List.zipWith f as bs

### take, drop #

theorem List.take_cons {α : Type u} (n : ) (a : α) (l : List α) :
List.take n.succ (a :: l) = a ::
@[simp]
theorem List.drop_tail {α : Type u} (l : List α) (n : ) :
List.drop n l.tail = List.drop (n + 1) l
theorem List.cons_get_drop_succ {α : Type u} {l : List α} {n : Fin l.length} :
l.get n :: List.drop (n + 1) l = List.drop (n) l
@[simp]
theorem List.takeI_length {α : Type u} [] (n : ) (l : List α) :
().length = n
@[simp]
theorem List.takeI_nil {α : Type u} [] (n : ) :
List.takeI n [] = List.replicate n default
theorem List.takeI_eq_take {α : Type u} [] {n : } {l : List α} :
n l.length =
@[simp]
theorem List.takeI_left {α : Type u} [] (l₁ : List α) (l₂ : List α) :
List.takeI l₁.length (l₁ ++ l₂) = l₁
theorem List.takeI_left' {α : Type u} [] {l₁ : List α} {l₂ : List α} {n : } (h : l₁.length = n) :
List.takeI n (l₁ ++ l₂) = l₁
@[simp]
theorem List.takeD_length {α : Type u} (n : ) (l : List α) (a : α) :
(List.takeD n l a).length = n
theorem List.takeD_eq_take {α : Type u} {n : } {l : List α} (a : α) :
n l.lengthList.takeD n l a =
@[simp]
theorem List.takeD_left {α : Type u} (l₁ : List α) (l₂ : List α) (a : α) :
List.takeD l₁.length (l₁ ++ l₂) a = l₁
theorem List.takeD_left' {α : Type u} {l₁ : List α} {l₂ : List α} {n : } {a : α} (h : l₁.length = n) :
List.takeD n (l₁ ++ l₂) a = l₁

### foldl, foldr #

theorem List.foldl_ext {α : Type u} {β : Type v} (f : αβα) (g : αβα) (a : α) {l : List β} (H : ∀ (a : α) (b : β), b lf a b = g a b) :
List.foldl f a l = List.foldl g a l
theorem List.foldr_ext {α : Type u} {β : Type v} (f : αββ) (g : αββ) (b : β) {l : List α} (H : ∀ (a : α), a l∀ (b : β), f a b = g a b) :
List.foldr f b l = List.foldr g b l
theorem List.foldl_concat {α : Type u} {β : Type v} (f : βαβ) (b : β) (x : α) (xs : List α) :
List.foldl f b (xs ++ [x]) = f (List.foldl f b xs) x
theorem List.foldr_concat {α : Type u} {β : Type v} (f : αββ) (b : β) (x : α) (xs : List α) :
List.foldr f b (xs ++ [x]) = List.foldr f (f x b) xs
theorem List.foldl_fixed' {α : Type u} {β : Type v} {f : αβα} {a : α} (hf : ∀ (b : β), f a b = a) (l : List β) :
List.foldl f a l = a
theorem List.foldr_fixed' {α : Type u} {β : Type v} {f : αββ} {b : β} (hf : ∀ (a : α), f a b = b) (l : List α) :
List.foldr f b l = b
@[simp]
theorem List.foldl_fixed {α : Type u} {β : Type v} {a : α} (l : List β) :
List.foldl (fun (a : α) (x : β) => a) a l = a
@[simp]
theorem List.foldr_fixed {α : Type u} {β : Type v} {b : β} (l : List α) :
List.foldr (fun (x : α) (b : β) => b) b l = b
@[simp]
theorem List.foldl_join {α : Type u} {β : Type v} (f : αβα) (a : α) (L : List (List β)) :
List.foldl f a L.join = List.foldl () a L
@[simp]
theorem List.foldr_join {α : Type u} {β : Type v} (f : αββ) (b : β) (L : List (List α)) :
List.foldr f b L.join = List.foldr (fun (l : List α) (b : β) => List.foldr f b l) b L
theorem List.foldr_eta {α : Type u} (l : List α) :
List.foldr List.cons [] l = l
@[simp]
theorem List.reverse_foldl {α : Type u} {l : List α} :
(List.foldl (fun (t : List α) (h : α) => h :: t) [] l).reverse = 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_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : αβγ) (op₁ : αια) (op₂ : βιβ) (op₃ : γιγ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i) :
List.foldl op₃ (f a b) l = f (List.foldl op₁ a l) (List.foldl op₂ b l)
theorem List.foldr_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : αβγ) (op₁ : ιαα) (op₂ : ιββ) (op₃ : ιγγ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)) :
List.foldr op₃ (f a b) l = f (List.foldr op₁ a l) (List.foldr op₂ b l)
theorem List.injective_foldl_comp {α : Type u} {l : List (αα)} {f : αα} (hl : ∀ (f : αα), f l) (hf : ) :
Function.Injective (List.foldl Function.comp f l)
def List.foldrRecOn {α : Type u} {β : Type v} {C : βSort u_2} (l : List α) (op : αββ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a lC (op a b)) :
C (List.foldr op b l)

Induction principle for values produced by a foldr: if a property holds for the seed element b : β and for all incremental op : α → β → β performed on the elements (a : α) ∈ l. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def List.foldlRecOn {α : Type u} {β : Type v} {C : βSort u_2} (l : List α) (op : βαβ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a lC (op b a)) :
C (List.foldl op b l)

Induction principle for values produced by a foldl: if a property holds for the seed element b : β and for all incremental op : β → α → β performed on the elements (a : α) ∈ l. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem List.foldrRecOn_nil {α : Type u} {β : Type v} {C : βSort u_2} (op : αββ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a []C (op a b)) :
[].foldrRecOn op b hb hl = hb
@[simp]
theorem List.foldrRecOn_cons {α : Type u} {β : Type v} {C : βSort u_2} (x : α) (l : List α) (op : αββ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a x :: lC (op a b)) :
(x :: l).foldrRecOn op b hb hl = hl (List.foldr op b l) (l.foldrRecOn op b hb fun (b : β) (hb : C b) (a : α) (ha : a l) => hl b hb a ) x
@[simp]
theorem List.foldlRecOn_nil {α : Type u} {β : Type v} {C : βSort u_2} (op : βαβ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a []C (op b a)) :
[].foldlRecOn op b hb hl = hb
theorem List.append_cons_inj_of_not_mem {α : Type u} {x₁ : List α} {x₂ : List α} {z₁ : List α} {z₂ : List α} {a₁ : α} {a₂ : α} (notin_x : ¬a₂ x₁) (notin_z : ¬a₂ z₁) :
x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ x₁ = x₂ a₁ = a₂ z₁ = z₂

Consider two lists l₁ and l₂ with designated elements a₁ and a₂ somewhere in them: l₁ = x₁ ++ [a₁] ++ z₁ and l₂ = x₂ ++ [a₂] ++ z₂. Assume the designated element a₂ is present in neither x₁ nor z₁. We conclude that the lists are equal (l₁ = l₂) if and only if their respective parts are equal (x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂).

theorem List.length_scanl {α : Type u} {β : Type v} {f : βαβ} (a : β) (l : List α) :
(List.scanl f a l).length = l.length + 1
@[simp]
theorem List.scanl_nil {α : Type u} {β : Type v} {f : βαβ} (b : β) :
List.scanl f b [] = [b]
@[simp]
theorem List.scanl_cons {α : Type u} {β : Type v} {f : βαβ} {b : β} {a : α} {l : List α} :
List.scanl f b (a :: l) = [b] ++ List.scanl f (f b a) l
@[simp]
theorem List.get?_zero_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} :
(List.scanl f b l).get? 0 = some b
@[simp]
theorem List.get_zero_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {h : 0 < (List.scanl f b l).length} :
(List.scanl f b l).get 0, h = b
@[simp, deprecated List.get_zero_scanl]
theorem List.nthLe_zero_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {h : 0 < (List.scanl f b l).length} :
(List.scanl f b l).nthLe 0 h = b
theorem List.get?_succ_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {i : } :
(List.scanl f b l).get? (i + 1) = ((List.scanl f b l).get? i).bind fun (x : β) => Option.map (fun (y : α) => f x y) (l.get? i)
@[deprecated List.get_succ_scanl]
theorem List.nthLe_succ_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {i : } {h : i + 1 < (List.scanl f b l).length} :
(List.scanl f b l).nthLe (i + 1) h = f ((List.scanl f b l).nthLe i ) (l.nthLe i )
theorem List.get_succ_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {i : } {h : i + 1 < (List.scanl f b l).length} :
(List.scanl f b l).get i + 1, h = f ((List.scanl f b l).get i, ) (l.get i, )
@[simp]
theorem List.scanr_nil {α : Type u} {β : Type v} (f : αββ) (b : β) :
List.scanr f b [] = [b]
@[simp]
theorem List.scanr_cons {α : Type u} {β : Type v} (f : αββ) (b : β) (a : α) (l : List α) :
List.scanr f b (a :: l) = List.foldr f b (a :: l) :: List.scanr f b l
theorem List.foldl1_eq_foldr1 {α : Type u} {f : ααα} (hassoc : ) (a : α) (b : α) (l : List α) :
List.foldl f a (l ++ [b]) = List.foldr f b (a :: l)
theorem List.foldl_eq_of_comm_of_assoc {α : Type u} {f : ααα} (hcomm : ) (hassoc : ) (a : α) (b : α) (l : List α) :
List.foldl f a (b :: l) = f b (List.foldl f a l)
theorem List.foldl_eq_foldr {α : Type u} {f : ααα} (hcomm : ) (hassoc : ) (a : α) (l : List α) :
List.foldl f a l = List.foldr f a l
theorem List.foldl_eq_of_comm' {α : Type u} {β : Type v} {f : αβα} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (b : β) (l : List β) :
List.foldl f a (b :: l) = f (List.foldl f a l) b
theorem List.foldl_eq_foldr' {α : Type u} {β : Type v} {f : αβα} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (l : List β) :
List.foldl f a l = List.foldr (flip f) a l
theorem List.foldr_eq_of_comm' {α : Type u} {β : Type v} {f : αββ} (hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)) (a : β) (b : α) (l : List α) :
List.foldr f a (b :: l) = List.foldr f (f b a) l
theorem List.foldl_assoc {α : Type u} {op : ααα} [ha : ] {l : List α} {a₁ : α} {a₂ : α} :
List.foldl op (op a₁ a₂) l = op a₁ (List.foldl op a₂ l)
theorem List.foldl_op_eq_op_foldr_assoc {α : Type u} {op : ααα} [ha : ] {l : List α} {a₁ : α} {a₂ : α} :
op (List.foldl op a₁ l) a₂ = op a₁ (List.foldr (fun (x x_1 : α) => op x x_1) a₂ l)
theorem List.foldl_assoc_comm_cons {α : Type u} {op : ααα} [ha : ] [hc : ] {l : List α} {a₁ : α} {a₂ : α} :
List.foldl op a₂ (a₁ :: l) = op a₁ (List.foldl op a₂ l)

### foldlM, foldrM, mapM #

theorem List.foldrM_eq_foldr {α : Type u} {β : Type v} {m : Type v → Type w} [] [] (f : αβm β) (b : β) (l : List α) :
List.foldrM f b l = List.foldr (fun (a : α) (mb : m β) => mb >>= f a) (pure b) l
theorem List.foldlM_eq_foldl {α : Type u} {β : Type v} {m : Type v → Type w} [] [] (f : βαm β) (b : β) (l : List α) :
List.foldlM f b l = List.foldl (fun (mb : m β) (a : α) => do let bmb f b a) (pure b) l

### intersperse #

@[simp]
theorem List.intersperse_singleton {α : Type u} (a : α) (b : α) :
@[simp]
theorem List.intersperse_cons_cons {α : Type u} (a : α) (b : α) (c : α) (tl : List α) :
List.intersperse a (b :: c :: tl) = b :: a :: List.intersperse a (c :: tl)

### splitAt and splitOn #

@[simp]
theorem List.splitAt_eq_take_drop {α : Type u} (n : ) (l : List α) :
= (, )
theorem List.splitAt_eq_take_drop.go_eq_take_drop {α : Type u} (n : ) (l : List α) (xs : List α) (acc : ) :
List.splitAt.go l xs n acc = if n < xs.length then (acc.toList ++ List.take n xs, List.drop n xs) else (l, [])
@[simp]
theorem List.splitOn_nil {α : Type u} [] (a : α) :
List.splitOn a [] = [[]]
@[simp]
theorem List.splitOnP_nil {α : Type u} (p : αBool) :
= [[]]
theorem List.splitOnP.go_ne_nil {α : Type u} (p : αBool) (xs : List α) (acc : List α) :
List.splitOnP.go p xs acc []
theorem List.splitOnP.go_acc {α : Type u} (p : αBool) (xs : List α) (acc : List α) :
List.splitOnP.go p xs acc = List.modifyHead (fun (x : List α) => acc.reverse ++ x) ()
theorem List.splitOnP_ne_nil {α : Type u} (p : αBool) (xs : List α) :
[]
@[simp]
theorem List.splitOnP_cons {α : Type u} (p : αBool) (x : α) (xs : List α) :
List.splitOnP p (x :: xs) = if p x = true then [] :: else List.modifyHead () ()
theorem List.splitOnP_spec {α : Type u} (p : αBool) (as : List α) :
(List.zipWith (fun (x x_1 : List α) => x ++ x_1) () (List.map (fun (x : α) => [x]) (List.filter p as) ++ [[]])).join = as

The original list L can be recovered by joining the lists produced by splitOnP p L, interspersed with the elements L.filter p.

theorem List.splitOnP_spec.join_zipWith {α : Type u} {xs : List (List α)} {ys : List (List α)} {a : α} (hxs : xs []) (hys : ys []) :
(List.zipWith (fun (x x_1 : List α) => x ++ x_1) (List.modifyHead () xs) ys).join = a :: (List.zipWith (fun (x x_1 : List α) => x ++ x_1) xs ys).join
theorem List.splitOnP_eq_single {α : Type u} (p : αBool) (xs : List α) (h : ∀ (x : α), x xs¬p x = true) :
= [xs]

If no element satisfies p in the list xs, then xs.splitOnP p = [xs]

theorem List.splitOnP_first {α : Type u} (p : αBool) (xs : List α) (h : ∀ (x : α), x xs¬p x = true) (sep : α) (hsep : p sep = true) (as : List α) :
List.splitOnP p (xs ++ sep :: as) = xs ::

When a list of the form [...xs, sep, ...as] is split on p, the first element is xs, assuming no element in xs satisfies p but sep does satisfy p

theorem List.intercalate_splitOn {α : Type u} (xs : List α) (x : α) [] :
[x].intercalate (List.splitOn x xs) = xs

intercalate [x] is the left inverse of splitOn x

theorem List.splitOn_intercalate {α : Type u} (ls : List (List α)) [] (x : α) (hx : ∀ (l : List α), l ls¬x l) (hls : ls []) :
List.splitOn x ([x].intercalate ls) = ls

splitOn x is the left inverse of intercalate [x], on the domain consisting of each nonempty list of lists ls whose elements do not contain x

### modifyLast #

theorem List.modifyLast.go_append_one {α : Type u} (f : αα) (a : α) (tl : List α) (r : ) :
List.modifyLast.go f (tl ++ [a]) r = r.toListAppend (List.modifyLast.go f (tl ++ [a]) #[])
theorem List.modifyLast_append_one {α : Type u} (f : αα) (a : α) (l : List α) :
List.modifyLast f (l ++ [a]) = l ++ [f a]
theorem List.modifyLast_append {α : Type u} (f : αα) (l₁ : List α) (l₂ : List α) :
l₂ []List.modifyLast f (l₁ ++ l₂) = l₁ ++

### map for partial functions #

@[simp]
theorem List.attach_nil {α : Type u} :
[].attach = []
theorem List.sizeOf_lt_sizeOf_of_mem {α : Type u} [] {x : α} {l : List α} (hx : x l) :
<
@[simp]
theorem List.pmap_eq_map {α : Type u} {β : Type v} (p : αProp) (f : αβ) (l : List α) (H : ∀ (a : α), a lp a) :
List.pmap (fun (a : α) (x : p a) => f a) l H = List.map f l
theorem List.pmap_congr {α : Type u} {β : Type v} {p : αProp} {q : αProp} {f : (a : α) → p aβ} {g : (a : α) → q aβ} (l : List α) {H₁ : ∀ (a : α), a lp a} {H₂ : ∀ (a : α), a lq a} (h : ∀ (a : α), a l∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) :
List.pmap f l H₁ = List.pmap g l H₂
theorem List.map_pmap {α : Type u} {β : Type v} {γ : Type w} {p : αProp} (g : βγ) (f : (a : α) → p aβ) (l : List α) (H : ∀ (a : α), a lp a) :
List.map g (List.pmap f l H) = List.pmap (fun (a : α) (h : p a) => g (f a h)) l H
theorem List.pmap_map {α : Type u} {β : Type v} {γ : Type w} {p : βProp} (g : (b : β) → p bγ) (f : αβ) (l : List α) (H : ∀ (a : β), a List.map f lp a) :
List.pmap g (List.map f l) H = List.pmap (fun (a : α) (h : p (f a)) => g (f a) h) l
theorem List.pmap_eq_map_attach {α : Type u} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (l : List α) (H : ∀ (a : α), a lp a) :
List.pmap f l H = List.map (fun (x : { x : α // x l }) => f x ) l.attach
theorem List.attach_map_coe' {α : Type u} {β : Type v} (l : List α) (f : αβ) :
List.map (fun (i : { i : α // i l }) => f i) l.attach = List.map f l
theorem List.attach_map_val' {α : Type u} {β : Type v} (l : List α) (f : αβ) :
List.map (fun (i : { x : α // x l }) => f i) l.attach = List.map f l
@[simp]
theorem List.attach_map_val {α : Type u} (l : List α) :
List.map Subtype.val l.attach = l
@[simp]
theorem List.mem_attach {α : Type u} (l : List α) (x : { x : α // x l }) :
x l.attach
@[simp]
theorem List.mem_pmap {α : Type u} {β : Type v} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} {b : β} :
b List.pmap f l H ∃ (a : α), ∃ (h : a l), f a = b
@[simp]
theorem List.length_pmap {α : Type u} {β : Type v} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} :
(List.pmap f l H).length = l.length
@[simp]
theorem List.length_attach {α : Type u} (L : List α) :
L.attach.length = L.length
@[simp]
theorem List.pmap_eq_nil {α : Type u} {β : Type v} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : ∀ (a : α), a lp a} :
List.pmap f l H = [] l = []
@[simp]
theorem List.attach_eq_nil {α : Type u} (l : List α) :
l.attach = [] l = []
theorem List.getLast_pmap {α : Type u} {β : Type v} (p : αProp) (f : (a : α) → p aβ) (l : List α) (hl₁ : ∀ (a : α), a lp a) (hl₂ : l []) :
(List.pmap f l hl₁).getLast = f (l.getLast hl₂)
theorem List.get?_pmap {α : Type u} {β : Type v} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : ∀ (a : α), a lp a) (n : ) :
(List.pmap f l h).get? n = Option.pmap f (l.get? n)
theorem List.get_pmap {α : Type u} {β : Type v} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : ∀ (a : α), a lp a) {n : } (hn : n < (List.pmap f l h).length) :
(List.pmap f l h).get n, hn = f (l.get n, )
@[deprecated List.get_pmap]
theorem List.nthLe_pmap {α : Type u} {β : Type v} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : ∀ (a : α), a lp a) {n : } (hn : n < (List.pmap f l h).length) :
(List.pmap f l h).nthLe n hn = f (l.nthLe n )
theorem List.pmap_append {ι : Type u_1} {α : Type u} {p : ιProp} (f : (a : ι) → p aα) (l₁ : List ι) (l₂ : List ι) (h : ∀ (a : ι), a l₁ ++ l₂p a) :
List.pmap f (l₁ ++ l₂) h = List.pmap f l₁ ++ List.pmap f l₂
theorem List.pmap_append' {α : Type u} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (l₁ : List α) (l₂ : List α) (h₁ : ∀ (a : α), a l₁p a) (h₂ : ∀ (a : α), a l₂p a) :
List.pmap f (l₁ ++ l₂) = List.pmap f l₁ h₁ ++ List.pmap f l₂ h₂

### find #

@[deprecated List.mem_of_find?_eq_some]
theorem List.find?_mem :
∀ {α : Type u_1} {p : αBool} {a : α} {l : List α}, = some aa l

Alias of List.mem_of_find?_eq_some.

### lookmap #

theorem List.lookmap.go_append {α : Type u} (f : α) (l : List α) (acc : ) :
List.lookmap.go f l acc = acc.toListAppend ()
@[simp]
theorem List.lookmap_nil {α : Type u} (f : α) :
List.lookmap f [] = []
@[simp]
theorem List.lookmap_cons_none {α : Type u} (f : α) {a : α} (l : List α) (h : f a = none) :
List.lookmap f (a :: l) = a ::
@[simp]
theorem List.lookmap_cons_some {α : Type u} (f : α) {a : α} {b : α} (l : List α) (h : f a = some b) :
List.lookmap f (a :: l) = b :: l
theorem List.lookmap_some {α : Type u} (l : List α) :
List.lookmap some l = l
theorem List.lookmap_none {α : Type u} (l : List α) :
List.lookmap (fun (x : α) => none) l = l
theorem List.lookmap_congr {α : Type u} {f : α} {g : α} {l : List α} :
(∀ (a : α), a lf a = g a) =
theorem List.lookmap_of_forall_not {α : Type u} (f : α) {l : List α} (H : ∀ (a : α), a lf a = none) :
= l
theorem List.lookmap_map_eq {α : Type u} {β : Type v} (f : α) (g : αβ) (h : ∀ (a b : α), b f ag a = g b) (l : List α) :
theorem List.lookmap_id' {α : Type u} (f : α) (h : ∀ (a b : α), b f aa = b) (l : List α) :
= l
theorem List.length_lookmap {α : Type u} (f : α) (l : List α) :
().length = l.length

### filter #

theorem List.length_eq_length_filter_add {α : Type u} {l : List α} (f : αBool) :
l.length = ().length + (List.filter (fun (x : α) => !f x) l).length

### filterMap #

theorem List.Sublist.map {α : Type u} {β : Type v} (f : αβ) {l₁ : List α} {l₂ : List α} (s : l₁.Sublist l₂) :
(List.map f l₁).Sublist (List.map f l₂)
theorem List.filterMap_eq_bind_toList {α : Type u} {β : Type v} (f : α) (l : List α) :
= l.bind fun (a : α) => (f a).toList
theorem List.filterMap_congr {α : Type u} {β : Type v} {f : α} {g : α} {l : List α} (h : ∀ (x : α), x lf x = g x) :
=
theorem List.filterMap_eq_map_iff_forall_eq_some {α : Type u} {β : Type v} {f : α} {g : αβ} {l : List α} :
= List.map g l ∀ (x : α), x lf x = some (g x)

### filter #

theorem List.filter_singleton {α : Type u} {p : αBool} {a : α} :
List.filter p [a] = bif p a then [a] else []
theorem List.filter_eq_foldr {α : Type u} (p : αBool) (l : List α) :
= List.foldr (fun (a : α) (out : List α) => bif p a then a :: out else out) [] l
@[simp]
theorem List.filter_subset {α : Type u} {p : αBool} (l : List α) :
l
theorem List.of_mem_filter {α : Type u} {p : αBool} {a : α} {l : List α} (h : a ) :
p a = true
theorem List.mem_of_mem_filter {α : Type u} {p : αBool} {a : α} {l : List α} (h : a ) :
a l
theorem List.mem_filter_of_mem {α : Type u} {p : αBool} {a : α} {l : List α} (h₁ : a l) (h₂ : p a = true) :
a
theorem List.monotone_filter_left {α : Type u} (p : αBool) ⦃l : List α ⦃l' : List α (h : l l') :
theorem List.monotone_filter_right {α : Type u} (l : List α) ⦃p : αBool ⦃q : αBool (h : ∀ (a : α), p a = trueq a = true) :
().Sublist ()
theorem List.map_filter' {α : Type u} {β : Type v} (p : αBool) {f : αβ} (hf : ) (l : List α) [DecidablePred fun (b : β) => ∃ (a : α), p a = true f a = b] :
List.map f () = List.filter (fun (b : β) => decide (∃ (a : α), p a = true f a = b)) (List.map f l)
theorem List.filter_attach' {α : Type u} (l : List α) (p : { a : α // a l }Bool) [] :
List.filter p l.attach = List.map (Subtype.map id ) (List.filter (fun (x : α) => decide (∃ (h : x l), p x, h = true)) l).attach
theorem List.filter_attach {α : Type u} (l : List α) (p : αBool) :
List.filter (fun (x : { x : α // x l }) => p x) l.attach = List.map (Subtype.map id ) ().attach
theorem List.filter_comm {α : Type u} (p : αBool) (q : αBool) (l : List α) :
@[simp]
theorem List.filter_true {α : Type u} (l : List α) :
List.filter (fun (x : α) => true) l = l
@[simp]
theorem List.filter_false {α : Type u} (l : List α) :
List.filter (fun (x : α) => false) l = []
theorem List.span.loop_eq_take_drop {α : Type u} (p : αBool) (l₁ : List α) (l₂ : List α) :
List.span.loop p l₁ l₂ = (l₂.reverse ++ , )
@[simp]
theorem List.span_eq_take_drop {α : Type u} (p : αBool) (l : List α) :
= (, )
theorem List.dropWhile_nthLe_zero_not {α : Type u} (p : αBool) (l : List α) (hl : 0 < ().length) :
¬p (().nthLe 0 hl) = true
@[simp]
theorem List.dropWhile_eq_nil_iff {α : Type u} {p : αBool} {l : List α} :
= [] ∀ (x : α), x lp x = true
@[simp]
theorem List.takeWhile_nil {α : Type u} {p : αBool} :
= []
theorem List.takeWhile_cons {α : Type u} {p : αBool} {l : List α} {x : α} :
List.takeWhile p (x :: l) = match p x with | true => x :: | false => []
theorem List.takeWhile_cons_of_pos {α : Type u} {p : αBool} {l : List α} {x : α} (h : p x = true) :
List.takeWhile p (x :: l) = x ::
theorem List.takeWhile_cons_of_neg {α : Type u} {p : αBool} {l : List α} {x : α} (h : ¬p x = true) :
List.takeWhile p (x :: l) = []
@[simp]
theorem List.takeWhile_eq_self_iff {α : Type u} {p : αBool} {l : List α} :
= l ∀ (x : α), x lp x = true
@[simp]
theorem List.takeWhile_eq_nil_iff {α : Type u} {p : αBool} {l : List α} :
= [] ∀ (hl : 0 < l.length), ¬p (l.nthLe 0 hl) = true
theorem List.mem_takeWhile_imp {α : Type u} {p : αBool} {l : List α} {x : α} (hx : x ) :
p x = true
theorem List.takeWhile_takeWhile {α : Type u} (p : αBool) (q : αBool) (l : List α) :
List.takeWhile p () = List.takeWhile (fun (a : α) => decide (p a = true q a = true)) l
theorem List.takeWhile_idem {α : Type u} {p : αBool} {l : List α} :

### erasep #

@[simp]
theorem List.length_eraseP_add_one {α : Type u} {p : αBool} {l : List α} {a : α} (al : a l) (pa : p a = true) :
().length + 1 = l.length

### erase #

@[simp]
theorem List.length_erase_add_one {α : Type u} [] {a : α} {l : List α} (h : a l) :
(l.erase a).length + 1 = l.length
theorem List.map_erase {α : Type u} {β : Type v} [] [] {f : αβ} (finj : ) {a : α} (l : List α) :
List.map f (l.erase a) = (List.map f l).erase (f a)
theorem List.map_foldl_erase {α : Type u} {β : Type v} [] [] {f : αβ} (finj : ) {l₁ : List α} {l₂ : List α} :
List.map f (List.foldl List.erase l₁ l₂) = List.foldl (fun (l : List β) (a : α) => l.erase (f a)) (List.map f l₁) l₂
theorem List.erase_get {ι : Type u_1} [] {l : List ι} (i : Fin l.length) :
(l.erase (l.get i)).Perm (l.eraseIdx i)
theorem List.length_eraseIdx_add_one {ι : Type u_1} {l : List ι} {i : } (h : i < l.length) :
(l.eraseIdx i).length + 1 = l.length

### diff #

@[simp]
theorem List.map_diff {α : Type u} {β : Type v} [] [] {f : αβ} (finj : ) {l₁ : List α} {l₂ : List α} :
List.map f (l₁.diff l₂) = (List.map f l₁).diff (List.map f l₂)
theorem List.erase_diff_erase_sublist_of_sublist {α : Type u} [] {a : α} {l₁ : List α} {l₂ : List α} :
l₁.Sublist l₂((l₂.erase a).diff (l₁.erase a)).Sublist (l₂.diff l₁)
theorem List.choose_spec {α : Type u} (p : αProp) [] (l : List α) (hp : ∃ (a : α), a l p a) :
List.choose p l hp l p (List.choose p l hp)
theorem List.choose_mem {α : Type u} (p : αProp) [] (l : List α) (hp : ∃ (a : α), a l p a) :
List.choose p l hp l
theorem List.choose_property {α : Type u} (p : αProp) [] (l : List α) (hp : ∃ (a : α), a l p a) :
p (List.choose p l hp)

### map₂Left' #

@[simp]
theorem List.map₂Left'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : αγ) (as : List α) :
List.map₂Left' f as [] = (List.map (fun (a : α) => f a none) as, [])

### map₂Right' #

@[simp]
theorem List.map₂Right'_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (bs : List β) :
List.map₂Right' f [] bs = (List.map (f none) bs, [])
@[simp]
theorem List.map₂Right'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (as : List α) :
List.map₂Right' f as [] = ([], as)
theorem List.map₂Right'_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (b : β) (bs : List β) :
List.map₂Right' f [] (b :: bs) = (f none b :: List.map (f none) bs, [])
@[simp]
theorem List.map₂Right'_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (a : α) (as : List α) (b : β) (bs : List β) :
List.map₂Right' f (a :: as) (b :: bs) = let r := List.map₂Right' f as bs; (f (some a) b :: r.1, r.2)

### zipLeft' #

@[simp]
theorem List.zipLeft'_nil_right {α : Type u} {β : Type v} (as : List α) :
as.zipLeft' [] = (List.map (fun (a : α) => (a, none)) as, [])
@[simp]
theorem List.zipLeft'_nil_left {α : Type u} {β : Type v} (bs : List β) :
[].zipLeft' bs = ([], bs)
theorem List.zipLeft'_cons_nil {α : Type u} {β : Type v} (a : α) (as : List α) :
(a :: as).zipLeft' [] = ((a, none) :: List.map (fun (a : α) => (a, none)) as, [])
@[simp]
theorem List.zipLeft'_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) :
(a :: as).zipLeft' (b :: bs) = let r := as.zipLeft' bs; ((a, some b) :: r.1, r.2)

### zipRight' #

@[simp]
theorem List.zipRight'_nil_left {α : Type u} {β : Type v} (bs : List β) :
[].zipRight' bs = (List.map (fun (b : β) => (none, b)) bs, [])
@[simp]
theorem List.zipRight'_nil_right {α : Type u} {β : Type v} (as : List α) :
as.zipRight' [] = ([], as)
theorem List.zipRight'_nil_cons {α : Type u} {β : Type v} (b : β) (bs : List β) :
[].zipRight' (b :: bs) = ((none, b) :: List.map (fun (b : β) => (none, b)) bs, [])
@[simp]
theorem List.zipRight'_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) :
(a :: as).zipRight' (b :: bs) = let r := as.zipRight' bs; ((some a, b) :: r.1, r.2)

### map₂Left #

@[simp]
theorem List.map₂Left_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : αγ) (as : List α) :
List.map₂Left f as [] = List.map (fun (a : α) => f a none) as
theorem List.map₂Left_eq_map₂Left' {α : Type u} {β : Type v} {γ : Type w} (f : αγ) (as : List α) (bs : List β) :
List.map₂Left f as bs = (List.map₂Left' f as bs).1
theorem List.map₂Left_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αγ) (as : List α) (bs : List β) :
as.length bs.lengthList.map₂Left f as bs = List.zipWith (fun (a : α) (b : β) => f a (some b)) as bs

### map₂Right #

@[simp]
theorem List.map₂Right_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (bs : List β) :
List.map₂Right f [] bs = List.map (f none) bs
@[simp]
theorem List.map₂Right_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (as : List α) :
List.map₂Right f as [] = []
theorem List.map₂Right_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (b : β) (bs : List β) :
List.map₂Right f [] (b :: bs) = f none b :: List.map (f none) bs
@[simp]
theorem List.map₂Right_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (a : α) (as : List α) (b : β) (bs : List β) :
List.map₂Right f (a :: as) (b :: bs) = f (some a) b :: List.map₂Right f as bs
theorem List.map₂Right_eq_map₂Right' {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (as : List α) (bs : List β) :
theorem List.map₂Right_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : βγ) (as : List α) (bs : List β) (h : bs.length as.length) :
List.map₂Right f as bs = List.zipWith (fun (a : α) (b : β) => f (some a) b) as bs

### zipLeft #

@[simp]
theorem List.zipLeft_nil_right {α : Type u} {β : Type v} (as : List α) :
as.zipLeft [] = List.map (fun (a : α) => (a, none)) as
@[simp]
theorem List.zipLeft_nil_left {α : Type u} {β : Type v} (bs : List β) :
[].zipLeft bs = []
theorem List.zipLeft_cons_nil {α : Type u} {β : Type v} (a : α) (as : List α) :
(a :: as).zipLeft [] = (a, none) :: List.map (fun (a : α) => (a, none)) as
@[simp]
theorem List.zipLeft_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) :
(a :: as).zipLeft (b :: bs) = (a, some b) :: as.zipLeft bs
theorem List.zipLeft_eq_zipLeft' {α : Type u} {β : Type v} (as : List α) (bs : List β) :
as.zipLeft bs = (as.zipLeft' bs).1

### zipRight #

@[simp]
theorem List.zipRight_nil_left {α : Type u} {β : Type v} (bs : List β) :
[].zipRight bs = List.map (fun (b : β) => (none, b)) bs
@[simp]
theorem List.zipRight_nil_right {α : Type u} {β : Type v} (as : List α) :
as.zipRight [] = []
theorem List.zipRight_nil_cons {α : Type u} {β : Type v} (b : β) (bs : List β) :
[].zipRight (b :: bs) = (none, b) :: List.map (fun (b : β) => (none, b)) bs
@[simp]
theorem List.zipRight_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) :
(a :: as).zipRight (b :: bs) = (some a, b) :: as.zipRight bs
theorem List.zipRight_eq_zipRight' {α : Type u} {β : Type v} (as : List α) (bs : List β) :
as.zipRight bs = (as.zipRight' bs).1

### Forall #

@[simp]
theorem List.forall_cons {α : Type u} (p : αProp) (x : α) (l : List α) :
List.Forall p (x :: l) p x
theorem List.forall_iff_forall_mem {α : Type u} {p : αProp} {l : List α} :
∀ (x : α), x lp x
theorem List.Forall.imp {α : Type u} {p : αProp} {q : αProp} (h : ∀ (x : α), p xq x) {l : List α} :
@[simp]
theorem List.forall_map_iff {α : Type u} {β : Type v} {l : List α} {p : βProp} (f : αβ) :
instance List.instDecidablePredForall {α : Type u} (p : αProp) [] :
Equations

### Miscellaneous lemmas #

theorem List.getLast_reverse {α : Type u} {l : List α} (hl : l.reverse []) (hl' : optParam (0 < l.length) ) :
l.reverse.getLast hl = l.get 0, hl'
@[simp]
theorem List.get_attach {α : Type u} (L : List α) (i : Fin L.attach.length) :
(L.attach.get i) = L.get i,
@[simp]
theorem List.mem_map_swap {α : Type u} {β : Type v} (x : α) (y : β) (xs : List (α × β)) :
(y, x) List.map Prod.swap xs (x, y) xs
theorem List.dropSlice_eq {α : Type u} (xs : List α) (n : ) (m : ) :
List.dropSlice n m xs = List.take n xs ++ List.drop (n + m) xs
theorem List.sizeOf_dropSlice_lt {α : Type u} [] (i : ) (j : ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) :
theorem List.disjoint_pmap {α : Type u} {β : Type v} {p : αProp} {f : (a : α) → p aβ} {s : List α} {t : List α} (hs : ∀ (a : α), a sp a) (ht : ∀ (a : α), a tp a) (hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha'a = a') (h : s.Disjoint t) :
(List.pmap f s hs).Disjoint (List.pmap f t ht)

The images of disjoint lists under a partially defined map are disjoint

theorem List.disjoint_map {α : Type u} {β : Type v} {f : αβ} {s : List α} {t : List α} (hf : ) (h : s.Disjoint t) :
(List.map f s).Disjoint (List.map f t)

The images of disjoint lists under an injective map are disjoint

theorem List.lookup_graph {α : Type u_2} {β : Type u_3} [BEq α] [] (f : αβ) {a : α} {as : List α} (h : a as) :
List.lookup a (List.map (fun (x : α) => (x, f x)) as) = some (f a)