data.list.basic

# Basic properties of lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def list.unique_of_is_empty {α : Type u} [is_empty α] :

There is only one list of an empty type

Equations
@[protected, instance]
def list.nil.is_left_id {α : Type u} :
@[protected, instance]
def list.nil.is_right_id {α : Type u} :
@[protected, instance]
theorem list.cons_ne_nil {α : Type u} (a : α) (l : list α) :
theorem list.cons_ne_self {α : Type u} (a : α) (l : list α) :
a :: l l
theorem list.head_eq_of_cons_eq {α : Type u} {h₁ h₂ : α} {t₁ t₂ : list α} :
h₁ :: t₁ = h₂ :: t₂ h₁ = h₂
theorem list.tail_eq_of_cons_eq {α : Type u} {h₁ h₂ : α} {t₁ t₂ : list α} :
h₁ :: t₁ = h₂ :: t₂ t₁ = t₂
@[simp]
theorem list.cons_injective {α : Type u} {a : α} :
theorem list.cons_inj {α : Type u} (a : α) {l l' : list α} :
a :: l = a :: l' l = l'
theorem list.cons_eq_cons {α : Type u} {a b : α} {l l' : list α} :
a :: l = b :: l' a = b l = l'
theorem list.singleton_injective {α : Type u} :
function.injective (λ (a : α), [a])
theorem list.singleton_inj {α : Type u} {a b : α} :
[a] = [b] a = b
theorem list.exists_cons_of_ne_nil {α : Type u} {l : list α} (h : l list.nil) :
(b : α) (L : list α), l = b :: L
theorem list.set_of_mem_cons {α : Type u} (l : list α) (a : α) :
{x : α | x a :: l} = {x : α | x l}

### mem #

theorem list.mem_singleton_self {α : Type u} (a : α) :
a [a]
theorem list.eq_of_mem_singleton {α : Type u} {a b : α} :
a [b] a = b
@[simp]
theorem list.mem_singleton {α : Type u} {a b : α} :
a [b] a = b
theorem list.mem_of_mem_cons_of_mem {α : Type u} {a b : α} {l : list α} :
a b :: l b l a l
theorem decidable.list.eq_or_ne_mem_of_mem {α : Type u} [decidable_eq α] {a b : α} {l : list α} (h : a b :: l) :
a = b a b a l
theorem list.eq_or_ne_mem_of_mem {α : Type u} {a b : α} {l : list α} :
a b :: l a = b a b a l
theorem list.not_mem_append {α : Type u} {a : α} {s t : list α} (h₁ : a s) (h₂ : a t) :
a s ++ t
theorem list.ne_nil_of_mem {α : Type u} {a : α} {l : list α} (h : a l) :
theorem list.mem_split {α : Type u} {a : α} {l : list α} (h : a l) :
(s t : list α), l = s ++ a :: t
theorem list.mem_of_ne_of_mem {α : Type u} {a y : α} {l : list α} (h₁ : a y) (h₂ : a y :: l) :
a l
theorem list.ne_of_not_mem_cons {α : Type u} {a b : α} {l : list α} :
a b :: l a b
theorem list.not_mem_of_not_mem_cons {α : Type u} {a b : α} {l : list α} :
a b :: l a l
theorem list.not_mem_cons_of_ne_of_not_mem {α : Type u} {a y : α} {l : list α} :
a y a l a y :: l
theorem list.ne_and_not_mem_of_not_mem_cons {α : Type u} {a y : α} {l : list α} :
a y :: l a y a l
@[simp]
theorem list.mem_map {α : Type u} {β : Type v} {f : α β} {b : β} {l : list α} :
b l (a : α), a l f a = b
theorem list.exists_of_mem_map {α : Type u} {β : Type v} {f : α β} {b : β} {l : list α} :
b l ( (a : α), a l f a = b)

Alias of the forward direction of `list.mem_map`.

theorem list.mem_map_of_mem {α : Type u} {β : Type v} (f : α β) {a : α} {l : list α} (h : a l) :
f a l
theorem list.mem_map_of_injective {α : Type u} {β : Type v} {f : α β} (H : function.injective f) {a : α} {l : list α} :
f a l a l
@[simp]
theorem function.involutive.exists_mem_and_apply_eq_iff {α : Type u} {f : α α} (hf : function.involutive f) (x : α) (l : list α) :
( (y : α), y l f y = x) f x l
theorem list.mem_map_of_involutive {α : Type u} {f : α α} (hf : function.involutive f) {a : α} {l : list α} :
a l f a l
theorem list.forall_mem_map_iff {α : Type u} {β : Type v} {f : α β} {l : list α} {P : β Prop} :
( (i : β), i l P i) (j : α), j l P (f j)
@[simp]
theorem list.map_eq_nil {α : Type u} {β : Type v} {f : α β} {l : list α} :
@[simp]
theorem list.mem_join {α : Type u} {a : α} {L : list (list α)} :
a L.join (l : list α), l L a l
theorem list.exists_of_mem_join {α : Type u} {a : α} {L : list (list α)} :
a L.join ( (l : list α), l L a l)
theorem list.mem_join_of_mem {α : Type u} {a : α} {L : list (list α)} {l : list α} (lL : l L) (al : a l) :
a L.join
@[simp]
theorem list.mem_bind {α : Type u} {β : Type v} {b : β} {l : list α} {f : α list β} :
b l.bind f (a : α) (H : a l), b f a
theorem list.exists_of_mem_bind {α : Type u} {β : Type v} {b : β} {l : list α} {f : α list β} :
b l.bind f ( (a : α) (H : a l), b f a)
theorem list.mem_bind_of_mem {α : Type u} {β : Type v} {b : β} {l : list α} {f : α list β} {a : α} (al : a l) (h : b f a) :
b l.bind f
theorem list.bind_map {α : Type u} {β : Type v} {γ : Type w} {g : α list β} {f : β γ} (l : list α) :
(l.bind g) = l.bind (λ (a : α), (g a))
theorem list.map_bind {α : Type u} {β : Type v} {γ : Type w} (g : β list γ) (f : α β) (l : list α) :
(list.map f l).bind g = l.bind (λ (a : α), g (f a))

### length #

theorem list.length_eq_zero {α : Type u} {l : list α} :
l.length = 0
@[simp]
theorem list.length_singleton {α : Type u} (a : α) :
[a].length = 1
theorem list.length_pos_of_mem {α : Type u} {a : α} {l : list α} :
a l 0 < l.length
theorem list.exists_mem_of_length_pos {α : Type u} {l : list α} :
0 < l.length ( (a : α), a l)
theorem list.length_pos_iff_exists_mem {α : Type u} {l : list α} :
0 < l.length (a : α), a l
theorem list.ne_nil_of_length_pos {α : Type u} {l : list α} :
0 < l.length
theorem list.length_pos_of_ne_nil {α : Type u} {l : list α} :
0 < l.length
theorem list.length_pos_iff_ne_nil {α : Type u} {l : list α} :
0 < l.length
theorem list.exists_mem_of_ne_nil {α : Type u} (l : list α) (h : l list.nil) :
(x : α), x l
theorem list.length_eq_one {α : Type u} {l : list α} :
l.length = 1 (a : α), l = [a]
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} :
@[simp]
theorem list.length_injective {α : Type u} [subsingleton α] :
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]
theorem list.sublist.length_le {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂ l₁.length l₂.length

Alias of `list.length_le_of_sublist`.

### set-theoretic notation of lists #

theorem list.empty_eq {α : Type u} :
theorem list.singleton_eq {α : Type u} (x : α) :
{x} = [x]
theorem list.insert_neg {α : Type u} [decidable_eq α] {x : α} {l : list α} (h : x l) :
= x :: l
theorem list.insert_pos {α : Type u} [decidable_eq α] {x : α} {l : list α} (h : x l) :
= l
theorem list.doubleton_eq {α : Type u} [decidable_eq α] {x y : α} (h : x y) :
{x, y} = [x, y]

### bounded quantifiers over lists #

theorem list.forall_mem_nil {α : Type u} (p : α Prop) (x : α) (H : x list.nil) :
p x
theorem list.forall_mem_cons {α : Type u} {p : α Prop} {a : α} {l : list α} :
( (x : α), x a :: l p x) p a (x : α), x l p x
theorem list.forall_mem_of_forall_mem_cons {α : Type u} {p : α Prop} {a : α} {l : list α} (h : (x : α), x a :: l p x) (x : α) (H : x l) :
p x
theorem list.forall_mem_singleton {α : Type u} {p : α Prop} {a : α} :
( (x : α), x [a] p x) p a
theorem list.forall_mem_append {α : Type u} {p : α Prop} {l₁ l₂ : list α} :
( (x : α), x l₁ ++ l₂ p x) ( (x : α), x l₁ p x) (x : α), x l₂ p x
theorem list.not_exists_mem_nil {α : Type u} (p : α Prop) :
¬ (x : α) (H : , p x
theorem list.exists_mem_cons_of {α : Type u} {p : α Prop} {a : α} (l : list α) (h : p a) :
(x : α) (H : x a :: l), p x
theorem list.exists_mem_cons_of_exists {α : Type u} {p : α Prop} {a : α} {l : list α} (h : (x : α) (H : x l), p x) :
(x : α) (H : x a :: l), p x
theorem list.or_exists_of_exists_mem_cons {α : Type u} {p : α Prop} {a : α} {l : list α} (h : (x : α) (H : x a :: l), p x) :
p a (x : α) (H : x l), p x
theorem list.exists_mem_cons_iff {α : Type u} (p : α Prop) (a : α) (l : list α) :
( (x : α) (H : x a :: l), p x) p a (x : α) (H : x l), p x

### list subset #

@[protected, instance]
theorem list.subset_def {α : Type u} {l₁ l₂ : list α} :
l₁ l₂ ⦃a : α⦄, a l₁ a l₂
theorem list.subset_append_of_subset_left {α : Type u} (l l₁ l₂ : list α) :
l l₁ l l₁ ++ l₂
theorem list.subset_append_of_subset_right {α : Type u} (l l₁ l₂ : list α) :
l l₂ l l₁ ++ l₂
@[simp]
theorem list.cons_subset {α : Type u} {a : α} {l m : list α} :
a :: l m a m l m
theorem list.cons_subset_of_subset_of_mem {α : Type u} {a : α} {l m : list α} (ainm : a m) (lsubm : l m) :
a :: l m
theorem list.append_subset_of_subset_of_subset {α : Type u} {l₁ l₂ l : list α} (l₁subl : l₁ l) (l₂subl : l₂ l) :
l₁ ++ l₂ l
@[simp]
theorem list.append_subset_iff {α : Type u} {l₁ l₂ l : list α} :
l₁ ++ l₂ l l₁ l l₂ l
theorem list.eq_nil_of_subset_nil {α : Type u} {l : list α} :
theorem list.eq_nil_iff_forall_not_mem {α : Type u} {l : list α} :
(a : α), a l
theorem list.map_subset {α : Type u} {β : Type v} {l₁ l₂ : list α} (f : α β) (H : l₁ l₂) :
l₁ l₂
theorem list.map_subset_iff {α : Type u} {β : Type v} {l₁ l₂ : list α} (f : α β) (h : function.injective f) :
l₁ l₂ l₁ l₂

### append #

theorem list.append_eq_has_append {α : Type u} {L₁ L₂ : list α} :
L₁.append L₂ = L₁ ++ L₂
@[simp]
theorem list.singleton_append {α : Type u} {x : α} {l : list α} :
[x] ++ l = x :: l
theorem list.append_ne_nil_of_ne_nil_left {α : Type u} (s t : list α) :
theorem list.append_ne_nil_of_ne_nil_right {α : Type u} (s t : list α) :
@[simp]
theorem list.append_eq_nil {α : Type u} {p q : list α} :
@[simp]
theorem list.nil_eq_append_iff {α : Type u} {a b : list α} :
theorem list.append_eq_cons_iff {α : Type u} {a b c : list α} {x : α} :
a ++ b = x :: c b = x :: c (a' : list α), a = x :: a' c = a' ++ b
theorem list.cons_eq_append_iff {α : Type u} {a b c : list α} {x : α} :
x :: c = a ++ b b = x :: c (a' : list α), a = x :: a' c = a' ++ b
theorem list.append_eq_append_iff {α : Type u} {a b c d : list α} :
a ++ b = c ++ d ( (a' : list α), c = a ++ a' b = a' ++ d) (c' : list α), a = c ++ c' d = c' ++ b
@[simp]
theorem list.take_append_drop {α : Type u} (n : ) (l : list α) :
l ++ l = l
theorem list.append_inj {α : Type u} {s₁ s₂ t₁ t₂ : list α} :
s₁ ++ t₁ = s₂ ++ t₂ s₁.length = s₂.length s₁ = s₂ t₁ = t₂
theorem list.append_inj_right {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.length = s₂.length) :
t₁ = t₂
theorem list.append_inj_left {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.length = s₂.length) :
s₁ = s₂
theorem list.append_inj' {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) :
s₁ = s₂ t₁ = t₂
theorem list.append_inj_right' {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) :
t₁ = t₂
theorem list.append_inj_left' {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) :
s₁ = s₂
theorem list.append_left_cancel {α : Type u} {s t₁ t₂ : list α} (h : s ++ t₁ = s ++ t₂) :
t₁ = t₂
theorem list.append_right_cancel {α : Type u} {s₁ s₂ t : list α} (h : s₁ ++ t = s₂ ++ t) :
s₁ = s₂
theorem list.append_right_injective {α : Type u} (s : list α) :
function.injective (λ (t : list α), s ++ t)
theorem list.append_right_inj {α : Type u} {t₁ t₂ : list α} (s : list α) :
s ++ t₁ = s ++ t₂ t₁ = t₂
theorem list.append_left_injective {α : Type u} (t : list α) :
function.injective (λ (s : list α), s ++ t)
theorem list.append_left_inj {α : Type u} {s₁ s₂ : list α} (t : list α) :
s₁ ++ t = s₂ ++ t s₁ = s₂
theorem list.map_eq_append_split {α : Type u} {β : Type v} {f : α β} {l : list α} {s₁ s₂ : list β} (h : l = s₁ ++ s₂) :
(l₁ l₂ : list α), l = l₁ ++ l₂ l₁ = s₁ l₂ = s₂

### replicate #

@[simp]
theorem list.replicate_zero {α : Type u} (a : α) :
@[simp]
theorem list.replicate_succ {α : Type u} (a : α) (n : ) :
list.replicate (n + 1) a = a ::
theorem list.replicate_one {α : Type u} (a : α) :
= [a]
@[simp]
theorem list.length_replicate {α : Type u} (n : ) (a : α) :
a).length = n
theorem list.mem_replicate {α : Type u} {a b : α} {n : } :
b n 0 b = a
theorem list.eq_of_mem_replicate {α : Type u} {a b : α} {n : } (h : b ) :
b = a
theorem list.eq_replicate_length {α : Type u} {a : α} {l : list α} :
l = (b : α), b l b = a
theorem list.eq_replicate_of_mem {α : Type u} {a : α} {l : list α} :
( (b : α), b l b = a) l =

Alias of the reverse direction of `list.eq_replicate_length`.

theorem list.eq_replicate {α : Type u} {a : α} {n : } {l : list α} :
l = l.length = n (b : α), b l b = 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 : α) :
a) = (f a)
@[simp]
theorem list.tail_replicate {α : Type u} (n : ) (a : α) :
a).tail = list.replicate (n - 1) a
@[simp]
theorem list.join_replicate_nil {α : Type u} (n : ) :
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 (λ (n : ), a)
@[simp]
theorem list.replicate_left_inj {α : Type u} {a : α} {n m : } :
= n = m

### pure #

@[simp]
theorem list.mem_pure {α : Type u_1} (x y : α) :
x = y

### bind #

@[simp]
theorem list.bind_eq_bind {α β : Type u_1} (f : α list β) (l : list α) :
l >>= f = l.bind f
theorem list.bind_append {α : Type u} {β : Type v} (f : α list β) (l₁ l₂ : list α) :
(l₁ ++ l₂).bind f = l₁.bind f ++ l₂.bind f
@[simp]
theorem list.bind_singleton {α : Type u} {β : Type v} (f : α list β) (x : α) :
[x].bind f = f x
@[simp]
theorem list.bind_singleton' {α : Type u} (l : list α) :
l.bind (λ (x : α), [x]) = l
theorem list.map_eq_bind {α : Type u_1} {β : Type u_2} (f : α β) (l : list α) :
l = l.bind (λ (x : α), [f x])
theorem list.bind_assoc {γ : Type w} {α : Type u_1} {β : Type u_2} (l : list α) (f : α list β) (g : β list γ) :
(l.bind f).bind g = l.bind (λ (x : α), (f x).bind g)

### concat #

theorem list.concat_nil {α : Type u} (a : α) :
= [a]
theorem list.concat_cons {α : Type u} (a b : α) (l : list α) :
(a :: l).concat b = a :: l.concat b
@[simp]
theorem list.concat_eq_append {α : Type u} (a : α) (l : list α) :
l.concat a = l ++ [a]
theorem list.init_eq_of_concat_eq {α : Type u} {a : α} {l₁ l₂ : list α} :
l₁.concat a = l₂.concat a l₁ = l₂
theorem list.last_eq_of_concat_eq {α : Type u} {a b : α} {l : list α} :
l.concat a = l.concat b a = b
theorem list.concat_ne_nil {α : Type u} (a : α) (l : list α) :
theorem list.concat_append {α : Type u} (a : α) (l₁ l₂ : list α) :
l₁.concat a ++ l₂ = l₁ ++ a :: l₂
theorem list.length_concat {α : Type u} (a : α) (l : list α) :
theorem list.append_concat {α : Type u} (a : α) (l₁ l₂ : list α) :
l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a

### reverse #

@[simp]
theorem list.reverse_nil {α : Type u} :
@[simp]
theorem list.reverse_cons {α : Type u} (a : α) (l : list α) :
(a :: l).reverse = l.reverse ++ [a]
theorem list.reverse_core_eq {α : Type u} (l₁ l₂ : list α) :
l₁.reverse_core l₂ = l₁.reverse ++ l₂
theorem list.reverse_cons' {α : Type u} (a : α) (l : list α) :
@[simp]
theorem list.reverse_singleton {α : Type u} (a : α) :
[a].reverse = [a]
@[simp]
theorem list.reverse_append {α : Type u} (s t : list α) :
theorem list.reverse_concat {α : Type u} (l : list α) (a : α) :
@[simp]
theorem list.reverse_reverse {α : Type u} (l : list α) :
@[simp]
theorem list.reverse_involutive {α : Type u} :
@[simp]
theorem list.reverse_injective {α : Type u} :
theorem list.reverse_surjective {α : Type u} :
theorem list.reverse_bijective {α : Type u} :
@[simp]
theorem list.reverse_inj {α : Type u} {l₁ l₂ : list α} :
l₁.reverse = l₂.reverse l₁ = l₂
theorem list.reverse_eq_iff {α : Type u} {l l' : list α} :
l.reverse = l' l = l'.reverse
@[simp]
theorem list.reverse_eq_nil {α : Type u} {l : list α} :
theorem list.concat_eq_reverse_cons {α : Type u} (a : α) (l : list α) :
@[simp]
theorem list.length_reverse {α : Type u} (l : list α) :
@[simp]
theorem list.map_reverse {α : Type u} {β : Type v} (f : α β) (l : list α) :
theorem list.map_reverse_core {α : Type u} {β : Type v} (f : α β) (l₁ l₂ : list α) :
(l₁.reverse_core l₂) = (list.map f l₁).reverse_core (list.map f l₂)
@[simp]
theorem list.mem_reverse {α : Type u} {a : α} {l : list α} :
a l.reverse a l
@[simp]
theorem list.reverse_replicate {α : Type u} (n : ) (a : α) :
a).reverse =

### empty #

theorem list.empty_iff_eq_nil {α : Type u} {l : list α} :

### init #

@[simp]
theorem list.length_init {α : Type u} (l : list α) :

### last #

@[simp]
theorem list.last_cons {α : Type u} {a : α} {l : list α} (h : l list.nil) :
(a :: l).last _ = l.last h
@[simp]
theorem list.last_append_singleton {α : Type u} {a : α} (l : list α) :
(l ++ [a]).last _ = a
theorem list.last_append {α : Type u} (l₁ l₂ : list α) (h : l₂ list.nil) :
(l₁ ++ l₂).last _ = l₂.last h
theorem list.last_concat {α : Type u} {a : α} (l : list α) :
(l.concat a).last _ = a
@[simp]
theorem list.last_singleton {α : Type u} (a : α) :
[a].last _ = a
@[simp]
theorem list.last_cons_cons {α : Type u} (a₁ a₂ : α) (l : list α) :
(a₁ :: a₂ :: l).last _ = (a₂ :: l).last _
theorem list.init_append_last {α : Type u} {l : list α} (h : l list.nil) :
l.init ++ [l.last h] = l
theorem list.last_congr {α : Type u} {l₁ l₂ : list α} (h₁ : l₁ list.nil) (h₂ : l₂ list.nil) (h₃ : l₁ = l₂) :
l₁.last h₁ = l₂.last h₂
theorem list.last_mem {α : Type u} {l : list α} (h : l list.nil) :
l.last h l
theorem list.last_replicate_succ {α : Type u} (m : ) (a : α) :
(list.replicate (m + 1) a).last _ = a

### last' #

@[simp]
theorem list.last'_is_none {α : Type u} {l : list α} :
@[simp]
theorem list.last'_is_some {α : Type u} {l : list α} :
theorem list.mem_last'_eq_last {α : Type u} {l : list α} {x : α} :
x l.last' ( (h : , x = l.last h)
theorem list.last'_eq_last_of_ne_nil {α : Type u} {l : list α} (h : l list.nil) :
theorem list.mem_last'_cons {α : Type u} {x y : α} {l : list α} (h : x l.last') :
x (y :: l).last'
theorem list.mem_of_mem_last' {α : Type u} {l : list α} {a : α} (ha : a l.last') :
a l
theorem list.init_append_last' {α : Type u} {l : list α} (a : α) (H : a l.last') :
l.init ++ [a] = l
theorem list.ilast_eq_last' {α : Type u} [inhabited α] (l : list α) :
@[simp]
theorem list.last'_append_cons {α : Type u} (l₁ : list α) (a : α) (l₂ : list α) :
(l₁ ++ a :: l₂).last' = (a :: l₂).last'
@[simp]
theorem list.last'_cons_cons {α : Type u} (x y : α) (l : list α) :
(x :: y :: l).last' = (y :: l).last'
theorem list.last'_append_of_ne_nil {α : Type u} (l₁ : list α) {l₂ : list α} (hl₂ : l₂ list.nil) :
(l₁ ++ l₂).last' = l₂.last'
theorem list.last'_append {α : Type u} {l₁ l₂ : list α} {x : α} (h : x l₂.last') :
x (l₁ ++ l₂).last'

theorem list.head_eq_head' {α : Type u} [inhabited α] (l : list α) :
theorem list.surjective_head {α : Type u} [inhabited α] :
theorem list.surjective_head' {α : Type u} :
theorem list.surjective_tail {α : 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} [inhabited α] (a : α) (l : list α) :
@[simp]
theorem list.tail_nil {α : Type u} :
@[simp]
theorem list.tail_cons {α : Type u} (a : α) (l : list α) :
(a :: l).tail = l
@[simp]
theorem list.head_append {α : Type u} [inhabited α] (t : list α) {s : list α} (h : s list.nil) :
theorem list.head'_append {α : Type u} {s t : list α} {x : α} (h : x s.head') :
theorem list.head'_append_of_ne_nil {α : Type u} (l₁ : list α) {l₂ : list α} (hl₁ : l₁ list.nil) :
theorem list.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : list α} (h : l list.nil) :
(l ++ [a]).tail = l.tail ++ [a]
theorem list.cons_head'_tail {α : Type u} {l : list α} {a : α} (h : a l.head') :
a :: l.tail = l
theorem list.head_mem_head' {α : Type u} [inhabited α] {l : list α} (h : l list.nil) :
theorem list.cons_head_tail {α : Type u} [inhabited α] {l : list α} (h : l list.nil) :
theorem list.head_mem_self {α : Type u} [inhabited α] {l : list α} (h : l list.nil) :
@[simp]
theorem list.head'_map {α : Type u} {β : Type v} (f : α β) (l : list α) :
theorem list.tail_append_of_ne_nil {α : Type u} (l l' : list α) (h : l list.nil) :
(l ++ l').tail = l.tail ++ l'
@[simp]
theorem list.nth_le_tail {α : Type u} (l : list α) (i : ) (h : i < l.tail.length) (h' : i + 1 < l.length := _) :
l.tail.nth_le i h = l.nth_le (i + 1) h'
theorem list.nth_le_cons_aux {α : Type u} {l : list α} {a : α} {n : } (hn : n 0) (h : n < (a :: l).length) :
n - 1 < l.length
theorem list.nth_le_cons {α : Type u} {l : list α} {a : α} {n : } (hl : n < (a :: l).length) :
(a :: l).nth_le n hl = dite (n = 0) (λ (hn : n = 0), a) (λ (hn : ¬n = 0), l.nth_le (n - 1) _)
@[simp]
theorem list.modify_head_modify_head {α : Type u} (l : list α) (f g : α α) :
l) = list.modify_head (g f) l

### Induction from the right #

def list.reverse_rec_on {α : Type u} {C : list α Sort u_1} (l : list α) (H0 : C list.nil) (H1 : Π (l : list α) (a : α), C l C (l ++ [a])) :
C 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
def list.bidirectional_rec {α : Type u} {C : list α Sort u_1} (H0 : C list.nil) (H1 : Π (a : α), C [a]) (Hn : Π (a : α) (l : list α) (b : α), C l C (a :: (l ++ [b]))) (l : list α) :
C 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
def list.bidirectional_rec_on {α : Type u} {C : list α Sort u_1} (l : list α) (H0 : C list.nil) (H1 : Π (a : α), C [a]) (Hn : Π (a : α) (l : list α) (b : α), C l C (a :: (l ++ [b]))) :
C l

Like `bidirectional_rec`, but with the list parameter placed first.

Equations
• H1 Hn = Hn l

### sublists #

@[simp]
theorem list.nil_sublist {α : Type u} (l : list α) :
@[simp, refl]
theorem list.sublist.refl {α : Type u} (l : list α) :
l <+ l
@[trans]
theorem list.sublist.trans {α : Type u} {l₁ l₂ l₃ : list α} (h₁ : l₁ <+ l₂) (h₂ : l₂ <+ l₃) :
l₁ <+ l₃
@[simp]
theorem list.sublist_cons {α : Type u} (a : α) (l : list α) :
l <+ a :: l
theorem list.sublist_of_cons_sublist {α : Type u} {a : α} {l₁ l₂ : list α} :
a :: l₁ <+ l₂ l₁ <+ l₂
theorem list.sublist.cons_cons {α : Type u} {l₁ l₂ : list α} (a : α) (s : l₁ <+ l₂) :
a :: l₁ <+ a :: l₂
@[simp]
theorem list.sublist_append_left {α : Type u} (l₁ l₂ : list α) :
l₁ <+ l₁ ++ l₂
@[simp]
theorem list.sublist_append_right {α : Type u} (l₁ l₂ : list α) :
l₂ <+ l₁ ++ l₂
theorem list.sublist_cons_of_sublist {α : Type u} (a : α) {l₁ l₂ : list α} :
l₁ <+ l₂ l₁ <+ a :: l₂
theorem list.sublist_append_of_sublist_left {α : Type u} {l l₁ l₂ : list α} (s : l <+ l₁) :
l <+ l₁ ++ l₂
theorem list.sublist_append_of_sublist_right {α : Type u} {l l₁ l₂ : list α} (s : l <+ l₂) :
l <+ l₁ ++ l₂
theorem list.sublist_of_cons_sublist_cons {α : Type u} {l₁ l₂ : list α} {a : α} :
a :: l₁ <+ a :: l₂ l₁ <+ l₂
theorem list.cons_sublist_cons_iff {α : Type u} {l₁ l₂ : list α} {a : α} :
a :: l₁ <+ a :: l₂ l₁ <+ l₂
@[simp]
theorem list.append_sublist_append_left {α : Type u} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ <+ l ++ l₂ l₁ <+ l₂
theorem list.sublist.append_right {α : Type u} {l₁ l₂ : list α} (h : l₁ <+ l₂) (l : list α) :
l₁ ++ l <+ l₂ ++ l
theorem list.sublist_or_mem_of_sublist {α : Type u} {l l₁ l₂ : list α} {a : α} (h : l <+ l₁ ++ a :: l₂) :
l <+ l₁ ++ l₂ a l
theorem list.sublist.reverse {α : Type u} {l₁ l₂ : list α} (h : l₁ <+ l₂) :
l₁.reverse <+ l₂.reverse
@[simp]
theorem list.reverse_sublist_iff {α : Type u} {l₁ l₂ : list α} :
l₁.reverse <+ l₂.reverse l₁ <+ l₂
@[simp]
theorem list.append_sublist_append_right {α : Type u} {l₁ l₂ : list α} (l : list α) :
l₁ ++ l <+ l₂ ++ l l₁ <+ l₂
theorem list.sublist.append {α : Type u} {l₁ l₂ r₁ r₂ : list α} (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) :
l₁ ++ r₁ <+ l₂ ++ r₂
theorem list.sublist.subset {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂ l₁ l₂
@[simp]
theorem list.singleton_sublist {α : Type u} {a : α} {l : list α} :
[a] <+ l a l
theorem list.eq_nil_of_sublist_nil {α : Type u} {l : list α} (s : l <+ list.nil) :
@[simp]
theorem list.sublist_nil_iff_eq_nil {α : Type u} {l : list α} :
@[simp]
theorem list.replicate_sublist_replicate {α : Type u} (a : α) {m n : } :
<+ m n
theorem list.sublist_replicate_iff {α : Type u} {l : list α} {a : α} {n : } :
l <+ (k : ) (H : k n), l =
theorem list.sublist.eq_of_length {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂ l₁.length = l₂.length l₁ = l₂
theorem list.sublist.eq_of_length_le {α : Type u} {l₁ l₂ : list α} (s : l₁ <+ l₂) (h : l₂.length l₁.length) :
l₁ = l₂
theorem list.sublist.antisymm {α : Type u} {l₁ l₂ : list α} (s₁ : l₁ <+ l₂) (s₂ : l₂ <+ l₁) :
l₁ = l₂
@[protected, instance]
def list.decidable_sublist {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <+ l₂)
Equations

### index_of #

@[simp]
theorem list.index_of_nil {α : Type u} [decidable_eq α] (a : α) :
theorem list.index_of_cons {α : Type u} [decidable_eq α] (a b : α) (l : list α) :
(b :: l) = ite (a = b) 0 l).succ
theorem list.index_of_cons_eq {α : Type u} [decidable_eq α] {a b : α} (l : list α) :
a = b (b :: l) = 0
@[simp]
theorem list.index_of_cons_self {α : Type u} [decidable_eq α] (a : α) (l : list α) :
(a :: l) = 0
@[simp]
theorem list.index_of_cons_ne {α : Type u} [decidable_eq α] {a b : α} (l : list α) :
a b (b :: l) = l).succ
theorem list.index_of_eq_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :
= l.length a l
@[simp]
theorem list.index_of_of_not_mem {α : Type u} [decidable_eq α] {l : list α} {a : α} :
a l = l.length
theorem list.index_of_le_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :
theorem list.index_of_lt_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :
< l.length a l
theorem list.index_of_append_of_mem {α : Type u} {l₁ l₂ : list α} [decidable_eq α] {a : α} (h : a l₁) :
(l₁ ++ l₂) = l₁
theorem list.index_of_append_of_not_mem {α : Type u} {l₁ l₂ : list α} [decidable_eq α] {a : α} (h : a l₁) :
(l₁ ++ l₂) = l₁.length + l₂

### nth element #

theorem list.nth_le_of_mem {α : Type u} {a : α} {l : list α} :
a l ( (n : ) (h : n < l.length), l.nth_le n h = a)
theorem list.nth_le_nth {α : Type u} {l : list α} {n : } (h : n < l.length) :
l.nth n = option.some (l.nth_le n h)
theorem list.nth_len_le {α : Type u} {l : list α} {n : } :
@[simp]
theorem list.nth_length {α : Type u} (l : list α) :
theorem list.nth_eq_some {α : Type u} {l : list α} {n : } {a : α} :
l.nth n = (h : n < l.length), l.nth_le n h = a
@[simp]
theorem list.nth_eq_none_iff {α : Type u} {l : list α} {n : } :
theorem list.nth_of_mem {α : Type u} {a : α} {l : list α} (h : a l) :
(n : ), l.nth n =
theorem list.nth_le_mem {α : Type u} (l : list α) (n : ) (h : n < l.length) :
l.nth_le n h l
theorem list.nth_mem {α : Type u} {l : list α} {n : } {a : α} (e : l.nth n = ) :
a l
theorem list.mem_iff_nth_le {α : Type u} {a : α} {l : list α} :
a l (n : ) (h : n < l.length), l.nth_le n h = a
theorem list.mem_iff_nth {α : Type u} {a : α} {l : list α} :
a l (n : ), l.nth n =
theorem list.nth_zero {α : Type u} (l : list α) :
theorem list.nth_injective {α : Type u} {xs : list α} {i j : } (h₀ : i < xs.length) (h₁ : xs.nodup) (h₂ : xs.nth i = xs.nth j) :
i = j
@[simp]
theorem list.nth_map {α : Type u} {β : Type v} (f : α β) (l : list α) (n : ) :
(list.map f l).nth n = (l.nth n)
theorem list.nth_le_map {α : Type u} {β : Type v} (f : α β) {l : list α} {n : } (H1 : n < (list.map f l).length) (H2 : n < l.length) :
(list.map f l).nth_le n H1 = f (l.nth_le n H2)
theorem list.nth_le_map_rev {α : Type u} {β : Type v} (f : α β) {l : list α} {n : } (H : n < l.length) :
f (l.nth_le n H) = (list.map f l).nth_le n _

A version of `nth_le_map` that can be used for rewriting.

@[simp]
theorem list.nth_le_map' {α : Type u} {β : Type v} (f : α β) {l : list α} {n : } (H : n < (list.map f l).length) :
(list.map f l).nth_le n H = f (l.nth_le n _)
theorem list.nth_le_of_eq {α : Type u} {L L' : list α} (h : L = L') {i : } (hi : i < L.length) :
L.nth_le i hi = L'.nth_le i _

If one has `nth_le L i hi` in a formula and `h : L = L'`, one can not `rw h` in the formula as `hi` gives `i < L.length` and not `i < L'.length`. The lemma `nth_le_of_eq` can be used to make such a rewrite, with `rw (nth_le_of_eq h)`.

@[simp]
theorem list.nth_le_singleton {α : Type u} (a : α) {n : } (hn : n < 1) :
[a].nth_le n hn = a
theorem list.nth_le_zero {α : Type u} [inhabited α] {L : list α} (h : 0 < L.length) :
theorem list.nth_le_append {α : Type u} {l₁ l₂ : list α} {n : } (hn₁ : n < (l₁ ++ l₂).length) (hn₂ : n < l₁.length) :
(l₁ ++ l₂).nth_le n hn₁ = l₁.nth_le n hn₂
theorem list.nth_le_append_right_aux {α : Type u} {l₁ l₂ : list α} {n : } (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
n - l₁.length < l₂.length
theorem list.nth_le_append_right {α : Type u} {l₁ l₂ : list α} {n : } (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
(l₁ ++ l₂).nth_le n h₂ = l₂.nth_le (n - l₁.length) _
@[simp]
theorem list.nth_le_replicate {α : Type u} (a : α) {n m : } (h : m < a).length) :
a).nth_le m h = a
theorem list.nth_append {α : Type u} {l₁ l₂ : list α} {n : } (hn : n < l₁.length) :
(l₁ ++ l₂).nth n = l₁.nth n
theorem list.nth_append_right {α : Type u} {l₁ l₂ : list α} {n : } (hn : l₁.length n) :
(l₁ ++ l₂).nth n = l₂.nth (n - l₁.length)
theorem list.last_eq_nth_le {α : Type u} (l : list α) (h : l list.nil) :
l.last h = l.nth_le (l.length - 1) _
theorem list.nth_le_length_sub_one {α : Type u} {l : list α} (h : l.length - 1 < l.length) :
l.nth_le (l.length - 1) h = l.last _
@[simp]
theorem list.nth_concat_length {α : Type u} (l : list α) (a : α) :
(l ++ [a]).nth l.length =
theorem list.nth_le_cons_length {α : Type u} (x : α) (xs : list α) (n : ) (h : n = xs.length) :
(x :: xs).nth_le n _ = (x :: xs).last _
theorem list.take_one_drop_eq_of_lt_length {α : Type u} {l : list α} {n : } (h : n < l.length) :
l) = [l.nth_le n h]
@[ext]
theorem list.ext {α : Type u} {l₁ l₂ : list α} :
( (n : ), l₁.nth n = l₂.nth n) l₁ = l₂
theorem list.ext_le {α : Type u} {l₁ l₂ : list α} (hl : l₁.length = l₂.length) (h : (n : ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.nth_le n h₁ = l₂.nth_le n h₂) :
l₁ = l₂
@[simp]
theorem list.index_of_nth_le {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : < l.length) :
l.nth_le l) h = a
@[simp]
theorem list.index_of_nth {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l) :
l.nth l) =
theorem list.nth_le_reverse_aux1 {α : Type u} (l r : list α) (i : ) (h1 : i + l.length < (l.reverse_core r).length) (h2 : i < r.length) :
(l.reverse_core r).nth_le (i + l.length) h1 = r.nth_le i h2
theorem list.index_of_inj {α : Type u} [decidable_eq α] {l : list α} {x y : α} (hx : x l) (hy : y l) :
= x = y
theorem list.nth_le_reverse_aux2 {α : Type u} (l r : list α) (i : ) (h1 : l.length - 1 - i < (l.reverse_core r).length) (h2 : i < l.length) :
(l.reverse_core r).nth_le (l.length - 1 - i) h1 = l.nth_le i h2
@[simp]
theorem list.nth_le_reverse {α : Type u} (l : list α) (i : ) (h1 : l.length - 1 - i < l.reverse.length) (h2 : i < l.length) :
l.reverse.nth_le (l.length - 1 - i) h1 = l.nth_le i h2
theorem list.nth_le_reverse' {α : Type u} (l : list α) (n : ) (hn : n < l.reverse.length) (hn' : l.length - 1 - n < l.length) :
l.reverse.nth_le n hn = l.nth_le (l.length - 1 - n) hn'
theorem list.eq_cons_of_length_one {α : Type u} {l : list α} (h : l.length = 1) :
l = [l.nth_le 0 _]
theorem list.nth_le_eq_iff {α : Type u} {l : list α} {n : } {x : α} {h : n < l.length} :
l.nth_le n h = x l.nth n =
theorem list.some_nth_le_eq {α : Type u} {l : list α} {n : } {h : n < l.length} :
option.some (l.nth_le n h) = l.nth n
theorem list.modify_nth_tail_modify_nth_tail {α : Type u} {f g : list α list α} (m n : ) (l : list α) :
(m + n) l) = list.modify_nth_tail (λ (l : list α), (f l)) n l
theorem list.modify_nth_tail_modify_nth_tail_le {α : Type u} {f g : list α list α} (m n : ) (l : list α) (h : n m) :
l) = list.modify_nth_tail (λ (l : list α), (m - n) (f l)) n l
theorem list.modify_nth_tail_modify_nth_tail_same {α : Type u} {f g : list α list α} (n : ) (l : list α) :
l) = list.modify_nth_tail (g f) n l
theorem list.modify_nth_tail_id {α : Type u} (n : ) (l : list α) :
= l
theorem list.remove_nth_eq_nth_tail {α : Type u} (n : ) (l : list α) :
theorem list.update_nth_eq_modify_nth {α : Type u} (a : α) (n : ) (l : list α) :
l.update_nth n a = list.modify_nth (λ (_x : α), a) n l
theorem list.modify_nth_eq_update_nth {α : Type u} (f : α α) (n : ) (l : list α) :
l = ((λ (a : α), l.update_nth n (f a)) <\$> l.nth n).get_or_else l
theorem list.nth_modify_nth {α : Type u} (f : α α) (n : ) (l : list α) (m : ) :
n l).nth m = (λ (a : α), ite (n = m) (f a) a) <\$> l.nth m
theorem list.modify_nth_tail_length {α : Type u} (f : list α list α) (H : (l : list α), (f l).length = l.length) (n : ) (l : list α) :
@[simp]
theorem list.modify_nth_length {α : Type u} (f : α α) (n : ) (l : list α) :
n l).length = l.length
@[simp]
theorem list.update_nth_length {α : Type u} (l : list α) (n : ) (a : α) :
@[simp]
theorem list.nth_modify_nth_eq {α : Type u} (f : α α) (n : ) (l : list α) :
n l).nth n = f <\$> l.nth n
@[simp]
theorem list.nth_modify_nth_ne {α : Type u} (f : α α) {m n : } (l : list α) (h : m n) :
m l).nth n = l.nth n
theorem list.nth_update_nth_eq {α : Type u} (a : α) (n : ) (l : list α) :
(l.update_nth n a).nth n = (λ (_x : α), a) <\$> l.nth n
theorem list.nth_update_nth_of_lt {α : Type u} (a : α) {n : } {l : list α} (h : n < l.length) :
(l.update_nth n a).nth n =
theorem list.nth_update_nth_ne {α : Type u} (a : α) {m n : } (l : list α) (h : m n) :
(l.update_nth m a).nth n = l.nth n
@[simp]
theorem list.update_nth_nil {α : Type u} (n : ) (a : α) :
@[simp]
theorem list.update_nth_succ {α : Type u} (x : α) (xs : list α) (n : ) (a : α) :
(x :: xs).update_nth n.succ a = x :: xs.update_nth n a
theorem list.update_nth_comm {α : Type u} (a b : α) {n m : } (l : list α) (h : n m) :
(l.update_nth n a).update_nth m b = (l.update_nth m b).update_nth n a
@[simp]
theorem list.nth_le_update_nth_eq {α : Type u} (l : list α) (i : ) (a : α) (h : i < (l.update_nth i a).length) :
(l.update_nth i a).nth_le i h = a
@[simp]
theorem list.nth_le_update_nth_of_ne {α : Type u} {l : list α} {i j : } (h : i j) (a : α) (hj : j < (l.update_nth i a).length) :
(l.update_nth i a).nth_le j hj = l.nth_le j _
theorem list.mem_or_eq_of_mem_update_nth {α : Type u} {l : list α} {n : } {a b : α} (h : a l.update_nth n b) :
a l a = b
@[simp]
theorem list.insert_nth_zero {α : Type u} (s : list α) (x : α) :
s = x :: s
@[simp]
theorem list.insert_nth_succ_nil {α : Type u} (n : ) (a : α) :
@[simp]
theorem list.insert_nth_succ_cons {α : Type u} (s : list α) (hd x : α) (n : ) :
list.insert_nth (n + 1) x (hd :: s) = hd :: s
theorem list.length_insert_nth {α : Type u} {a : α} (n : ) (as : list α) :
n as.length a as).length = as.length + 1
theorem list.remove_nth_insert_nth {α : Type u} {a : α} (n : ) (l : list α) :
a l).remove_nth n = l
theorem list.insert_nth_remove_nth_of_ge {α : Type u} {a : α} (n m : ) (as : list α) :
n < as.length n m (as.remove_nth n) = (list.insert_nth (m + 1) a as).remove_nth n
theorem list.insert_nth_remove_nth_of_le {α : Type u} {a : α} (n m : ) (as : list α) :
n < as.length m n (as.remove_nth n) = a as).remove_nth (n + 1)
theorem list.insert_nth_comm {α : Type u} (a b : α) (i j : ) (l : list α) (h : i j) (hj : j l.length) :
list.insert_nth (j + 1) b a l) = b l)
theorem list.mem_insert_nth {α : Type u} {a b : α} {n : } {l : list α} (hi : n l.length) :
a l a = b a l
theorem list.insert_nth_of_length_lt {α : Type u} (l : list α) (x : α) (n : ) (h : l.length < n) :
l = l
@[simp]
theorem list.insert_nth_length_self {α : Type u} (l : list α) (x : α) :
l = l ++ [x]
theorem list.length_le_length_insert_nth {α : Type u} (l : list α) (x : α) (n : ) :
theorem list.length_insert_nth_le_succ {α : Type u} (l : list α) (x : α) (n : ) :
x l).length l.length + 1
theorem list.nth_le_insert_nth_of_lt {α : Type u} (l : list α) (x : α) (n k : ) (hn : k < n) (hk : k < l.length) (hk' : k < x l).length := _) :
x l).nth_le k hk' = l.nth_le k hk
@[simp]
theorem list.nth_le_insert_nth_self {α : Type u} (l : list α) (x : α) (n : ) (hn : n l.length) (hn' : n < x l).length := _) :
x l).nth_le n hn' = x
theorem list.nth_le_insert_nth_add_succ {α : Type u} (l : list α) (x : α) (n k : ) (hk' : n + k < l.length) (hk : n + k + 1 < x l).length := _) :
x l).nth_le (n + k + 1) hk = l.nth_le (n + k) hk'
theorem list.insert_nth_injective {α : Type u} (n : ) (x : α) :

### map #

@[simp]
theorem list.map_nil {α : Type u} {β : Type v} (f : α β) :
theorem list.map_eq_foldr {α : Type u} {β : Type v} (f : α β) (l : list α) :
l = list.foldr (λ (a : α) (bs : list β), f a :: bs) list.nil l
theorem list.map_congr {α : Type u} {β : Type v} {f g : α β} {l : list α} :
( (x : α), x l f x = g x) l = l
theorem list.map_eq_map_iff {α : Type u} {β : Type v} {f g : α β} {l : list α} :
l = l (x : α), x l f x = g x
theorem list.map_concat {α : Type u} {β : Type v} (f : α β) (a : α) (l : list α) :
(l.concat a) = (list.map f l).concat (f a)
@[simp]
theorem list.map_id'' {α : Type u} (l : list α) :
list.map (λ (x : α), x) l = l
theorem list.map_id' {α : Type u} {f : α α} (h : (x : α), f x = x) (l : list α) :
l = l
theorem list.eq_nil_of_map_eq_nil {α : Type u} {β : Type v} {f : α β} {l : list α} (h : l = list.nil) :
@[simp]
theorem list.map_join {α : Type u} {β : Type v} (f : α β) (L : list (list α)) :
theorem list.bind_ret_eq_map {α : Type u} {β : Type v} (f : α β) (l : list α) :
l.bind (list.ret f) = l
theorem list.bind_congr {α : Type u} {β : Type v} {l : list α} {f g : α list β} (h : (x : α), x l f x = g x) :
l.bind f = l.bind g
@[simp]
theorem list.map_eq_map {α β : Type u_1} (f : α β) (l : list α) :
f <\$> l = l
@[simp]
theorem list.map_tail {α : Type u} {β : Type v} (f : α β) (l : list α) :
l.tail = (list.map f l).tail
@[simp]
theorem list.map_injective_iff {α : Type u} {β : Type v} {f : α β} :
theorem list.comp_map {α : Type u} {β : Type v} {γ : Type w} (h : β γ) (g : α β) (l : list α) :
list.map (h g) l = (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 list.map_filter_eq_foldr {α : Type u} {β : Type v} (f : α β) (p : α Prop) (as : list α) :
as) = list.foldr (λ (a : α) (bs : list β), ite (p a) (f a :: bs) bs) list.nil as
theorem list.last_map {α : Type u} {β : Type v} (f : α β) {l : list α} (hl : l list.nil) :
(list.map f l).last _ = f (l.last hl)
theorem list.map_eq_replicate_iff {α : Type u} {β : Type v} {l : list α} {f : α β} {b : β} :
l = (x : α), x l f x = b
@[simp]
theorem list.map_const {α : Type u} {β : Type v} (l : list α) (b : β) :
list.map b) l =
theorem list.map_const' {α : Type u} {β : Type v} (l : list α) (b : β) :
list.map (λ (_x : α), b) l =
theorem list.eq_of_mem_map_const {α : Type u} {β : Type v} {b₁ b₂ : β} {l : list α} (h : b₁ list.map b₂) l) :
b₁ = b₂

### map₂ #

theorem list.nil_map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) (l : list β) :
theorem list.map₂_nil {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) (l : list α) :
@[simp]
theorem list.map₂_flip {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) (as : list α) (bs : list β) :
list.map₂ (flip f) bs as = as bs

### take, drop #

@[simp]
theorem list.take_zero {α : Type u} (l : list α) :
@[simp]
theorem list.take_nil {α : Type u} (n : ) :
theorem list.take_cons {α : Type u} (n : ) (a : α) (l : list α) :
(a :: l) = a :: l
@[simp]
theorem list.take_length {α : Type u} (l : list α) :
l = l
theorem list.take_all_of_le {α : Type u} {n : } {l : list α} :
l.length n l = l
@[simp]
theorem list.take_left {α : Type u} (l₁ l₂ : list α) :
(l₁ ++ l₂) = l₁
theorem list.take_left' {α : Type u} {l₁ l₂ : list α} {n : } (h : l₁.length = n) :
(l₁ ++ l₂) = l₁
theorem list.take_take {α : Type u} (n m : ) (l : list α) :
l) = l
theorem list.take_replicate {α : Type u} (a : α) (n m : ) :
a) = a
theorem list.map_take {α : Type u_1} {β : Type u_2} (f : α β) (L : list α) (i : ) :
L) = (list.map f L)
theorem list.take_append_eq_append_take {α : Type u} {l₁ l₂ : list α} {n : } :
(l₁ ++ l₂) = l₁ ++ list.take (n - l₁.length) l₂

Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements of `l₁` to the first `n - l₁.length` elements of `l₂`.

theorem list.take_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : } (h : n l₁.length) :
(l₁ ++ l₂) = l₁
theorem list.take_append {α : Type u} {l₁ l₂ : list α} (i : ) :
list.take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ l₂

Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first `i` elements of `l₂` to `l₁`.

theorem list.nth_le_take {α : Type u} (L : list α) {i j : } (hi : i < L.length) (hj : i < j) :
L.nth_le i hi = L).nth_le i _

The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the big list to the small list.

theorem list.nth_le_take' {α : Type u} (L : list α) {i j : } (hi : i < L).length) :
L).nth_le i hi = L.nth_le i _

The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the small list to the big list.

theorem list.nth_take {α : Type u} {l : list α} {n m : } (h : m < n) :
l).nth m = l.nth m
@[simp]
theorem list.nth_take_of_succ {α : Type u} {l : list α} {n : } :
(list.take (n + 1) l).nth n = l.nth n
theorem list.take_succ {α : Type u} {l : list α} {n : } :
list.take (n + 1) l = l ++ (l.nth n).to_list
@[simp]
theorem list.take_eq_nil_iff {α : Type u} {l : list α} {k : } :
k = 0
theorem list.take_eq_take {α : Type u} {l : list α} {m n : } :
l = l
theorem list.take_add {α : Type u} (l : list α) (m n : ) :
list.take (m + n) l = l ++ l)
theorem list.init_eq_take {α : Type u} (l : list α) :
l.init = l
theorem list.init_take {α : Type u} {n : } {l : list α} (h : n < l.length) :
l).init = l
@[simp]
theorem list.init_cons_of_ne_nil {α : Type u_1} {x : α} {l : list α} (h : l list.nil) :
(x :: l).init = x :: l.init
@[simp]
theorem list.init_append_of_ne_nil {α : Type u_1} {l : list α} (l' : list α) (h : l list.nil) :
(l' ++ l).init = l' ++ l.init
@[simp]
theorem list.drop_eq_nil_of_le {α : Type u} {l : list α} {k : } (h : l.length k) :
theorem list.drop_eq_nil_iff_le {α : Type u} {l : list α} {k : } :
theorem list.tail_drop {α : Type u} (l : list α) (n : ) :
l).tail = list.drop (n + 1) l
theorem list.cons_nth_le_drop_succ {α : Type u} {l : list α} {n : } (hn : n < l.length) :
l.nth_le n hn :: list.drop (n + 1) l = l
theorem list.drop_nil {α : Type u} (n : ) :
@[simp]
theorem list.drop_one {α : Type u} (l : list α) :
l = l.tail
theorem list.drop_add {α : Type u} (m n : ) (l : list α) :
list.drop (m + n) l = l)
@[simp]
theorem list.drop_left {α : Type u} (l₁ l₂ : list α) :
(l₁ ++ l₂) = l₂
theorem list.drop_left' {α : Type u} {l₁ l₂ : list α} {n : } (h : l₁.length = n) :
(l₁ ++ l₂) = l₂
theorem list.drop_eq_nth_le_cons {α : Type u} {n : } {l : list α} (h : n < l.length) :
l = l.nth_le n h :: list.drop (n + 1) l
@[simp]
theorem list.drop_length {α : Type u} (l : list α) :
theorem list.drop_length_cons {α : Type u} {l : list α} (h : l list.nil) (a : α) :
(a :: l) = [l.last h]
theorem list.drop_append_eq_append_drop {α : Type u} {l₁ l₂ : list α} {n : } :
(l₁ ++ l₂) = l₁ ++ list.drop (n - l₁.length) l₂

Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n` in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them.

theorem list.drop_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : } (h : n l₁.length) :
(l₁ ++ l₂) = l₁ ++ l₂
theorem list.drop_append {α : Type u} {l₁ l₂ : list α} (i : ) :
list.drop (l₁.length + i) (l₁ ++ l₂) = l₂

Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements up to `i` in `l₂`.

theorem list.drop_sizeof_le {α : Type u} [has_sizeof α] (l : list α) (n : ) :
l).sizeof l.sizeof
theorem list.nth_le_drop {α : Type u} (L : list α) {i j : } (h : i + j < L.length) :
L.nth_le (i + j) h = L).nth_le j _

The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by dropping the first `i` elements. Version designed to rewrite from the big list to the small list.

theorem list.nth_le_drop' {α : Type u} (L : list α) {i j : } (h : j < L).length) :
L).nth_le j h = L.nth_le (i + j) _

The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by dropping the first `i` elements. Version designed to rewrite from the small list to the big list.

theorem list.nth_drop {α : Type u} (L : list α) (i j : ) :
L).nth j = L.nth (i + j)
@[simp]
theorem list.drop_drop {α : Type u} (n m : ) (l : list α) :
l) = list.drop (n + m) l
theorem list.drop_take {α : Type u} (m n : ) (l : list α) :
(list.take (m + n) l) = l)
theorem list.map_drop {α : Type u_1} {β : Type u_2} (f : α β) (L : list α) (i : ) :
L) = (list.map f L)
theorem list.modify_nth_tail_eq_take_drop {α : Type u} (f : list α list α) (H : = list.nil) (n : ) (l : list α) :
l = l ++ f l)
theorem list.modify_nth_eq_take_drop {α : Type u} (f : α α) (n : ) (l : list α) :
l = l ++ l)
theorem list.modify_nth_eq_take_cons_drop {α : Type u} (f : α α) {n : } {l : list α} (h : n < l.length) :
l = l ++ f (l.nth_le n h) :: list.drop (n + 1) l
theorem list.update_nth_eq_take_cons_drop {α : Type u} (a : α) {n : } {l : list α} (h : n < l.length) :
l.update_nth n a = l ++ a :: list.drop (n + 1) l
theorem list.reverse_take {α : Type u_1} {xs : list α} (n : ) (h : n xs.length) :
xs.reverse = (list.drop (xs.length - n) xs).reverse
@[simp]
theorem list.update_nth_eq_nil {α : Type u} (l : list α) (n : ) (a : α) :
@[simp]
theorem list.take'_length {α : Type u} [inhabited α] (n : ) (l : list α) :
l).length = n
@[simp]
theorem list.take'_nil {α : Type u} [inhabited α] (n : ) :
theorem list.take'_eq_take {α : Type u} [inhabited α] {n : } {l : list α} :
n l.length l = l
@[simp]
theorem list.take'_left {α : Type u} [inhabited α] (l₁ l₂ : list α) :
(l₁ ++ l₂) = l₁
theorem list.take'_left' {α : Type u} [inhabited α] {l₁ l₂ : list α} {n : } (h : l₁.length = n) :
(l₁ ++ l₂) = l₁

### foldl, foldr #

theorem list.foldl_ext {α : Type u} {β : Type v} (f g : α β α) (a : α) {l : list β} (H : (a : α) (b : β), b l f a b = g a b) :
a l = 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) :
b l = b l
@[simp]
theorem list.foldl_nil {α : Type u} {β : Type v} (f : α β α) (a : α) :
= a
@[simp]
theorem list.foldl_cons {α : Type u} {β : Type v} (f : α β α) (a : α) (b : β) (l : list β) :
a (b :: l) = (f a b) l
@[simp]
theorem list.foldr_nil {α : Type u} {β : Type v} (f : α β β) (b : β) :
= b
@[simp]
theorem list.foldr_cons {α : Type u} {β : Type v} (f : α β β) (b : β) (a : α) (l : list α) :
b (a :: l) = f a b l)
@[simp]
theorem list.foldl_append {α : Type u} {β : Type v} (f : α β α) (a : α) (l₁ l₂ : list β) :
a (l₁ ++ l₂) = a l₁) l₂
@[simp]
theorem list.foldr_append {α : Type u} {β : Type v} (f : α β β) (b : β) (l₁ l₂ : list α) :
b (l₁ ++ l₂) = b l₂) l₁
theorem list.foldl_fixed' {α : Type u} {β : Type v} {f : α β α} {a : α} (hf : (b : β), f a b = a) (l : list β) :
a l = a
theorem