# Bootstrapping theorems for lists #

These are theorems used in the definitions of Std.Data.List.Basic and tactics. New theorems should be added to Std.Data.List.Lemmas if they are not needed by the bootstrap.

@[simp]
theorem List.get?_nil {α : Type u_1} {n : Nat} :
[].get? n = none
@[simp]
theorem List.get?_cons_zero {α : Type u_1} {a : α} {l : List α} :
(a :: l).get? 0 = some a
@[simp]
theorem List.get?_cons_succ {α : Type u_1} {a : α} {l : List α} {n : Nat} :
(a :: l).get? (n + 1) = l.get? n
@[simp]
theorem List.get_cons_zero :
∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).get 0 = a
@[simp]
theorem List.head?_nil {α : Type u_1} :
@[simp]
theorem List.head?_cons {α : Type u_1} {a : α} {l : List α} :
(a :: l).head? = some a
@[simp]
theorem List.headD_nil {α : Type u_1} {d : α} :
@[simp]
theorem List.headD_cons {α : Type u_1} {a : α} {l : List α} {d : α} :
(a :: l).headD d = a
@[simp]
theorem List.head_cons {α : Type u_1} {a : α} {l : List α} {h : a :: l []} :
(a :: l).head h = a
@[simp]
theorem List.tail?_nil {α : Type u_1} :
[].tail? = none
@[simp]
theorem List.tail?_cons {α : Type u_1} {a : α} {l : List α} :
(a :: l).tail? = some l
@[simp]
theorem List.tail!_cons {α : Type u_1} {a : α} {l : List α} :
(a :: l).tail! = l
@[simp]
theorem List.tailD_nil {α : Type u_1} {l' : List α} :
[].tailD l' = l'
@[simp]
theorem List.tailD_cons {α : Type u_1} {a : α} {l : List α} {l' : List α} :
(a :: l).tailD l' = l
@[simp]
theorem List.any_nil :
∀ {α : Type u_1} {f : αBool}, [].any f = false
@[simp]
theorem List.any_cons :
∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, (a :: l).any f = (f a || l.any f)
@[simp]
theorem List.all_nil :
∀ {α : Type u_1} {f : αBool}, [].all f = true
@[simp]
theorem List.all_cons :
∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, (a :: l).all f = (f a && l.all f)
@[simp]
theorem List.or_nil :
[].or = false
@[simp]
theorem List.or_cons {a : Bool} {l : } :
(a :: l).or = (a || l.or)
@[simp]
theorem List.and_nil :
[].and = true
@[simp]
theorem List.and_cons {a : Bool} {l : } :
(a :: l).and = (a && l.and)

### length #

theorem List.eq_nil_of_length_eq_zero :
∀ {α : Type u_1} {l : List α}, l.length = 0l = []
theorem List.ne_nil_of_length_eq_succ :
∀ {α : Type u_1} {l : List α} {n : Nat}, l.length = n.succl []
theorem List.length_eq_zero :
∀ {α : Type u_1} {l : List α}, l.length = 0 l = []

### mem #

@[simp]
theorem List.not_mem_nil {α : Type u_1} (a : α) :
¬a []
@[simp]
theorem List.mem_cons :
∀ {α : Type u_1} {a b : α} {l : List α}, a b :: l a = b a l
theorem List.mem_cons_self {α : Type u_1} (a : α) (l : List α) :
a a :: l
theorem List.mem_cons_of_mem {α : Type u_1} (y : α) {a : α} {l : List α} :
a la y :: l
theorem List.eq_nil_iff_forall_not_mem {α : Type u_1} {l : List α} :
l = [] ∀ (a : α), ¬a l

### append #

@[simp]
theorem List.singleton_append :
∀ {α : Type u_1} {x : α} {l : List α}, [x] ++ l = x :: l
theorem List.append_inj {α : Type u_1} {s₁ : List α} {s₂ : List α} {t₁ : List α} {t₂ : List α} :
s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengths₁ = s₂ t₁ = t₂
theorem List.append_inj_right :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengtht₁ = t₂
theorem List.append_inj_left :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengths₁ = s₂
theorem List.append_inj' :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = s₂ t₁ = t₂
theorem List.append_inj_right' :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengtht₁ = t₂
theorem List.append_inj_left' :
∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = s₂
theorem List.append_right_inj {α : Type u_1} {t₁ : List α} {t₂ : List α} (s : List α) :
s ++ t₁ = s ++ t₂ t₁ = t₂
theorem List.append_left_inj {α : Type u_1} {s₁ : List α} {s₂ : List α} (t : List α) :
s₁ ++ t = s₂ ++ t s₁ = s₂
@[simp]
theorem List.append_eq_nil :
∀ {α : Type u_1} {p q : List α}, p ++ q = [] p = [] q = []
theorem List.get_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (n : Nat) (h : n < l₁.length) :
(l₁ ++ l₂).get n, = l₁.get n, h

### map #

@[simp]
theorem List.map_nil {α : Type u_1} {β : Type u_2} {f : αβ} :
List.map f [] = []
@[simp]
theorem List.map_cons {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) (l : List α) :
List.map f (a :: l) = f a :: List.map f l
@[simp]
theorem List.map_append {α : Type u_1} {β : Type u_2} (f : αβ) (l₁ : List α) (l₂ : List α) :
List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂
@[simp]
theorem List.map_id {α : Type u_1} (l : List α) :
List.map id l = l
@[simp]
theorem List.map_id' {α : Type u_1} (l : List α) :
List.map (fun (a : α) => a) l = l
@[simp]
theorem List.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : αβ} {l : List α} :
b List.map f l ∃ (a : α), a l f a = b
theorem List.mem_map_of_mem {α : Type u_1} {β : Type u_2} {a : α} {l : List α} (f : αβ) (h : a l) :
f a List.map f l
@[simp]
theorem List.map_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (g : βγ) (f : αβ) (l : List α) :
List.map g (List.map f l) = List.map (g f) l

### bind #

@[simp]
theorem List.nil_bind {α : Type u_1} {β : Type u_2} (f : αList β) :
[].bind f = []
@[simp]
theorem List.cons_bind {α : Type u_1} {β : Type u_2} (x : α) (xs : List α) (f : αList β) :
(x :: xs).bind f = f x ++ xs.bind f
@[simp]
theorem List.append_bind {α : Type u_1} {β : Type u_2} (xs : List α) (ys : List α) (f : αList β) :
(xs ++ ys).bind f = xs.bind f ++ ys.bind f
@[simp]
theorem List.bind_id {α : Type u_1} (l : List (List α)) :
l.bind id = l.join

### join #

@[simp]
theorem List.join_nil {α : Type u_1} :
[].join = []
@[simp]
theorem List.join_cons :
∀ {α : Type u_1} {l : List α} {ls : List (List α)}, (l :: ls).join = l ++ ls.join

### bounded quantifiers over Lists #

theorem List.forall_mem_cons {α : Type u_1} {p : αProp} {a : α} {l : List α} :
(∀ (x : α), x a :: lp x) p a ∀ (x : α), x lp x

### reverse #

@[simp]
theorem List.reverseAux_nil :
∀ {α : Type u_1} {r : List α}, [].reverseAux r = r
@[simp]
theorem List.reverseAux_cons :
∀ {α : Type u_1} {a : α} {l r : List α}, (a :: l).reverseAux r = l.reverseAux (a :: r)
theorem List.reverseAux_eq {α : Type u_1} (as : List α) (bs : List α) :
as.reverseAux bs = as.reverse ++ bs
theorem List.reverse_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) :
(List.map f l).reverse = List.map f l.reverse
@[simp]
theorem List.reverse_eq_nil_iff {α : Type u_1} {xs : List α} :
xs.reverse = [] xs = []

### nth element #

theorem List.get_of_mem {α : Type u_1} {a : α} {l : List α} :
a l∃ (n : Fin l.length), l.get n = a
theorem List.get_mem {α : Type u_1} (l : List α) (n : Nat) (h : n < l.length) :
l.get n, h l
theorem List.mem_iff_get {α : Type u_1} {a : α} {l : List α} :
a l ∃ (n : Fin l.length), l.get n = a
theorem List.get?_len_le {α : Type u_1} {l : List α} {n : Nat} :
l.length nl.get? n = none
theorem List.get?_eq_get {α : Type u_1} {l : List α} {n : Nat} (h : n < l.length) :
l.get? n = some (l.get n, h)
theorem List.get?_eq_some :
∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, l.get? n = some a ∃ (h : n < l.length), l.get n, h = a
@[simp]
theorem List.get?_eq_none :
∀ {α : Type u_1} {l : List α} {n : Nat}, l.get? n = none l.length n
@[simp]
theorem List.get?_map {α : Type u_1} {β : Type u_2} (f : αβ) (l : List α) (n : Nat) :
(List.map f l).get? n = Option.map f (l.get? n)
theorem List.get?_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < l₁.length) :
(l₁ ++ l₂).get? n = l₁.get? n
@[simp]
theorem List.get?_concat_length {α : Type u_1} (l : List α) (a : α) :
(l ++ [a]).get? l.length = some a
theorem List.getLast_eq_get {α : Type u_1} (l : List α) (h : l []) :
l.getLast h = l.get l.length - 1,
@[simp]
theorem List.getLast?_nil {α : Type u_1} :
[].getLast? = none
theorem List.getLast?_eq_getLast {α : Type u_1} (l : List α) (h : l []) :
l.getLast? = some (l.getLast h)
theorem List.getLast?_eq_get? {α : Type u_1} (l : List α) :
l.getLast? = l.get? (l.length - 1)
@[simp]
theorem List.getLast?_concat {α : Type u_1} {a : α} (l : List α) :
(l ++ [a]).getLast? = some a
theorem List.getD_eq_get? {α : Type u_1} (l : List α) (n : Nat) (a : α) :
l.getD n a = (l.get? n).getD a
theorem List.get?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} :
l₁.length n(l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
theorem List.get?_reverse' {α : Type u_1} {l : List α} (i : Nat) (j : Nat) :
i + j + 1 = l.lengthl.reverse.get? i = l.get? j
theorem List.get?_reverse {α : Type u_1} {l : List α} (i : Nat) (h : i < l.length) :
l.reverse.get? i = l.get? (l.length - 1 - i)
@[simp]
theorem List.getD_nil {n : Nat} :
∀ {α : Type u_1} {d : α}, [].getD n d = d
@[simp]
theorem List.getD_cons_zero :
∀ {α : Type u_1} {x : α} {xs : List α} {d : α}, (x :: xs).getD 0 d = x
@[simp]
theorem List.getD_cons_succ :
∀ {α : Type u_1} {x : α} {xs : List α} {n : Nat} {d : α}, (x :: xs).getD (n + 1) d = xs.getD n d
theorem List.ext_get {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : l₁.length = l₂.length) (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get n, h₁ = l₂.get n, h₂) :
l₁ = l₂
@[simp]
theorem List.get_map {α : Type u_1} {β : Type u_2} (f : αβ) {l : List α} {n : Fin (List.map f l).length} :
(List.map f l).get n = f (l.get n, )

### take and drop #

@[simp]
theorem List.take_append_drop {α : Type u_1} (n : Nat) (l : List α) :
++ = l
@[simp]
theorem List.length_drop {α : Type u_1} (i : Nat) (l : List α) :
().length = l.length - i
theorem List.drop_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length i) :
= []
theorem List.take_length_le {α : Type u_1} {i : Nat} {l : List α} (h : l.length i) :
= l
@[simp]
theorem List.take_zero {α : Type u_1} (l : List α) :
= []
@[simp]
theorem List.take_nil {α : Type u_1} {i : Nat} :
List.take i [] = []
@[simp]
theorem List.take_cons_succ :
∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as
@[simp]
theorem List.drop_zero {α : Type u_1} (l : List α) :
= l
@[simp]
theorem List.drop_succ_cons :
∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, List.drop (n + 1) (a :: l) =
@[simp]
theorem List.drop_length {α : Type u_1} (l : List α) :
List.drop l.length l = []
@[simp]
theorem List.take_length {α : Type u_1} (l : List α) :
List.take l.length l = l
theorem List.take_concat_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) :
().concat l[i] = List.take (i + 1) l
theorem List.reverse_concat {α : Type u_1} (l : List α) (a : α) :
(l.concat a).reverse = a :: l.reverse

### takeWhile and dropWhile #

@[simp]
theorem List.dropWhile_nil {α : Type u_1} {p : αBool} :
= []
theorem List.dropWhile_cons {α : Type u_1} {x : α} {xs : List α} {p : αBool} :
List.dropWhile p (x :: xs) = if p x = true then else x :: xs

### foldlM and foldrM #

@[simp]
theorem List.foldlM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (l : List α) (f : βαm β) (b : β) :
List.foldlM f b l.reverse = List.foldrM (fun (x : α) (y : β) => f y x) b l
@[simp]
theorem List.foldlM_nil {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [] (f : βαm β) (b : β) :
List.foldlM f b [] = pure b
@[simp]
theorem List.foldlM_cons {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [] (f : βαm β) (b : β) (a : α) (l : List α) :
List.foldlM f b (a :: l) = do let initf b a List.foldlM f init l
@[simp]
theorem List.foldlM_append {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [] [] (f : βαm β) (b : β) (l : List α) (l' : List α) :
List.foldlM f b (l ++ l') = do let initList.foldlM f b l List.foldlM f init l'
@[simp]
theorem List.foldrM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αβm β) (b : β) :
List.foldrM f b [] = pure b
@[simp]
theorem List.foldrM_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (a : α) (l : List α) (f : αβm β) (b : β) :
List.foldrM f b (a :: l) = List.foldrM f b l >>= f a
@[simp]
theorem List.foldrM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (l : List α) (f : αβm β) (b : β) :
List.foldrM f b l.reverse = List.foldlM (fun (x : β) (y : α) => f y x) b l
theorem List.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} (f : βαβ) (b : β) (l : List α) :
theorem List.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (l : List α) :

### foldl and foldr #

@[simp]
theorem List.foldl_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : βαβ) (b : β) :
List.foldl f b l.reverse = List.foldr (fun (x : α) (y : β) => f y x) b l
@[simp]
theorem List.foldr_reverse {α : Type u_1} {β : Type u_2} (l : List α) (f : αββ) (b : β) :
List.foldr f b l.reverse = List.foldl (fun (x : β) (y : α) => f y x) b l
@[simp]
theorem List.foldrM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αβm β) (b : β) (l : List α) (l' : List α) :
List.foldrM f b (l ++ l') = do let initList.foldrM f b l' List.foldrM f init l
@[simp]
theorem List.foldl_append {α : Type u_1} {β : Type u_2} (f : βαβ) (b : β) (l : List α) (l' : List α) :
List.foldl f b (l ++ l') = List.foldl f (List.foldl f b l) l'
@[simp]
theorem List.foldr_append {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (l : List α) (l' : List α) :
List.foldr f b (l ++ l') = List.foldr f (List.foldr f b l') l
@[simp]
theorem List.foldl_nil :
∀ {α : Type u_1} {β : Type u_2} {f : αβα} {b : α}, List.foldl f b [] = b
@[simp]
theorem List.foldl_cons {α : Type u_1} {β : Type u_2} {a : α} {f : βαβ} (l : List α) (b : β) :
List.foldl f b (a :: l) = List.foldl f (f b a) l
@[simp]
theorem List.foldr_nil :
∀ {α : Type u_1} {α_1 : Type u_2} {f : αα_1α_1} {b : α_1}, List.foldr f b [] = b
@[simp]
theorem List.foldr_cons {α : Type u_1} {a : α} :
∀ {α_1 : Type u_2} {f : αα_1α_1} {b : α_1} (l : List α), List.foldr f b (a :: l) = f a (List.foldr f b l)
@[simp]
theorem List.foldr_self_append {α : Type u_1} {l' : List α} (l : List α) :
List.foldr List.cons l' l = l ++ l'
theorem List.foldr_self {α : Type u_1} (l : List α) :
List.foldr List.cons [] l = l
theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁β₂) (g : αβ₂α) (l : List β₁) (init : α) :
List.foldl g init (List.map f l) = List.foldl (fun (x : α) (y : β₁) => g x (f y)) init l
theorem List.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁α₂) (g : α₂ββ) (l : List α₁) (init : β) :
List.foldr g init (List.map f l) = List.foldr (fun (x : α₁) (y : β) => g (f x) y) init l

### mapM #

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

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

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

### forM #

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

### eraseIdx #

@[simp]
theorem List.eraseIdx_nil {α : Type u_1} {i : Nat} :
[].eraseIdx i = []
@[simp]
theorem List.eraseIdx_cons_zero :
∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).eraseIdx 0 = as
@[simp]
theorem List.eraseIdx_cons_succ :
∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i

### find? #

@[simp]
theorem List.find?_nil {α : Type u_1} {p : αBool} :
List.find? p [] = none
theorem List.find?_cons :
∀ {α : Type u_1} {a : α} {as : List α} {p : αBool}, List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as

### filter #

@[simp]
theorem List.filter_nil {α : Type u_1} (p : αBool) :
List.filter p [] = []
@[simp]
theorem List.filter_cons_of_pos {α : Type u_1} {p : αBool} {a : α} (l : List α) (pa : p a = true) :
List.filter p (a :: l) = a ::
@[simp]
theorem List.filter_cons_of_neg {α : Type u_1} {p : αBool} {a : α} (l : List α) (pa : ¬p a = true) :
List.filter p (a :: l) =
theorem List.filter_cons {α : Type u_1} {x : α} {xs : List α} {p : αBool} :
List.filter p (x :: xs) = if p x = true then x :: List.filter p xs else List.filter p xs
theorem List.mem_filter :
∀ {α : Type u_1} {x : α} {p : αBool} {as : List α}, x List.filter p as x as p x = true
theorem List.filter_eq_nil :
∀ {α : Type u_1} {p : αBool} {l : List α}, = [] ∀ (a : α), a l¬p a = true

### findSome? #

@[simp]
theorem List.findSome?_nil {α : Type u_1} :
∀ {α_1 : Type u_2} {f : αOption α_1}, = none
theorem List.findSome?_cons {α : Type u_1} {β : Type u_2} {a : α} {as : List α} {f : α} :
List.findSome? f (a :: as) = match f a with | some b => some b | none =>

### replace #

@[simp]
theorem List.replace_nil {α : Type u_1} {a : α} {b : α} [BEq α] :
[].replace a b = []
theorem List.replace_cons {α : Type u_1} {as : List α} {b : α} {c : α} [BEq α] {a : α} :
(a :: as).replace b c = match a == b with | true => c :: as | false => a :: as.replace b c
@[simp]
theorem List.replace_cons_self {α : Type u_1} {as : List α} {b : α} [BEq α] [] {a : α} :
(a :: as).replace a b = b :: as

### elem #

@[simp]
theorem List.elem_nil {α : Type u_1} {a : α} [BEq α] :
theorem List.elem_cons {α : Type u_1} {as : List α} {b : α} [BEq α] {a : α} :
List.elem b (a :: as) = match b == a with | true => true | false => List.elem b as
@[simp]
theorem List.elem_cons_self {α : Type u_1} {as : List α} [BEq α] [] {a : α} :
List.elem a (a :: as) = true

### lookup #

@[simp]
theorem List.lookup_nil {α : Type u_1} {β : Type u_2} {a : α} [BEq α] :
List.lookup a [] = none
theorem List.lookup_cons {α : Type u_1} :
∀ {β : Type u_2} {b : β} {es : List (α × β)} {a : α} [inst : BEq α] {k : α}, List.lookup a ((k, b) :: es) = match a == k with | true => some b | false => List.lookup a es
@[simp]
theorem List.lookup_cons_self {α : Type u_1} :
∀ {β : Type u_2} {b : β} {es : List (α × β)} [inst : BEq α] [inst_1 : ] {k : α}, List.lookup k ((k, b) :: es) = some b

### zipWith #

@[simp]
theorem List.zipWith_nil_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List β} {f : αβγ} :
List.zipWith f [] l = []
@[simp]
theorem List.zipWith_nil_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : αβγ} :
List.zipWith f l [] = []
@[simp]
theorem List.zipWith_cons_cons {α : Type u_1} {β : Type u_2} {γ : Type u_3} {a : α} {as : List α} {b : β} {bs : List β} {f : αβγ} :
List.zipWith f (a :: as) (b :: bs) = f a b :: List.zipWith f as bs
theorem List.zipWith_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : αβγ} :
(List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | x, x_1 => none

### zipWithAll #

theorem List.zipWithAll_get? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {i : Nat} {f : γ} :
(List.zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => none | a?, b? => some (f a? b?)

### zip #

@[simp]
theorem List.zip_nil_left {α : Type u_1} {β : Type u_2} {l : List β} :
[].zip l = []
@[simp]
theorem List.zip_nil_right {α : Type u_1} {l : List α} {β : Type u_2} :
l.zip [] = []
@[simp]
theorem List.zip_cons_cons :
∀ {α : Type u_1} {a : α} {as : List α} {α_1 : Type u_2} {b : α_1} {bs : List α_1}, (a :: as).zip (b :: bs) = (a, b) :: as.zip bs

### unzip #

@[simp]
theorem List.unzip_nil {α : Type u_1} {β : Type u_2} :
[].unzip = ([], [])
@[simp]
theorem List.unzip_cons {α : Type u_1} {β : Type u_2} {t : List (α × β)} {h : α × β} :
(h :: t).unzip = match t.unzip with | (al, bl) => (h.fst :: al, h.snd :: bl)

### all / any #

@[simp]
theorem List.all_eq_true {α : Type u_1} {p : αBool} {l : List α} :
l.all p = true ∀ (x : α), x lp x = true
@[simp]
theorem List.any_eq_true {α : Type u_1} {p : αBool} {l : List α} :
l.any p = true ∃ (x : α), x l p x = true

### enumFrom #

@[simp]
theorem List.enumFrom_nil {α : Type u_1} {i : Nat} :
= []
@[simp]
theorem List.enumFrom_cons :
∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.enumFrom i (a :: as) = (i, a) :: List.enumFrom (i + 1) as

### iota #

@[simp]
theorem List.iota_zero :
= []
@[simp]
theorem List.iota_succ {i : Nat} :
List.iota (i + 1) = (i + 1) ::

### intersperse #

@[simp]
theorem List.intersperse_nil {α : Type u_1} (sep : α) :
@[simp]
theorem List.intersperse_single {α : Type u_1} {x : α} (sep : α) :
List.intersperse sep [x] = [x]
@[simp]
theorem List.intersperse_cons₂ {α : Type u_1} {x : α} {y : α} {zs : List α} (sep : α) :
List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)

### isPrefixOf #

@[simp]
theorem List.isPrefixOf_nil_left {α : Type u_1} {l : List α} [BEq α] :
[].isPrefixOf l = true
@[simp]
theorem List.isPrefixOf_cons_nil {α : Type u_1} {a : α} {as : List α} [BEq α] :
(a :: as).isPrefixOf [] = false
theorem List.isPrefixOf_cons₂ {α : Type u_1} {as : List α} {b : α} {bs : List α} [BEq α] {a : α} :
(a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)
@[simp]
theorem List.isPrefixOf_cons₂_self {α : Type u_1} {as : List α} {bs : List α} [BEq α] [] {a : α} :
(a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs

### isEqv #

@[simp]
theorem List.isEqv_nil_nil {α : Type u_1} {eqv : ααBool} :
[].isEqv [] eqv = true
@[simp]
theorem List.isEqv_nil_cons {α : Type u_1} {a : α} {as : List α} {eqv : ααBool} :
[].isEqv (a :: as) eqv = false
@[simp]
theorem List.isEqv_cons_nil {α : Type u_1} {a : α} {as : List α} {eqv : ααBool} :
(a :: as).isEqv [] eqv = false
theorem List.isEqv_cons₂ :
∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : ααBool}, (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)

### dropLast #

@[simp]
theorem List.dropLast_nil {α : Type u_1} :
[].dropLast = []
@[simp]
theorem List.dropLast_single :
∀ {α : Type u_1} {x : α}, [x].dropLast = []
@[simp]
theorem List.dropLast_cons₂ :
∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast

### minimum? #

@[simp]
theorem List.minimum?_nil {α : Type u_1} [Min α] :
[].minimum? = none
theorem List.minimum?_cons {α : Type u_1} {x : α} [Min α] {xs : List α} :
(x :: xs).minimum? = some (List.foldl min x xs)
@[simp]
theorem List.minimum?_eq_none_iff {α : Type u_1} {xs : List α} [Min α] :
xs.minimum? = none xs = []
theorem List.minimum?_mem {α : Type u_1} {a : α} [Min α] (min_eq_or : ∀ (a b : α), min a b = a min a b = b) {xs : List α} :
xs.minimum? = some aa xs
theorem List.le_minimum?_iff {α : Type u_1} {a : α} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a min b c a b a c) {xs : List α} :
xs.minimum? = some a∀ (x : α), x a ∀ (b : α), b xsx b
theorem List.minimum?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] [anti : Antisymm fun (x x_1 : α) => x x_1] (le_refl : ∀ (a : α), a a) (min_eq_or : ∀ (a b : α), min a b = a min a b = b) (le_min_iff : ∀ (a b c : α), a min b c a b a c) {xs : List α} :
xs.minimum? = some a a xs ∀ (b : α), b xsa b
@[simp]
theorem List.get_cons_succ {α : Type u_1} {i : Nat} {a : α} {as : List α} {h : i + 1 < (a :: as).length} :
(a :: as).get i + 1, h = as.get i,
@[simp]
theorem List.get_cons_succ' {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} :
(a :: as).get i.succ = as.get i
@[simp]
theorem List.set_nil {α : Type u_1} (n : Nat) (a : α) :
[].set n a = []
@[simp]
theorem List.set_zero {α : Type u_1} (x : α) (xs : List α) (a : α) :
(x :: xs).set 0 a = a :: xs
@[simp]
theorem List.set_succ {α : Type u_1} (x : α) (xs : List α) (n : Nat) (a : α) :
(x :: xs).set n.succ a = x :: xs.set n a
@[simp]
theorem List.get_set_eq {α : Type u_1} (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
(l.set i a).get i, h = a
@[simp]
theorem List.get_set_ne {α : Type u_1} (l : List α) {i : Nat} {j : Nat} (h : i j) (a : α) (hj : j < (l.set i a).length) :
(l.set i a).get j, hj = l.get j,