# Documentation

Mathlib.Data.List.Basic

# Basic properties of lists #

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

There is only one list of an empty type

Equations
• List.uniqueOfIsEmpty = let src := instInhabitedList; { toInhabited := { default := default }, uniq := (_ : ∀ (l : List α), l = default) }
instance List.instIsLeftIdListAppendInstAppendListNil {α : Type u} :
IsLeftId (List α) Append.append []
Equations
instance List.instIsRightIdListAppendInstAppendListNil {α : Type u} :
IsRightId (List α) Append.append []
Equations
@[simp]
theorem List.cons_injective {α : Type u} {a : α} :
theorem List.cons_eq_cons {α : Type u} {a : α} {b : α} {l : List α} {l' : List α} :
a :: l = b :: l' a = b l = l'
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} [inst : ] {a : α} {b : α} {l : List α} (h : a b :: l) :
a = b a b a l
theorem List.eq_or_mem_of_mem_cons :
∀ {α : Type u_1} {a b : α} {l : List α}, a b :: la = b a l

Alias of the forward direction of List.mem_cons.

theorem List.not_mem_append {α : Type u} {a : α} {s : List α} {t : List α} (h₁ : ¬a s) (h₂ : ¬a t) :
¬a s ++ t
theorem List.mem_split {α : Type u} {a : α} {l : List α} (h : a l) :
s t, 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 :: la 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 :: la y ¬a l
@[simp]
theorem List.mem_map' {α : Type u} {β : Type v} {f : αβ} {b : β} {l : List α} :
b List.map f l a, a l f a = b
theorem List.exists_of_mem_map' {α : Type u} {β : Type v} {f : αβ} {b : β} {l : List α} :
b List.map f la, a l f a = b

Alias of the forward direction of List.mem_map'.

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.bind (List.map f l) g = List.bind l fun a => g (f a)

### length #

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

Alias of the reverse direction of List.length_pos.

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

Alias of the forward direction of List.length_pos.

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

Alias of List.Sublist.length_le.

### set-theoretic notation of lists #

instance List.instSingletonList {α : Type u} :
Singleton α (List α)
Equations
• List.instSingletonList = { singleton := fun x => [x] }
instance List.instInsertList {α : Type u} [inst : ] :
Insert α (List α)
Equations
• List.instInsertList = { insert := List.insert }
theorem List.singleton_eq {α : Type u} (x : α) :
{x} = [x]
theorem List.insert_neg {α : Type u} [inst : ] {x : α} {l : List α} (h : ¬x l) :
insert x l = x :: l
theorem List.insert_pos {α : Type u} [inst : ] {x : α} {l : List α} (h : x l) :
insert x l = l
theorem List.doubleton_eq {α : Type u} [inst : ] {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.not_exists_mem_nil {α : Type u} (p : αProp) :
¬x, x [] p 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 #

theorem List.subset_append_of_subset_right' {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) :
l l₂l l₁ ++ l₂
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 α} :
List.append L₁ L₂ = L₁ ++ L₂
theorem List.append_eq_cons_iff {α : Type u} {a : List α} {b : List α} {c : List α} {x : α} :
a ++ b = x :: c a = [] b = x :: c a', a = x :: a' c = a' ++ b
theorem List.cons_eq_append_iff {α : Type u} {a : List α} {b : List α} {c : List α} {x : α} :
x :: c = a ++ b a = [] b = x :: c a', a = x :: a' c = a' ++ b
theorem List.append_left_cancel {α : Type u} {s : List α} {t₁ : List α} {t₂ : List α} (h : s ++ t₁ = s ++ t₂) :
t₁ = t₂
theorem List.append_right_cancel {α : Type u} {s₁ : List α} {s₂ : List α} {t : List α} (h : s₁ ++ t = s₂ ++ t) :
s₁ = s₂
theorem List.append_right_injective {α : Type u} (s : List α) :
Function.Injective fun t => s ++ t
theorem List.append_left_injective {α : Type u} (t : List α) :
Function.Injective fun s => 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 = ∀ (b : α), b lb = a
theorem List.eq_replicate_of_mem {α : Type u} {a : α} {l : List α} :
(∀ (b : α), b lb = a) → l =

Alias of the reverse direction of List.eq_replicate_length.

theorem List.eq_replicate {α : Type u} {a : α} {n : } {l : List α} :
l = = n ∀ (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 : ) :
@[simp]
theorem List.join_replicate_nil {α : Type u} (n : ) :
List.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
@[simp]
theorem List.replicate_left_inj {α : Type u} {a : α} {n : } {m : } :
= n = m

### pure #

theorem List.bind_singleton {α : Type u} {β : Type v} (f : αList β) (x : α) :
List.bind [x] f = f x
@[simp]
theorem List.bind_singleton' {α : Type u} (l : List α) :
(List.bind l fun x => [x]) = l
theorem List.map_eq_bind {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
List.map f l = List.bind l fun x => [f x]
theorem List.bind_assoc {γ : Type w} {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) (g : βList γ) :
List.bind () g = List.bind l fun x => List.bind (f x) g
@[simp]
theorem List.mem_pure {α : Type u_1} (x : α) (y : α) :
x pure y x = y

### bind #

@[simp]
theorem List.bind_eq_bind {α : Type u_1} {β : Type u_1} (f : αList β) (l : List α) :
l >>= f =
theorem List.bind_append {α : Type u} {β : Type v} (f : αList β) (l₁ : List α) (l₂ : List α) :
List.bind (l₁ ++ l₂) f = List.bind l₁ f ++ List.bind l₂ f

### concat #

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

### reverse #

theorem List.reverse_cons' {α : Type u} (a : α) (l : List α) :
theorem List.reverse_singleton {α : Type u} (a : α) :
List.reverse [a] = [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₁ = l₂
theorem List.reverse_eq_iff {α : Type u} {l : List α} {l' : List α} :
= l' l =
@[simp]
theorem List.reverse_eq_nil {α : Type u} {l : List α} :
= [] l = []
theorem List.concat_eq_reverse_cons {α : Type u} (a : α) (l : List α) :
theorem List.map_reverse {α : Type u} {β : Type v} (f : αβ) (l : List α) :
theorem List.map_reverseAux {α : Type u} {β : Type v} (f : αβ) (l₁ : List α) (l₂ : List α) :
List.map f (List.reverseAux l₁ l₂) = List.reverseAux (List.map f l₁) (List.map f l₂)
theorem List.mem_reverse' {α : Type u} {a : α} {l : List α} :
a l
@[simp]
theorem List.reverse_replicate {α : Type u} (n : ) (a : α) :
=

### empty #

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

### dropLast #

@[simp]
theorem List.length_dropLast {α : Type u} (l : List α) :
= - 1
theorem List.dropLast_cons_cons {α : Type u} (a : α) (b : α) (l : List α) :

### getLast #

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

### getLast? #

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

theorem List.head!_eq_head? {α : Type u} [inst : ] (l : List α) :
theorem List.surjective_head {α : Type u} [inst : ] :
theorem List.eq_cons_of_mem_head? {α : Type u} {x : α} {l : List α} :
x l = x ::
theorem List.mem_of_mem_head? {α : Type u} {x : α} {l : List α} (h : x ) :
x l
@[simp]
theorem List.head!_cons {α : Type u} [inst : ] (a : α) (l : List α) :
List.head! (a :: l) = a
@[simp]
theorem List.head!_append {α : Type u} [inst : ] (t : List α) {s : List α} (h : s []) :
theorem List.head?_append {α : Type u} {s : List α} {t : List α} {x : α} (h : x ) :
theorem List.head?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} :
l₁ []List.head? (l₁ ++ l₂) =
theorem List.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : List α} (h : l []) :
List.tail (l ++ [a]) = ++ [a]
theorem List.cons_head?_tail {α : Type u} {l : List α} {a : α} :
a a :: = l
theorem List.head!_mem_head? {α : Type u} [inst : ] {l : List α} :
l []
theorem List.cons_head!_tail {α : Type u} [inst : ] {l : List α} (h : l []) :
= l
theorem List.head!_mem_self {α : Type u} [inst : ] {l : List α} (h : l []) :
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 []) :
List.tail (l ++ l') = ++ l'
@[simp]
theorem List.nthLe_tail {α : Type u} (l : List α) (i : ) (h : i < ) (h' : optParam (i + 1 < ) (_ : i + 1 < )) :
List.nthLe () i h = List.nthLe l (i + 1) h'
theorem List.nthLe_cons_aux {α : Type u} {l : List α} {a : α} {n : } (hn : n 0) (h : n < List.length (a :: l)) :
n - 1 <
theorem List.nthLe_cons {α : Type u} {l : List α} {a : α} {n : } (hl : n < List.length (a :: l)) :
List.nthLe (a :: l) n hl = if hn : n = 0 then a else List.nthLe l (n - 1) (_ : n - 1 < )
@[simp]
theorem List.modifyHead_modifyHead {α : Type u} (l : List α) (f : αα) (g : αα) :

### Induction from the right #

def List.reverseRecOn {α : Type u} {C : List αSort u_1} (l : List α) (H0 : C []) (H1 : (l : List α) → (a : α) → C lC (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
• One or more equations did not get rendered due to their size.
def List.bidirectionalRec {α : Type u} {C : List αSort u_1} (H0 : C []) (H1 : (a : α) → C [a]) (Hn : (a : α) → (l : List α) → (b : α) → C lC (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.bidirectionalRecOn {α : Type u} {C : List αSort u_1} (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

### sublists #

theorem List.Sublist.cons_cons {α : Type u} {l₁ : List α} {l₂ : List α} (a : α) (s : List.Sublist l₁ l₂) :
List.Sublist (a :: l₁) (a :: l₂)
theorem List.sublist_cons_of_sublist {α : Type u} (a : α) {l₁ : List α} {l₂ : List α} :
List.Sublist l₁ l₂List.Sublist l₁ (a :: l₂)
theorem List.sublist_of_cons_sublist_cons {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} :
List.Sublist (a :: l₁) (a :: l₂)List.Sublist l₁ l₂
theorem List.cons_sublist_cons_iff {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} :
List.Sublist (a :: l₁) (a :: l₂) List.Sublist l₁ l₂
@[simp]
theorem List.singleton_sublist {α : Type u} {a : α} {l : List α} :
List.Sublist [a] l a l
theorem List.eq_nil_of_sublist_nil {α : Type u} {l : List α} (s : List.Sublist l []) :
l = []
@[simp]
theorem List.sublist_nil_iff_eq_nil {α : Type u} {l : List α} :
List.Sublist l [] l = []
@[simp]
theorem List.replicate_sublist_replicate {α : Type u} {m : } {n : } (a : α) :
List.Sublist () () m n
theorem List.sublist_replicate_iff {α : Type u} {l : List α} {a : α} {n : } :
List.Sublist l () k, k n l =
theorem List.Sublist.eq_of_length {α : Type u} {l₁ : List α} {l₂ : List α} :
List.Sublist l₁ l₂ = l₁ = l₂
theorem List.Sublist.eq_of_length_le {α : Type u} {l₁ : List α} {l₂ : List α} (s : List.Sublist l₁ l₂) (h : ) :
l₁ = l₂
theorem List.Sublist.antisymm {α : Type u} {l₁ : List α} {l₂ : List α} (s₁ : List.Sublist l₁ l₂) (s₂ : List.Sublist l₂ l₁) :
l₁ = l₂
instance List.decidableSublist {α : Type u} [inst : ] (l₁ : List α) (l₂ : List α) :
Equations

### indexOf #

theorem List.indexOf_nil {α : Type u} [inst : ] (a : α) :
@[simp]
theorem List.indexOf_cons_self {α : Type u} [inst : ] (a : α) (l : List α) :
List.indexOf a (a :: l) = 0
theorem List.indexOf_cons_eq {α : Type u} [inst : ] {a : α} {b : α} (l : List α) :
a = bList.indexOf a (b :: l) = 0
@[simp]
theorem List.indexOf_cons_ne {α : Type u} [inst : ] {a : α} {b : α} (l : List α) :
a bList.indexOf a (b :: l) = Nat.succ ()
theorem List.indexOf_cons_ne.findIdx_go_succ {α : Type u} (p : αBool) (l : List α) (n : ) :
theorem List.indexOf_cons {α : Type u} [inst : ] (a : α) (b : α) (l : List α) :
List.indexOf a (b :: l) = if a = b then 0 else Nat.succ ()
theorem List.indexOf_eq_length {α : Type u} [inst : ] {a : α} {l : List α} :
= ¬a l
@[simp]
theorem List.indexOf_of_not_mem {α : Type u} [inst : ] {l : List α} {a : α} :
¬a l =
theorem List.indexOf_le_length {α : Type u} [inst : ] {a : α} {l : List α} :
theorem List.indexOf_lt_length {α : Type u} [inst : ] {a : α} {l : List α} :
< a l
theorem List.indexOf_append_of_mem {α : Type u} {l₁ : List α} {l₂ : List α} [inst : ] {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 α} [inst : ] {a : α} (h : ¬a l₁) :
List.indexOf a (l₁ ++ l₂) = + List.indexOf a l₂

### nth element #

theorem List.nthLe_of_mem {α : Type u} {a : α} {l : List α} (h : a l) :
n h, List.nthLe l n h = a
theorem List.nthLe_get? {α : Type u} {l : List α} {n : } (h : n < ) :
= some (List.nthLe l n h)
@[simp]
theorem List.get?_length {α : Type u} (l : List α) :
List.get? l () = none
theorem List.get?_eq_some' {α : Type u} {l : List α} {n : } {a : α} :
= some a h, List.nthLe l n h = a
theorem List.nthLe_mem {α : Type u} (l : List α) (n : ) (h : n < ) :
List.nthLe l n h l
theorem List.mem_iff_nthLe {α : Type u} {a : α} {l : List α} :
a l n h, List.nthLe l n h = a
theorem List.get?_injective {α : Type u} {xs : List α} {i : } {j : } (h₀ : i < ) (h₁ : ) (h₂ : List.get? xs i = List.get? xs j) :
i = j
theorem List.nthLe_map {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : } (H1 : n < List.length (List.map f l)) (H2 : n < ) :
List.nthLe (List.map f l) n H1 = f (List.nthLe l n H2)
theorem List.get_map_rev {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : Fin ()} :
f (List.get l n) = List.get (List.map f l) { val := n, isLt := (_ : n < List.length (List.map f l)) }

A version of get_map that can be used for rewriting.

theorem List.nthLe_map_rev {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : } (H : n < ) :
f (List.nthLe l n H) = List.nthLe (List.map f l) n (_ : n < List.length (List.map f l))

A version of nthLe_map that can be used for rewriting.

@[simp]
theorem List.nthLe_map' {α : Type u} {β : Type v} (f : αβ) {l : List α} {n : } (H : n < List.length (List.map f l)) :
List.nthLe (List.map f l) n H = f (List.nthLe l n (_ : n < ))
theorem List.nthLe_of_eq {α : Type u} {L : List α} {L' : List α} (h : L = L') {i : } (hi : i < ) :
List.nthLe L i hi = List.nthLe L' i (_ : i < )

If one has nthLe 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.nthLe_singleton {α : Type u} (a : α) {n : } (hn : n < 1) :
List.nthLe [a] n hn = a
theorem List.nthLe_zero {α : Type u} [inst : ] {L : List α} (h : 0 < ) :
List.nthLe L 0 h =
theorem List.nthLe_append {α : Type u} {l₁ : List α} {l₂ : List α} {n : } (hn₁ : n < List.length (l₁ ++ l₂)) (hn₂ : n < ) :
List.nthLe (l₁ ++ l₂) n hn₁ = List.nthLe l₁ n hn₂
theorem List.nthLe_append_right {α : Type u} {l₁ : List α} {l₂ : List α} {n : } (h₁ : n) (h₂ : n < List.length (l₁ ++ l₂)) :
List.nthLe (l₁ ++ l₂) n h₂ = List.nthLe l₂ (n - ) (_ : n - < )
theorem List.nthLe_replicate {α : Type u} (a : α) {n : } {m : } (h : m < ) :
List.nthLe () m h = a
theorem List.getLast_eq_nthLe {α : Type u} (l : List α) (h : l []) :
= List.nthLe l ( - 1) (_ : - 1 < )
theorem List.get_length_sub_one {α : Type u} {l : List α} (h : - 1 < ) :
List.get l { val := - 1, isLt := h } = List.getLast l (_ : l = []False)
theorem List.nthLe_length_sub_one {α : Type u} {l : List α} (h : - 1 < ) :
List.nthLe l ( - 1) h = List.getLast l (_ : l = []False)
theorem List.nthLe_cons_length {α : Type u} (x : α) (xs : List α) (n : ) (h : n = ) :
List.nthLe (x :: xs) n (_ : n < Nat.succ ()) = List.getLast (x :: xs) (_ : x :: xs [])
theorem List.take_one_drop_eq_of_lt_length {α : Type u} {l : List α} {n : } (h : n < ) :
List.take 1 () = [List.get l { val := n, isLt := h }]
theorem List.take_one_drop_eq_of_lt_length' {α : Type u} {l : List α} {n : } (h : n < ) :
List.take 1 () = [List.nthLe l n h]
theorem List.ext_nthLe {α : Type u} {l₁ : List α} {l₂ : List α} (hl : = ) (h : ∀ (n : ) (h₁ : n < ) (h₂ : n < ), List.nthLe l₁ n h₁ = List.nthLe l₂ n h₂) :
l₁ = l₂
@[simp]
theorem List.indexOf_get {α : Type u} [inst : ] {a : α} {l : List α} (h : < ) :
List.get l { val := , isLt := h } = a
@[simp]
theorem List.indexOf_nthLe {α : Type u} [inst : ] {a : α} {l : List α} (h : < ) :
List.nthLe l () h = a
@[simp]
theorem List.indexOf_get? {α : Type u} [inst : ] {a : α} {l : List α} (h : a l) :
theorem List.get_reverse_aux₁ {α : Type u} (l : List α) (r : List α) (i : ) (h1 : i + < ) (h2 : i < ) :
List.get () { val := i + , isLt := h1 } = List.get r { val := i, isLt := h2 }
theorem List.indexOf_inj {α : Type u} [inst : ] {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 : - 1 - i < ) (h2 : i < ) :
List.get () { val := - 1 - i, isLt := h1 } = List.get l { val := i, isLt := h2 }
@[simp]
theorem List.get_reverse {α : Type u} (l : List α) (i : ) (h1 : - 1 - i < ) (h2 : i < ) :
List.get () { val := - 1 - i, isLt := h1 } = List.get l { val := i, isLt := h2 }
@[simp]
theorem List.nthLe_reverse {α : Type u} (l : List α) (i : ) (h1 : - 1 - i < ) (h2 : i < ) :
List.nthLe () ( - 1 - i) h1 = List.nthLe l i h2
theorem List.nthLe_reverse' {α : Type u} (l : List α) (n : ) (hn : n < ) (hn' : - 1 - n < ) :
List.nthLe () n hn = List.nthLe l ( - 1 - n) hn'
theorem List.get_reverse' {α : Type u} (l : List α) (n : Fin ()) (hn' : - 1 - n < ) :
List.get () n = List.get l { val := - 1 - n, isLt := hn' }
theorem List.eq_cons_of_length_one {α : Type u} {l : List α} (h : = 1) :
l = [List.nthLe l 0 (_ : 0 < )]
theorem List.get_eq_iff {α : Type u} {l : List α} {n : Fin ()} {x : α} :
List.get l n = x List.get? l n = some x
theorem List.nthLe_eq_iff {α : Type u} {l : List α} {n : } {x : α} {h : n < } :
List.nthLe l n h = x = some x
theorem List.some_nthLe_eq {α : Type u} {l : List α} {n : } {h : n < } :
some (List.nthLe l n h) =
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.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.modifyNthTail g (m - n) (f l)) n l
theorem List.modifyNthTail_modifyNthTail_same {α : Type u} {f : List αList α} {g : List αList α} (n : ) (l : List α) :
theorem List.removeNth_eq_nthTail {α : Type u} (n : ) (l : List α) :
= List.modifyNthTail List.tail n l
theorem List.modifyNth_eq_set {α : Type u} (f : αα) (n : ) (l : List α) :
= Option.getD ((fun a => List.set l n (f a)) <$> ) l theorem List.length_modifyNthTail {α : Type u} (f : List αList α) (H : ∀ (l : List α), List.length (f l) = ) (n : ) (l : List α) : theorem List.length_modifyNth {α : Type u} (f : αα) (n : ) (l : List α) : @[simp] theorem List.nthLe_set_eq {α : Type u} (l : List α) (i : ) (a : α) (h : i < List.length (List.set l i a)) : List.nthLe (List.set l i a) i h = a @[simp] theorem List.get_set_of_ne {α : Type u} {l : List α} {i : } {j : } (h : i j) (a : α) (hj : j < List.length (List.set l i a)) : List.get (List.set l i a) { val := j, isLt := hj } = List.get l { val := j, isLt := (_ : j < ) } @[simp] theorem List.nthLe_set_of_ne {α : Type u} {l : List α} {i : } {j : } (h : i j) (a : α) (hj : j < List.length (List.set l i a)) : List.nthLe (List.set l i a) j hj = List.nthLe l j (_ : j < ) @[simp] theorem List.insertNth_zero {α : Type u} (s : List α) (x : α) : = x :: s @[simp] theorem List.insertNth_succ_nil {α : Type u} (n : ) (a : α) : List.insertNth (n + 1) a [] = [] @[simp] theorem List.insertNth_succ_cons {α : Type u} (s : List α) (hd : α) (x : α) (n : ) : List.insertNth (n + 1) x (hd :: s) = hd :: theorem List.length_insertNth {α : Type u} {a : α} (n : ) (as : List α) : n List.length (List.insertNth n a as) = + 1 theorem List.removeNth_insertNth {α : Type u} {a : α} (n : ) (l : List α) : theorem List.insertNth_removeNth_of_ge {α : Type u} {a : α} (n : ) (m : ) (as : List α) : n < n mList.insertNth m a () = List.removeNth (List.insertNth (m + 1) a as) n theorem List.insertNth_removeNth_of_le {α : Type u} {a : α} (n : ) (m : ) (as : List α) : n < m nList.insertNth m a () = List.removeNth (List.insertNth m a as) (n + 1) theorem List.insertNth_comm {α : Type u} (a : α) (b : α) (i : ) (j : ) (l : List α) : i jj List.insertNth (j + 1) b () = List.insertNth i a () theorem List.mem_insertNth {α : Type u} {a : α} {b : α} {n : } {l : List α} : n → (a a = b a l) theorem List.insertNth_of_length_lt {α : Type u} (l : List α) (x : α) (n : ) (h : < n) : = l @[simp] theorem List.insertNth_length_self {α : Type u} (l : List α) (x : α) : = l ++ [x] theorem List.length_le_length_insertNth {α : Type u} (l : List α) (x : α) (n : ) : theorem List.length_insertNth_le_succ {α : Type u} (l : List α) (x : α) (n : ) : theorem List.get_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hn : k < n) (hk : k < ) (hk' : optParam (k < List.length ()) (_ : k < List.length ())) : List.get () { val := k, isLt := hk' } = List.get l { val := k, isLt := hk } theorem List.nthLe_insertNth_of_lt {α : Type u} (l : List α) (x : α) (n : ) (k : ) : k < n∀ (hk : k < ) (hk' : optParam (k < List.length ()) (_ : k < List.length ())), List.nthLe () k hk' = List.nthLe l k hk @[simp] theorem List.get_insertNth_self {α : Type u} (l : List α) (x : α) (n : ) (hn : n ) (hn' : optParam (n < List.length ()) (_ : n < List.length ())) : List.get () { val := n, isLt := hn' } = x @[simp] theorem List.nthLe_insertNth_self {α : Type u} (l : List α) (x : α) (n : ) (hn : n ) (hn' : optParam (n < List.length ()) (_ : n < List.length ())) : List.nthLe () n hn' = x theorem List.get_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hk' : n + k < ) (hk : optParam (n + k + 1 < List.length ()) (_ : n + k + 1 < List.length ())) : List.get () { val := n + k + 1, isLt := hk } = List.get l { val := n + k, isLt := hk' } theorem List.nthLe_insertNth_add_succ {α : Type u} (l : List α) (x : α) (n : ) (k : ) (hk' : n + k < ) (hk : optParam (n + k + 1 < List.length ()) (_ : n + k + 1 < List.length ())) : List.nthLe () (n + k + 1) hk = List.nthLe l (n + k) hk' theorem List.insertNth_injective {α : Type u} (n : ) (x : α) : ### map # theorem List.map_eq_foldr {α : Type u} {β : Type v} (f : αβ) (l : List α) : List.map f l = List.foldr (fun a bs => 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 () = List.concat (List.map f l) (f a) @[simp] theorem List.map_id'' {α : Type u} (l : List α) : List.map (fun x => x) l = l 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 α)) : theorem List.bind_ret_eq_map {α : Type u} {β : Type v} (f : αβ) (l : List α) : List.bind l (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) : = @[simp] theorem List.map_eq_map {α : Type u_1} {β : Type u_1} (f : αβ) (l : List α) : f <$> l = List.map f l
@[simp]
theorem List.map_tail {α : Type u} {β : Type v} (f : αβ) (l : List α) :
@[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 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 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 => bif p a then f a :: bs else bs) [] as
theorem List.getLast_map {α : Type u} {β : Type v} (f : αβ) {l : List α} (hl : l []) :
List.getLast (List.map f l) (_ : ¬List.map f l = []) = f (List.getLast l hl)
theorem List.map_eq_replicate_iff {α : Type u} {β : Type v} {l : List α} {f : αβ} {b : β} :
List.map f l = ∀ (x : α), x lf x = b
@[simp]
theorem List.map_const {α : Type u} {β : Type v} (l : List α) (b : β) :
List.map () l =
@[simp]
theorem List.map_const' {α : Type u} {β : Type v} (l : List α) (b : β) :
List.map (fun x => b) l =
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 #

@[simp]
theorem List.take_zero {α : Type u} (l : List α) :
= []
@[simp]
theorem List.take_nil {α : Type u} (n : ) :
List.take n [] = []
theorem List.take_cons {α : Type u} (n : ) (a : α) (l : List α) :
List.take () (a :: l) = a ::
theorem List.take_all_of_le {α : Type u} {n : } {l : List α} :
n = l
@[simp]
theorem List.take_left {α : Type u} (l₁ : List α) (l₂ : List α) :
List.take () (l₁ ++ l₂) = l₁
theorem List.take_left' {α : Type u} {l₁ : List α} {l₂ : List α} {n : } (h : = n) :
List.take n (l₁ ++ l₂) = l₁
theorem List.take_take {α : Type u} (n : ) (m : ) (l : List α) :
List.take n () = List.take (min n m) l
theorem List.take_replicate {α : Type u} (a : α) (n : ) (m : ) :
theorem List.map_take {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : ) :
theorem List.take_append_eq_append_take {α : Type u} {l₁ : List α} {l₂ : List α} {n : } :
List.take n (l₁ ++ l₂) = List.take n l₁ ++ List.take (n - ) 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₁ : List α} {l₂ : List α} {n : } (h : n ) :
List.take n (l₁ ++ l₂) = List.take n l₁
theorem List.take_append {α : Type u} {l₁ : List α} {l₂ : List α} (i : ) :
List.take ( + i) (l₁ ++ l₂) = l₁ ++ List.take i 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.get_take {α : Type u} (L : List α) {i : } {j : } (hi : i < ) (hj : i < j) :
List.get L { val := i, isLt := hi } = List.get () { val := i, isLt := (_ : i < List.length ()) }

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.nthLe_take {α : Type u} (L : List α) {i : } {j : } (hi : i < ) (hj : i < j) :
List.nthLe L i hi = List.nthLe () i (_ : i < List.length ())

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.get_take' {α : Type u} (L : List α) {j : } {i : Fin (List.length ())} :
List.get () i = List.get L { val := i, isLt := (_ : 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.nthLe_take' {α : Type u} (L : List α) {i : } {j : } (hi : i < List.length ()) :
List.nthLe () i hi = List.nthLe L i (_ : 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.get?_take {α : Type u} {l : List α} {n : } {m : } (h : m < n) :
List.get? () m =
@[simp]
theorem List.nth_take_of_succ {α : Type u} {l : List α} {n : } :
List.get? (List.take (n + 1) l) n =
theorem List.take_succ {α : Type u} {l : List α} {n : } :
@[simp]
theorem List.take_eq_nil_iff {α : Type u} {l : List α} {k : } :
= [] l = [] k = 0
theorem List.take_eq_take {α : Type u} {l : List α} {m : } {n : } :
= min m () = min n ()
theorem List.take_add {α : Type u} (l : List α) (m : ) (n : ) :
List.take (m + n) l = ++ List.take n ()
theorem List.dropLast_eq_take {α : Type u} (l : List α) :
= List.take () l
theorem List.dropLast_take {α : Type u} {n : } {l : List α} (h : n < ) :
theorem List.dropLast_cons_of_ne_nil {α : Type u_1} {x : α} {l : List α} (h : l []) :
@[simp]
theorem List.dropLast_append_of_ne_nil {α : Type u_1} {l : List α} (l' : List α) :
l []List.dropLast (l' ++ l) = l' ++
theorem List.drop_eq_nil_iff_le {α : Type u} {l : List α} {k : } :
= [] k
theorem List.tail_drop {α : Type u} (l : List α) (n : ) :
List.tail () = List.drop (n + 1) l
theorem List.cons_get_drop_succ {α : Type u} {l : List α} {n : Fin ()} :
List.get l n :: List.drop (n + 1) l = List.drop (n) l
theorem List.cons_nthLe_drop_succ {α : Type u} {l : List α} {n : } (hn : n < ) :
List.nthLe l n hn :: List.drop (n + 1) l =
@[simp]
theorem List.drop_one {α : Type u} (l : List α) :
=
theorem List.drop_add {α : Type u} (m : ) (n : ) (l : List α) :
List.drop (m + n) l = List.drop m ()
@[simp]
theorem List.drop_left {α : Type u} (l₁ : List α) (l₂ : List α) :
List.drop () (l₁ ++ l₂) = l₂
theorem List.drop_left' {α : Type u} {l₁ : List α} {l₂ : List α} {n : } (h : = n) :
List.drop n (l₁ ++ l₂) = l₂
theorem List.drop_eq_get_cons {α : Type u} {n : } {l : List α} (h : n < ) :
= List.get l { val := n, isLt := h } :: List.drop (n + 1) l
theorem List.drop_length_cons {α : Type u} {l : List α} (h : l []) (a : α) :
List.drop () (a :: l) = []
theorem List.drop_append_eq_append_drop {α : Type u} {l₁ : List α} {l₂ : List α} {n : } :
List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ List.drop (n - ) 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₁ : List α} {l₂ : List α} {n : } (h : n ) :
List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ l₂
theorem List.drop_append {α : Type u} {l₁ : List α} {l₂ : List α} (i : ) :
List.drop ( + i) (l₁ ++ l₂) = List.drop i 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} [inst : ] (l : List α) (n : ) :
theorem List.get_drop {α : Type u} (L : List α) {i : } {j : } (h : i + j < ) :
List.get L { val := i + j, isLt := h } = List.get () { val := j, isLt := (_ : j < List.length ()) }

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.nthLe_drop {α : Type u} (L : List α) {i : } {j : } (h : i + j < ) :
List.nthLe L (i + j) h = List.nthLe () j (_ : j < List.length ())

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.get_drop' {α : Type u} (L : List α) {i : } {j : Fin (List.length ())} :
List.get () j = List.get L { val := i + j, isLt := (_ : 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.nthLe_drop' {α : Type u} (L : List α) {i : } {j : } (h : j < List.length ()) :
List.nthLe () j h = List.nthLe L (i + j) (_ : 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.get?_drop {α : Type u} (L : List α) (i : ) (j : ) :
List.get? () j = List.get? L (i + j)
@[simp]
theorem List.drop_drop {α : Type u} (n : ) (m : ) (l : List α) :
List.drop n () = List.drop (n + m) l
theorem List.drop_take {α : Type u} (m : ) (n : ) (l : List α) :
List.drop m (List.take (m + n) l) = List.take n ()
theorem List.map_drop {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : ) :
theorem List.modifyNthTail_eq_take_drop {α : Type u} (f : List αList α) (H : f [] = []) (n : ) (l : List α) :
= ++ f ()
theorem List.modifyNth_eq_take_drop {α : Type u} (f : αα) (n : ) (l : List α) :
theorem List.modifyNth_eq_take_cons_drop {α : Type u} (f : αα) {n : } {l : List α} (h : n < ) :
= ++ f (List.get l { val := n, isLt := h }) :: List.drop (n + 1) l
theorem List.set_eq_take_cons_drop {α : Type u} (a : α) {n : } {l : List α} (h : n < ) :
List.set l n a = ++ a :: List.drop (n + 1) l
theorem List.reverse_take {α : Type u_1} {xs : List α} (n : ) (h : n ) :
@[simp]
theorem List.set_eq_nil {α : Type u} (l : List α) (n : ) (a : α) :
List.set l n a = [] l = []
@[simp]
theorem List.takeI_length {α : Type u} [inst : ] (n : ) (l : List α) :
@[simp]
theorem List.takeI_nil {α : Type u} [inst : ] (n : ) :
List.takeI n [] = List.replicate n default
theorem List.takeI_eq_take {α : Type u} [inst : ] {n : } {l : List α} :
n =
@[simp]
theorem List.takeI_left {α : Type u} [inst : ] (l₁ : List α) (l₂ : List α) :
List.takeI () (l₁ ++ l₂) = l₁
theorem List.takeI_left' {α : Type u} [inst : ] {l₁ : List α} {l₂ : List α} {n : } (h : = n) :
List.takeI n (l₁ ++ l₂) = l₁
@[simp]
theorem List.takeD_length {α : Type u} (n : ) (l : List α) (a : α) :
theorem List.takeD_eq_take {α : Type u} {n : } {l : List α} (a : α) :
n List.takeD n l a =
@[simp]
theorem List.takeD_left {α : Type u} (l₁ : List α) (l₂ : List α) (a : α) :
List.takeD () (l₁ ++ l₂) a = l₁
theorem List.takeD_left' {α : Type u} {l₁ : List α} {l₂ : List α} {n : } {a : α} (h : = 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
@[simp]
theorem List.foldl_nil {α : Type u} {β : Type v} (f : αβα) (a : α) :
List.foldl f a [] = a
@[simp]
theorem List.foldl_cons {α : Type u} {β : Type v} (f : αβα) (a : α) (b : β) (l : List β) :
List.foldl f a (b :: l) = List.foldl f (f a b) l
@[simp]
theorem List.foldr_nil {α : Type u} {β : Type v} (f : αββ) (b : β) :
List.foldr f b [] = b
@[simp]
theorem List.foldr_cons {α : Type u} {β : Type v} (f : αββ) (b : β) (a : α) (l : List α) :
List.foldr f b (a :: l) = f a (List.foldr f b l)
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 () = List.foldl () a L
@[simp]
theorem List.foldr_join {α : Type u} {β : Type v} (f : αββ) (b : β) (L : List (List α)) :
List.foldr f b () = List.foldr (fun l 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.reverse (List.foldl (fun t h => h :: t) [] l) = 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_1} {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_1} (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∈ 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.
def List.foldlRecOn {α : Type u} {β : Type v} {C : βSort u_1} (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∈ 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.
@[simp]
theorem List.foldrRecOn_nil {α : Type u} {β : Type v} {C : βSort u_1} (op : αββ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a []C (op a b)) :
List.foldrRecOn [] op b hb hl = hb
@[simp]
theorem List.foldrRecOn_cons {α : Type u} {β : Type v} {C : βSort u_1} (x : α) (l : List α) (op : αββ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a x :: lC (op a b)) :
List.foldrRecOn (x :: l) op b hb hl = hl (List.foldr op b l) (List.foldrRecOn l op b hb fun b hb a ha => hl b hb a (_ : a x :: l)) x (_ : x x :: l)
@[simp]
theorem List.foldlRecOn_nil {α : Type u} {β : Type v} {C : βSort u_1} (op : βαβ) (b : β) (hb : C b) (hl : (b : β) → C b(a : α) → a []C (op b a)) :
List.foldlRecOn [] op b hb hl = hb
theorem List.length_scanl {α : Type u} {β : Type v} {f : βαβ} (a : β) (l : List α) :
@[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 α} :
@[simp]
theorem List.get_zero_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {h : 0 < List.length (List.scanl f b l)} :
List.get (List.scanl f b l) { val := 0, isLt := h } = b
@[simp]
theorem List.nthLe_zero_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {h : 0 < List.length (List.scanl f b l)} :
List.nthLe (List.scanl f b l) 0 h = b
theorem List.get?_succ_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {i : } :
List.get? (List.scanl f b l) (i + 1) = Option.bind (List.get? (List.scanl f b l) i) fun x => Option.map (fun y => f x y) ()
theorem List.nthLe_succ_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {i : } {h : i + 1 < List.length (List.scanl f b l)} :
List.nthLe (List.scanl f b l) (i + 1) h = f (List.nthLe (List.scanl f b l) i (_ : i < List.length (List.scanl f b l))) (List.nthLe l i (_ : i < ))
theorem List.get_succ_scanl {α : Type u} {β : Type v} {f : βαβ} {b : β} {l : List α} {i : } {h : i + 1 < List.length (List.scanl f b l)} :
List.get (List.scanl f b l) { val := i + 1, isLt := h } = f (List.get (List.scanl f b l) { val := i, isLt := (_ : i < List.length (List.scanl f b l)) }) (List.get l { val := i, isLt := (_ : 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 #

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

### intersperse #

@[simp]
theorem List.intersperse_nil {α : Type u} (a : α) :
= []
@[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 < then (Array.toList acc ++ List.take n xs, List.drop n xs) else (l, [])
@[simp]
theorem List.splitOn_nil {α : Type u} [inst : ] (a : α) :
List.splitOn a [] = [[]]
@[simp]
theorem List.splitOnP_nil {α : Type u} (p : αBool) :
= [[]]
theorem List.splitOnP.go_append {α : Type u} (p : αBool) (xs : List α) (acc : ) (r : Array (List α)) :
theorem List.splitOnP.go_acc {α : Type u} (p : αBool) (xs : List α) (acc : ) :
List.splitOnP.go p xs acc #[] = List.modifyHead () (List.splitOnP.go p xs #[] #[])
theorem List.splitOnP_ne_nil {α : Type u} (p : αBool) (xs : List α) :
[]
theorem List.splitOnP_ne_nil.modifyHead_ne_nil_of_ne_nil {α : Type u} {f : αα} {l : List α} :
l [] []
@[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.join (List.zipWith (fun x x_1 => x ++ x_1) () (List.map (fun x => [x]) (List.filter p as) ++ [[]])) = 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.join (List.zipWith (fun x x_1 => x ++ x_1) (List.modifyHead () xs) ys) = a :: List.join (List.zipWith (fun x x_1 => x ++ x_1) xs ys)
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 : α) [inst : ] :

intercalate [x] is the left inverse of splitOn x

theorem List.splitOn_intercalate {α : Type u} (ls : List (List α)) [inst : ] (x : α) (hx : ∀ (l : List α), l ls¬x l) (hls : 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 : ) :
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 #

def List.pmap {α : Type u} {β : Type v} {p : αProp} (f : (a : α) → p aβ) (l : List α) :
((a : α) → a lp a) → List β

Partial map. If f : Π a, p a → β→ β is a partial function defined on a : α satisfying p, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy p, using the proof to apply f.

Equations
def List.attach {α : Type u} (l : List α) :
List { x // x l }

"Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}∈ l}.

Equations
theorem List.sizeOf_lt_sizeOf_of_mem {α : Type u} [inst : ] {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 => 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 => 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 => g (f a) h) l fun a h => H (f a) (_ : f a List.map f 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 => f (x) (H x (_ : x l))) ()
theorem List.attach_map_coe' {α : Type u} {β : Type v} (l : List α) (f : αβ) :
List.map (fun i => f i) () = List.map f l
theorem List.attach_map_val' {α : Type u} {β : Type v} (l : List α) (f : αβ) :
List.map (fun i => f i) () = List.map f l
@[simp]
theorem List.attach_map_val {α : Type u} (l : List α) :
List.map Subtype.val () = l
@[simp]
theorem List.mem_attach {α : Type u} (l : List α) (x : { x // x l }) :
x
@[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, f a (H a h) = b
@[simp]
theorem List.length_pmap {α : Type u} {β : Type v} {p : αProp} {f : (a : α) → p aβ} {l : List α} {H : (a : α) → a lp a} :
@[simp]
theorem List.length_attach {α : Type u} (L : List α) :
@[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 = []
theorem List.getLast_pmap {α : Type u_1} {β : Type u_2} (p : αProp) (f : (a : α) → p aβ) (l : List α) (hl₁ : (a : α) → a lp a) (hl₂ : l []) :
List.getLast (List.pmap f l hl₁) (_ : ¬List.pmap f l hl₁ = []) = f (List.getLast l hl₂) (hl₁ (List.getLast l hl₂) (_ : List.getLast l hl₂ l))
theorem List.get?_pmap {α : Type u} {β : Type v} {p : αProp} (f : (a : α) → p aβ) {l : List α} (h : (a : α) → a lp a) (n : ) :
List.get? (List.pmap f l h) n = Option.pmap f () fun x H => h x (_ : x l)
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.length (List.pmap f l h)) :
List.get (List.pmap f l h) { val := n, isLt := hn } = f (List.get l { val := n, isLt := (_ : n < ) }) (h (List.get l { val := n, isLt := (_ : n < ) }) (_ : List.get l { val := n, isLt := (_ : n < ) } l))
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.length (List.pmap f l h)) :
List.nthLe (List.pmap f l h) n hn = f (List.nthLe l n (_ : n < )) (h (List.nthLe l n (_ : n < )) (_ : List.get l { val := n, isLt := (_ : n < ) } l))
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₁ fun a ha => h a (_ : a l₁ ++ l₂)) ++ List.pmap f l₂ fun a ha => h a (_ : a l₁ ++ l₂)
theorem List.pmap_append' {α : Type u_1} {β : Type u_2} {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₂) fun a ha => Or.elim (_ : a l₁ a l₂) (h₁ a) (h₂ a)) = List.pmap f l₁ h₁ ++ List.pmap f l₂ h₂

### find #

@[simp]
theorem List.find?_nil {α : Type u} (p : αBool) :
List.find? p [] = none
@[simp]
theorem List.find?_cons_of_pos {α : Type u} {p : αBool} {a : α} (l : List α) (h : p a = true) :
List.find? p (a :: l) = some a
@[simp]
theorem List.find?_cons_of_neg {α : Type u} {p : αBool} {a : α} (l : List α) (h : ¬p a = true) :
List.find? p (a :: l) =
@[simp]
theorem List.find?_eq_none {α : Type u} {p : αBool} {l : List α} :
= none ∀ (x : α), x l¬p x = true
theorem List.find?_some {α : Type u} {p : αBool} {l : List α} {a : α} (H : = some a) :
p a = true
@[simp]
theorem List.find?_mem {α : Type u} {p : αBool} {l : List α} {a : α} (H : = some a) :
a l

### lookmap #

theorem List.lookmap.go_append {α : Type u} (f : α) (l : List α) (acc : ) :
@[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