Documentation

Std.Data.List.Lemmas

Basic properties of Lists #

theorem List.cons_ne_nil {α : Type u_1} (a : α) (l : List α) :
a :: l []
theorem List.cons_ne_self {α : Type u_1} (a : α) (l : List α) :
a :: l l
theorem List.head_eq_of_cons_eq :
∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂h₁ = h₂
theorem List.tail_eq_of_cons_eq :
∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂t₁ = t₂
theorem List.cons_inj {α : Type u_1} (a : α) {l : List α} {l' : List α} :
a :: l = a :: l' l = l'
theorem List.cons_eq_cons {α : Type u_1} {a : α} {b : α} {l : List α} {l' : List α} :
a :: l = b :: l' a = b l = l'
theorem List.exists_cons_of_ne_nil {α : Type u_1} {l : List α} :
l []∃ (b : α), ∃ (L : List α), l = b :: L

length #

@[simp]
theorem List.length_singleton {α : Type u_1} (a : α) :
theorem List.length_pos_of_mem {α : Type u_1} {a : α} {l : List α} :
a l0 < List.length l
theorem List.exists_mem_of_length_pos {α : Type u_1} {l : List α} :
0 < List.length l∃ (a : α), a l
theorem List.length_pos_iff_exists_mem {α : Type u_1} {l : List α} :
0 < List.length l ∃ (a : α), a l
theorem List.exists_cons_of_length_pos {α : Type u_1} {l : List α} :
0 < List.length l∃ (h : α), ∃ (t : List α), l = h :: t
theorem List.length_pos_iff_exists_cons {α : Type u_1} {l : List α} :
0 < List.length l ∃ (h : α), ∃ (t : List α), l = h :: t
theorem List.exists_cons_of_length_succ {α : Type u_1} {n : Nat} {l : List α} :
List.length l = n + 1∃ (h : α), ∃ (t : List α), l = h :: t
theorem List.length_pos {α : Type u_1} {l : List α} :
0 < List.length l l []
theorem List.exists_mem_of_ne_nil {α : Type u_1} (l : List α) (h : l []) :
∃ (x : α), x l
theorem List.length_eq_one {α : Type u_1} {l : List α} :
List.length l = 1 ∃ (a : α), l = [a]

mem #

theorem List.mem_nil_iff {α : Type u_1} (a : α) :
@[simp]
theorem List.mem_toArray {α : Type u_1} {a : α} {l : List α} :
theorem List.mem_singleton_self {α : Type u_1} (a : α) :
a [a]
theorem List.eq_of_mem_singleton :
∀ {α : Type u_1} {a b : α}, a [b]a = b
@[simp]
theorem List.mem_singleton {α : Type u_1} {a : α} {b : α} :
a [b] a = b
theorem List.mem_of_mem_cons_of_mem {α : Type u_1} {a : α} {b : α} {l : List α} :
a b :: lb la l
theorem List.eq_or_ne_mem_of_mem {α : Type u_1} {a : α} {b : α} {l : List α} (h' : a b :: l) :
a = b a b a l
theorem List.ne_nil_of_mem {α : Type u_1} {a : α} {l : List α} (h : a l) :
l []
theorem List.append_of_mem {α : Type u_1} {a : α} {l : List α} :
a l∃ (s : List α), ∃ (t : List α), l = s ++ a :: t
@[simp]
theorem List.elem_iff {α : Type u_1} :
∀ {x : DecidableEq α} {a : α} {as : List α}, List.elem a as = true a as
theorem List.mem_of_ne_of_mem {α : Type u_1} {a : α} {y : α} {l : List α} (h₁ : a y) (h₂ : a y :: l) :
a l
theorem List.ne_of_not_mem_cons {α : Type u_1} {a : α} {b : α} {l : List α} :
¬a b :: la b
theorem List.not_mem_of_not_mem_cons {α : Type u_1} {a : α} {b : α} {l : List α} :
¬a b :: l¬a l
theorem List.not_mem_cons_of_ne_of_not_mem {α : Type u_1} {a : α} {y : α} {l : List α} :
a y¬a l¬a y :: l
theorem List.ne_and_not_mem_of_not_mem_cons {α : Type u_1} {a : α} {y : α} {l : List α} :
¬a y :: la y ¬a l

drop #

@[simp]
theorem List.drop_one {α : Type u_1} (l : List α) :
theorem List.drop_add {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :
List.drop (m + n) l = List.drop m (List.drop n l)
@[simp]
theorem List.drop_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
List.drop (List.length l₁) (l₁ ++ l₂) = l₂
theorem List.drop_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : List.length l₁ = n) :
List.drop n (l₁ ++ l₂) = l₂

isEmpty #

@[simp]
theorem List.isEmpty_nil {α : Type u_1} :
@[simp]
theorem List.isEmpty_cons {α : Type u_1} {x : α} {xs : List α} :

append #

theorem List.append_eq_append :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.append l₁ l₂ = l₁ ++ l₂
theorem List.append_ne_nil_of_ne_nil_left {α : Type u_1} (s : List α) (t : List α) :
s []s ++ t []
theorem List.append_ne_nil_of_ne_nil_right {α : Type u_1} (s : List α) (t : List α) :
t []s ++ t []
@[simp]
theorem List.nil_eq_append :
∀ {α : Type u_1} {a b : List α}, [] = a ++ b a = [] b = []
theorem List.append_ne_nil_of_left_ne_nil {α : Type u_1} (a : List α) (b : List α) (h0 : a []) :
a ++ b []
theorem List.append_eq_cons :
∀ {α : Type u_1} {a b : List α} {x : α} {c : List α}, a ++ b = x :: c a = [] b = x :: c ∃ (a' : List α), a = x :: a' c = a' ++ b
theorem List.cons_eq_append :
∀ {α : Type u_1} {x : α} {c a b : List α}, x :: c = a ++ b a = [] b = x :: c ∃ (a' : List α), a = x :: a' c = a' ++ b
theorem List.append_eq_append_iff {α : Type u_1} {a : List α} {b : List α} {c : List α} {d : List α} :
a ++ b = c ++ d (∃ (a' : List α), c = a ++ a' b = a' ++ d) ∃ (c' : List α), a = c ++ c' d = c' ++ b
@[simp]
theorem List.mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} :
a s ++ t a s a t
theorem List.not_mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} (h₁ : ¬a s) (h₂ : ¬a t) :
¬a s ++ t
theorem List.mem_append_eq {α : Type u_1} (a : α) (s : List α) (t : List α) :
(a s ++ t) = (a s a t)
theorem List.mem_append_left {α : Type u_1} {a : α} {l₁ : List α} (l₂ : List α) (h : a l₁) :
a l₁ ++ l₂
theorem List.mem_append_right {α : Type u_1} {a : α} (l₁ : List α) {l₂ : List α} (h : a l₂) :
a l₁ ++ l₂
theorem List.mem_iff_append {α : Type u_1} {a : α} {l : List α} :
a l ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

concat #

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

map #

theorem List.map_singleton {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
List.map f [a] = [f a]
theorem List.exists_of_mem_map :
∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {f : α_1α} {l : List α_1}, b List.map f l∃ (a : α_1), a l f a = b
theorem List.forall_mem_map_iff {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {P : βProp} :
(∀ (i : β), i List.map f lP i) ∀ (j : α), j lP (f j)
@[simp]
theorem List.map_eq_nil {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} :
List.map f l = [] l = []

zipWith #

@[simp]
theorem List.length_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (l₁ : List α) (l₂ : List β) :
List.length (List.zipWith f l₁ l₂) = min (List.length l₁) (List.length l₂)
@[simp]
theorem List.zipWith_map {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {μ : Type u_5} (f : γδμ) (g : αγ) (h : βδ) (l₁ : List α) (l₂ : List β) :
List.zipWith f (List.map g l₁) (List.map h l₂) = List.zipWith (fun (a : α) (b : β) => f (g a) (h b)) l₁ l₂
theorem List.zipWith_map_left {α : Type u_1} {β : Type u_2} {α' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : αα') (g : α'βγ) :
List.zipWith g (List.map f l₁) l₂ = List.zipWith (fun (a : α) (b : β) => g (f a) b) l₁ l₂
theorem List.zipWith_map_right {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} (l₁ : List α) (l₂ : List β) (f : ββ') (g : αβ'γ) :
List.zipWith g l₁ (List.map f l₂) = List.zipWith (fun (a : α) (b : β) => g a (f b)) l₁ l₂
theorem List.zipWith_foldr_eq_zip_foldr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : γδδ} {f : αβγ} (i : δ) :
List.foldr g i (List.zipWith f l₁ l₂) = List.foldr (fun (p : α × β) (r : δ) => g (f p.fst p.snd) r) i (List.zip l₁ l₂)
theorem List.zipWith_foldl_eq_zip_foldl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {l₁ : List α} {l₂ : List β} {g : δγδ} {f : αβγ} (i : δ) :
List.foldl g i (List.zipWith f l₁ l₂) = List.foldl (fun (r : δ) (p : α × β) => g r (f p.fst p.snd)) i (List.zip l₁ l₂)
@[simp]
theorem List.zipWith_eq_nil_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {l : List α} {l' : List β} :
List.zipWith f l l' = [] l = [] l' = []
theorem List.map_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδα) (l : List γ) (l' : List δ) :
List.map f (List.zipWith g l l') = List.zipWith (fun (x : γ) (y : δ) => f (g x y)) l l'
theorem List.zipWith_distrib_take :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.take n (List.zipWith f l l') = List.zipWith f (List.take n l) (List.take n l')
theorem List.zipWith_distrib_drop :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1} {n : Nat}, List.drop n (List.zipWith f l l') = List.zipWith f (List.drop n l) (List.drop n l')
theorem List.zipWith_distrib_tail :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1}, List.tail (List.zipWith f l l') = List.zipWith f (List.tail l) (List.tail l')
theorem List.zipWith_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (l : List α) (la : List α) (l' : List β) (lb : List β) (h : List.length l = List.length l') :
List.zipWith f (l ++ la) (l' ++ lb) = List.zipWith f l l' ++ List.zipWith f la lb

zip #

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

join #

theorem List.mem_join {α : Type u_1} {a : α} {L : List (List α)} :
a List.join L ∃ (l : List α), l L a l
theorem List.exists_of_mem_join :
∀ {α : Type u_1} {a : α} {L : List (List α)}, a List.join L∃ (l : List α), l L a l
theorem List.mem_join_of_mem :
∀ {α : Type u_1} {l : List α} {L : List (List α)} {a : α}, l La la List.join L

bind #

theorem List.mem_bind {α : Type u_1} {β : Type u_2} {f : αList β} {b : β} {l : List α} :
b List.bind l f ∃ (a : α), a l b f a
theorem List.exists_of_mem_bind {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : αList β} :
b List.bind l f∃ (a : α), a l b f a
theorem List.mem_bind_of_mem {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : αList β} {a : α} (al : a l) (h : b f a) :
theorem List.bind_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : βγ) (g : αList β) (l : List α) :
List.map f (List.bind l g) = List.bind l fun (a : α) => List.map f (g a)

set-theoretic notation of Lists #

@[simp]
theorem List.empty_eq {α : Type u_1} :
= []

bounded quantifiers over Lists #

theorem List.exists_mem_nil {α : Type u_1} (p : αProp) :
¬∃ (x : α), x [] p x
theorem List.forall_mem_nil {α : Type u_1} (p : αProp) (x : α) :
x []p x
theorem List.exists_mem_cons {α : Type u_1} {p : αProp} {a : α} {l : List α} :
(∃ (x : α), x a :: l p x) p a ∃ (x : α), x l p x
theorem List.forall_mem_singleton {α : Type u_1} {p : αProp} {a : α} :
(∀ (x : α), x [a]p x) p a
theorem List.forall_mem_append {α : Type u_1} {p : αProp} {l₁ : List α} {l₂ : List α} :
(∀ (x : α), x l₁ ++ l₂p x) (∀ (x : α), x l₁p x) ∀ (x : α), x l₂p x

List subset #

theorem List.subset_def {α : Type u_1} {l₁ : List α} {l₂ : List α} :
l₁ l₂ ∀ {a : α}, a l₁a l₂
@[simp]
theorem List.nil_subset {α : Type u_1} (l : List α) :
[] l
@[simp]
theorem List.Subset.refl {α : Type u_1} (l : List α) :
l l
theorem List.Subset.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ l₂) (h₂ : l₂ l₃) :
l₁ l₃
instance List.instTransListMemInstMembershipListSubsetInstHasSubsetList {α : Type u_1} :
Trans Membership.mem Subset Membership.mem
Equations
  • List.instTransListMemInstMembershipListSubsetInstHasSubsetList = { trans := }
instance List.instTransListSubsetInstHasSubsetList {α : Type u_1} :
Trans Subset Subset Subset
Equations
  • List.instTransListSubsetInstHasSubsetList = { trans := }
@[simp]
theorem List.subset_cons {α : Type u_1} (a : α) (l : List α) :
l a :: l
theorem List.subset_of_cons_subset {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} :
a :: l₁ l₂l₁ l₂
theorem List.subset_cons_of_subset {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} :
l₁ l₂l₁ a :: l₂
theorem List.cons_subset_cons {α : Type u_1} {l₁ : List α} {l₂ : List α} (a : α) (s : l₁ l₂) :
a :: l₁ a :: l₂
@[simp]
theorem List.subset_append_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₁ l₁ ++ l₂
@[simp]
theorem List.subset_append_right {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₂ l₁ ++ l₂
theorem List.subset_append_of_subset_left {α : Type u_1} {l : List α} {l₁ : List α} (l₂ : List α) :
l l₁l l₁ ++ l₂
theorem List.subset_append_of_subset_right {α : Type u_1} {l : List α} {l₂ : List α} (l₁ : List α) :
l l₂l l₁ ++ l₂
@[simp]
theorem List.cons_subset :
∀ {α : Type u_1} {a : α} {l m : List α}, a :: l m a m l m
@[simp]
theorem List.append_subset {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} :
l₁ ++ l₂ l l₁ l l₂ l
theorem List.subset_nil {α : Type u_1} {l : List α} :
l [] l = []
theorem List.map_subset {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : αβ) (H : l₁ l₂) :
List.map f l₁ List.map f l₂

replicate #

theorem List.replicate_succ {α : Type u_1} (a : α) (n : Nat) :
theorem List.mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} :
b List.replicate n a n 0 b = a
theorem List.eq_of_mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} (h : b List.replicate n a) :
b = a
theorem List.eq_replicate_of_mem {α : Type u_1} {a : α} {l : List α} :
(∀ (b : α), b lb = a)l = List.replicate (List.length l) a
theorem List.eq_replicate {α : Type u_1} {a : α} {n : Nat} {l : List α} :
l = List.replicate n a List.length l = n ∀ (b : α), b lb = a

getLast #

theorem List.getLast_cons' {α : Type u_1} {a : α} {l : List α} (h₁ : a :: l []) (h₂ : l []) :
List.getLast (a :: l) h₁ = List.getLast l h₂
@[simp]
theorem List.getLast_append {α : Type u_1} {a : α} (l : List α) (h : l ++ [a] []) :
List.getLast (l ++ [a]) h = a
theorem List.getLast_concat :
∀ {α : Type u_1} {l : List α} {a : α} (h : List.concat l a []), List.getLast (List.concat l a) h = a
theorem List.eq_nil_or_concat {α : Type u_1} (l : List α) :
l = [] ∃ (L : List α), ∃ (b : α), l = L ++ [b]

sublists #

@[simp]
theorem List.nil_sublist {α : Type u_1} (l : List α) :
@[simp]
theorem List.Sublist.refl {α : Type u_1} (l : List α) :
theorem List.Sublist.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : List.Sublist l₁ l₂) (h₂ : List.Sublist l₂ l₃) :
List.Sublist l₁ l₃
instance List.instTransListSublist {α : Type u_1} :
Trans List.Sublist List.Sublist List.Sublist
Equations
  • List.instTransListSublist = { trans := }
@[simp]
theorem List.sublist_cons {α : Type u_1} (a : α) (l : List α) :
theorem List.sublist_of_cons_sublist :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Sublist (a :: l₁) l₂List.Sublist l₁ l₂
@[simp]
theorem List.sublist_append_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
List.Sublist l₁ (l₁ ++ l₂)
@[simp]
theorem List.sublist_append_right {α : Type u_1} (l₁ : List α) (l₂ : List α) :
List.Sublist l₂ (l₁ ++ l₂)
theorem List.sublist_append_of_sublist_left :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Sublist l l₁List.Sublist l (l₁ ++ l₂)
theorem List.sublist_append_of_sublist_right :
∀ {α : Type u_1} {l l₂ l₁ : List α}, List.Sublist l l₂List.Sublist l (l₁ ++ l₂)
theorem List.cons_sublist_cons :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Sublist (a :: l₁) (a :: l₂) List.Sublist l₁ l₂
@[simp]
theorem List.append_sublist_append_left :
∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), List.Sublist (l ++ l₁) (l ++ l₂) List.Sublist l₁ l₂
theorem List.Sublist.append_left :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂∀ (l : List α), List.Sublist (l ++ l₁) (l ++ l₂)
theorem List.Sublist.append_right :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂∀ (l : List α), List.Sublist (l₁ ++ l) (l₂ ++ l)
theorem List.sublist_or_mem_of_sublist :
∀ {α : Type u_1} {l l₁ : List α} {a : α} {l₂ : List α}, List.Sublist l (l₁ ++ a :: l₂)List.Sublist l (l₁ ++ l₂) a l
theorem List.Sublist.reverse :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂List.Sublist (List.reverse l₁) (List.reverse l₂)
@[simp]
theorem List.reverse_sublist :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist (List.reverse l₁) (List.reverse l₂) List.Sublist l₁ l₂
@[simp]
theorem List.append_sublist_append_right :
∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), List.Sublist (l₁ ++ l) (l₂ ++ l) List.Sublist l₁ l₂
theorem List.Sublist.append :
∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, List.Sublist l₁ l₂List.Sublist r₁ r₂List.Sublist (l₁ ++ r₁) (l₂ ++ r₂)
theorem List.Sublist.subset :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂l₁ l₂
instance List.instTransListSublistSubsetInstHasSubsetList {α : Type u_1} :
Trans List.Sublist Subset Subset
Equations
  • List.instTransListSublistSubsetInstHasSubsetList = { trans := }
instance List.instTransListSubsetSublistInstHasSubsetList {α : Type u_1} :
Trans Subset List.Sublist Subset
Equations
  • List.instTransListSubsetSublistInstHasSubsetList = { trans := }
instance List.instTransListMemInstMembershipListSublist {α : Type u_1} :
Trans Membership.mem List.Sublist Membership.mem
Equations
  • List.instTransListMemInstMembershipListSublist = { trans := }
theorem List.Sublist.length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂List.length l₁ List.length l₂
@[simp]
theorem List.sublist_nil {α : Type u_1} {l : List α} :
List.Sublist l [] l = []
theorem List.Sublist.eq_of_length :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂List.length l₁ = List.length l₂l₁ = l₂
theorem List.Sublist.eq_of_length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Sublist l₁ l₂List.length l₂ List.length l₁l₁ = l₂
@[simp]
theorem List.singleton_sublist {α : Type u_1} {a : α} {l : List α} :
List.Sublist [a] l a l
@[simp]
theorem List.replicate_sublist_replicate {α : Type u_1} {m : Nat} {n : Nat} (a : α) :
theorem List.isSublist_iff_sublist {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} :
List.isSublist l₁ l₂ = true List.Sublist l₁ l₂
instance List.instDecidableSublist {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
Equations
theorem List.head!_of_head? {α : Type u_1} {a : α} [Inhabited α] {l : List α} :
theorem List.head?_eq_head {α : Type u_1} (l : List α) (h : l []) :

tail #

@[simp]
theorem List.tailD_eq_tail? {α : Type u_1} (l : List α) (l' : List α) :
theorem List.tail_eq_tailD {α : Type u_1} (l : List α) :
theorem List.tail_eq_tail? {α : Type u_1} (l : List α) :

next? #

@[simp]
theorem List.next?_nil {α : Type u_1} :
List.next? [] = none
@[simp]
theorem List.next?_cons {α : Type u_1} (a : α) (l : List α) :
List.next? (a :: l) = some (a, l)

getLast #

@[simp]
theorem List.getLastD_nil {α : Type u_1} (a : α) :
@[simp]
theorem List.getLastD_cons {α : Type u_1} (a : α) (b : α) (l : List α) :
theorem List.getLast_eq_getLastD {α : Type u_1} (a : α) (l : List α) (h : a :: l []) :
theorem List.getLastD_eq_getLast? {α : Type u_1} (a : α) (l : List α) :
@[simp]
theorem List.getLast_singleton {α : Type u_1} (a : α) (h : [a] []) :
List.getLast [a] h = a
theorem List.getLast!_cons {α : Type u_1} {a : α} {l : List α} [Inhabited α] :
theorem List.getLast?_cons {α : Type u_1} {a : α} {l : List α} :
@[simp]
theorem List.getLast?_singleton {α : Type u_1} (a : α) :
theorem List.getLast_mem {α : Type u_1} {l : List α} (h : l []) :
theorem List.getLastD_mem_cons {α : Type u_1} (l : List α) (a : α) :

dropLast #

NB: dropLast is the specification for Array.pop, so theorems about List.dropLast are often used for theorems about Array.pop.

theorem List.dropLast_cons_of_ne_nil {α : Type u} {x : α} {l : List α} (h : l []) :
@[simp]
theorem List.dropLast_append_of_ne_nil {α : Type u} {l : List α} (l' : List α) :
l []List.dropLast (l' ++ l) = l' ++ List.dropLast l
theorem List.dropLast_append_cons :
∀ {α : Type u_1} {l₁ : List α} {b : α} {l₂ : List α}, List.dropLast (l₁ ++ b :: l₂) = l₁ ++ List.dropLast (b :: l₂)
@[simp]
theorem List.dropLast_concat :
∀ {α : Type u_1} {l₁ : List α} {b : α}, List.dropLast (l₁ ++ [b]) = l₁
@[simp]
theorem List.length_dropLast {α : Type u_1} (xs : List α) :
@[simp]
theorem List.get_dropLast {α : Type u_1} (xs : List α) (i : Fin (List.length (List.dropLast xs))) :
List.get (List.dropLast xs) i = List.get xs { val := i, isLt := }

nth element #

@[simp]
theorem List.get_cons_cons_one :
∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, List.get (a₁ :: a₂ :: as) 1 = a₂
theorem List.get!_cons_succ {α : Type u_1} [Inhabited α] (l : List α) (a : α) (n : Nat) :
List.get! (a :: l) (n + 1) = List.get! l n
theorem List.get!_cons_zero {α : Type u_1} [Inhabited α] (l : List α) (a : α) :
List.get! (a :: l) 0 = a
theorem List.get!_nil {α : Type u_1} [Inhabited α] (n : Nat) :
List.get! [] n = default
theorem List.get!_len_le {α : Type u_1} [Inhabited α] {l : List α} {n : Nat} :
List.length l nList.get! l n = default
theorem List.get?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a l) :
∃ (n : Nat), List.get? l n = some a
theorem List.get?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : List.get? l n = some a) :
a l
theorem List.Fin.exists_iff {n : Nat} (p : Fin nProp) :
(∃ (i : Fin n), p i) ∃ (i : Nat), ∃ (h : i < n), p { val := i, isLt := h }
theorem List.mem_iff_get? {α : Type u_1} {a : α} {l : List α} :
a l ∃ (n : Nat), List.get? l n = some a
theorem List.get?_zero {α : Type u_1} (l : List α) :
@[simp]
theorem List.getElem_eq_get {α : Type u_1} (l : List α) (i : Nat) (h : i < List.length l) :
l[i] = List.get l { val := i, isLt := h }
@[simp]
theorem List.getElem?_eq_get? {α : Type u_1} (l : List α) (i : Nat) :
l[i]? = List.get? l i
theorem List.get?_inj {i : Nat} :
∀ {α : Type u_1} {xs : List α} {j : Nat}, i < List.length xsList.Nodup xsList.get? xs i = List.get? xs ji = j
@[simp]
theorem List.get_map {α : Type u_1} {β : Type u_2} (f : αβ) {l : List α} {n : Fin (List.length (List.map f l))} :
List.get (List.map f l) n = f (List.get l { val := n, isLt := })
theorem List.get_of_eq {α : Type u_1} {l : List α} {l' : List α} (h : l = l') (i : Fin (List.length l)) :
List.get l i = List.get l' { val := i, isLt := }

If one has get 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 theorem get_of_eq can be used to make such a rewrite, with rw (get_of_eq h).

@[simp]
theorem List.get_singleton {α : Type u_1} (a : α) (n : Fin 1) :
List.get [a] n = a
theorem List.get_zero {α : Type u_1} {l : List α} (h : 0 < List.length l) :
some (List.get l { val := 0, isLt := h }) = List.head? l
theorem List.get_append_right_aux {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : List.length l₁ n) (h₂ : n < List.length (l₁ ++ l₂)) :
theorem List.get_append_right' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : List.length l₁ n) (h₂ : n < List.length (l₁ ++ l₂)) :
List.get (l₁ ++ l₂) { val := n, isLt := h₂ } = List.get l₂ { val := n - List.length l₁, isLt := }
theorem List.get_of_append_proof {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : List.length l₁ = n) :
theorem List.get_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : List.length l₁ = n) :
List.get l { val := n, isLt := } = a
@[simp]
theorem List.get_replicate {α : Type u_1} (a : α) {n : Nat} (m : Fin (List.length (List.replicate n a))) :
@[simp]
theorem List.getLastD_concat {α : Type u_1} (a : α) (b : α) (l : List α) :
List.getLastD (l ++ [b]) a = b
theorem List.get_cons_length {α : Type u_1} (x : α) (xs : List α) (n : Nat) (h : n = List.length xs) :
List.get (x :: xs) { val := n, isLt := } = List.getLast (x :: xs)
theorem List.ext {α : Type u_1} {l₁ : List α} {l₂ : List α} :
(∀ (n : Nat), List.get? l₁ n = List.get? l₂ n)l₁ = l₂
theorem List.ext_get {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : List.length l₁ = List.length l₂) (h : ∀ (n : Nat) (h₁ : n < List.length l₁) (h₂ : n < List.length l₂), List.get l₁ { val := n, isLt := h₁ } = List.get l₂ { val := n, isLt := h₂ }) :
l₁ = l₂
theorem List.get!_of_get? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} :
List.get? l n = some aList.get! l n = a
@[simp]
theorem List.get!_eq_getD {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) :
List.get! l n = List.getD l n default

take #

theorem List.take_succ_cons :
∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as

Alias of List.take_cons_succ.

@[simp]
theorem List.length_take {α : Type u_1} (i : Nat) (l : List α) :
theorem List.length_take_le {α : Type u_1} (n : Nat) (l : List α) :
theorem List.length_take_le' {α : Type u_1} (n : Nat) (l : List α) :
theorem List.length_take_of_le {n : Nat} :
∀ {α : Type u_1} {l : List α}, n List.length lList.length (List.take n l) = n
theorem List.take_all_of_le {α : Type u_1} {n : Nat} {l : List α} :
List.length l nList.take n l = l
@[simp]
theorem List.take_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
List.take (List.length l₁) (l₁ ++ l₂) = l₁
theorem List.take_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : List.length l₁ = n) :
List.take n (l₁ ++ l₂) = l₁
theorem List.take_take {α : Type u_1} (n : Nat) (m : Nat) (l : List α) :
theorem List.take_replicate {α : Type u_1} (a : α) (n : Nat) (m : Nat) :
theorem List.map_take {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : Nat) :
theorem List.take_append_eq_append_take {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} :
List.take n (l₁ ++ l₂) = List.take n l₁ ++ List.take (n - List.length l₁) 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_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : n List.length l₁) :
List.take n (l₁ ++ l₂) = List.take n l₁
theorem List.take_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (i : Nat) :
List.take (List.length l₁ + 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_1} (L : List α) {i : Nat} {j : Nat} (hi : i < List.length L) (hj : i < j) :
List.get L { val := i, isLt := hi } = List.get (List.take j L) { val := i, isLt := }

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_1} (L : List α) {j : Nat} {i : Fin (List.length (List.take j L))} :
List.get (List.take j L) i = List.get L { val := i, isLt := }

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_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) :
@[simp]
theorem List.nth_take_of_succ {α : Type u_1} {l : List α} {n : Nat} :
List.get? (List.take (n + 1) l) n = List.get? l n
theorem List.take_succ {α : Type u_1} {l : List α} {n : Nat} :
@[simp]
theorem List.take_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} :
List.take k l = [] l = [] k = 0
theorem List.take_eq_take {α : Type u_1} {l : List α} {m : Nat} {n : Nat} :
theorem List.take_add {α : Type u_1} (l : List α) (m : Nat) (n : Nat) :
theorem List.take_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} :
as = []List.take i as = []
theorem List.ne_nil_of_take_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.take i as []) :
as []
theorem List.dropLast_take {α : Type u_1} {n : Nat} {l : List α} (h : n < List.length l) :
theorem List.map_eq_append_split {α : Type u_1} {β : Type u_2} {f : αβ} {l : List α} {s₁ : List β} {s₂ : List β} (h : List.map f l = s₁ ++ s₂) :
∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.map f l₁ = s₁ List.map f l₂ = s₂

drop #

theorem List.drop_eq_nil_iff_le {α : Type u_1} {l : List α} {k : Nat} :
theorem List.tail_drop {α : Type u_1} (l : List α) (n : Nat) :
theorem List.drop_length_cons {α : Type u_1} {l : List α} (h : l []) (a : α) :
theorem List.drop_append_eq_append_drop {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} :
List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ List.drop (n - List.length l₁) 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_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : n List.length l₁) :
List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ l₂
theorem List.drop_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (i : Nat) :
List.drop (List.length l₁ + 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_1} [SizeOf α] (l : List α) (n : Nat) :
theorem List.lt_length_drop {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (h : i + j < List.length L) :
theorem List.get_drop {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (h : i + j < List.length L) :
List.get L { val := i + j, isLt := h } = List.get (List.drop i L) { val := j, isLt := }

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_1} (L : List α) {i : Nat} {j : Fin (List.length (List.drop i L))} :
List.get (List.drop i L) j = List.get L { val := i + j, isLt := }

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_1} (L : List α) (i : Nat) (j : Nat) :
List.get? (List.drop i L) j = List.get? L (i + j)
@[simp]
theorem List.drop_drop {α : Type u_1} (n : Nat) (m : Nat) (l : List α) :
List.drop n (List.drop m l) = List.drop (n + m) l
theorem List.drop_take {α : Type u_1} (m : Nat) (n : Nat) (l : List α) :
theorem List.map_drop {α : Type u_1} {β : Type u_2} (f : αβ) (L : List α) (i : Nat) :
theorem List.reverse_take {α : Type u_1} {xs : List α} (n : Nat) (h : n List.length xs) :
theorem List.get_cons_drop {α : Type u_1} (l : List α) (i : Fin (List.length l)) :
List.get l i :: List.drop (i + 1) l = List.drop (i) l
theorem List.drop_eq_get_cons {α : Type u_1} {n : Nat} {l : List α} (h : n < List.length l) :
List.drop n l = List.get l { val := n, isLt := h } :: List.drop (n + 1) l
theorem List.drop_eq_nil_of_eq_nil {α : Type u_1} {as : List α} {i : Nat} :
as = []List.drop i as = []
theorem List.ne_nil_of_drop_ne_nil {α : Type u_1} {as : List α} {i : Nat} (h : List.drop i as []) :
as []

modify nth #

theorem List.modifyNthTail_id {α : Type u_1} (n : Nat) (l : List α) :
theorem List.removeNth_eq_nth_tail {α : Type u_1} (n : Nat) (l : List α) :
theorem List.get?_modifyNth {α : Type u_1} (f : αα) (n : Nat) (l : List α) (m : Nat) :
List.get? (List.modifyNth f n l) m = (fun (a : α) => if n = m then f a else a) <$> List.get? l m
theorem List.modifyNthTail_length {α : Type u_1} (f : List αList α) (H : ∀ (l : List α), List.length (f l) = List.length l) (n : Nat) (l : List α) :
theorem List.modifyNthTail_add {α : Type u_1} (f : List αList α) (n : Nat) (l₁ : List α) (l₂ : List α) :
List.modifyNthTail f (List.length l₁ + n) (l₁ ++ l₂) = l₁ ++ List.modifyNthTail f n l₂
theorem List.exists_of_modifyNthTail {α : Type u_1} (f : List αList α) {n : Nat} {l : List α} (h : n List.length l) :
∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ List.length l₁ = n List.modifyNthTail f n l = l₁ ++ f l₂
@[simp]
theorem List.modify_get?_length {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
@[simp]
theorem List.get?_modifyNth_eq {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
@[simp]
theorem List.get?_modifyNth_ne {α : Type u_1} (f : αα) {m : Nat} {n : Nat} (l : List α) (h : m n) :
theorem List.exists_of_modifyNth {α : Type u_1} (f : αα) {n : Nat} {l : List α} (h : n < List.length l) :
∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ List.length l₁ = n List.modifyNth f n l = l₁ ++ f a :: l₂
theorem List.modifyNthTail_eq_take_drop {α : Type u_1} (f : List αList α) (H : f [] = []) (n : Nat) (l : List α) :
theorem List.modifyNth_eq_take_drop {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
theorem List.modifyNth_eq_take_cons_drop {α : Type u_1} (f : αα) {n : Nat} {l : List α} (h : n < List.length l) :
List.modifyNth f n l = List.take n l ++ f (List.get l { val := n, isLt := h }) :: List.drop (n + 1) l

set #

theorem List.set_eq_modifyNth {α : Type u_1} (a : α) (n : Nat) (l : List α) :
List.set l n a = List.modifyNth (fun (x : α) => a) n l
theorem List.set_eq_take_cons_drop {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < List.length l) :
List.set l n a = List.take n l ++ a :: List.drop (n + 1) l
theorem List.modifyNth_eq_set_get? {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
List.modifyNth f n l = Option.getD ((fun (a : α) => List.set l n (f a)) <$> List.get? l n) l
theorem List.modifyNth_eq_set_get {α : Type u_1} (f : αα) {n : Nat} {l : List α} (h : n < List.length l) :
List.modifyNth f n l = List.set l n (f (List.get l { val := n, isLt := h }))
theorem List.exists_of_set {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < List.length l) :
∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ List.length l₁ = n List.set l n a' = l₁ ++ a' :: l₂
theorem List.exists_of_set' {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < List.length l) :
∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ List.get l { val := n, isLt := h } :: l₂ List.length l₁ = n List.set l n a' = l₁ ++ a' :: l₂
theorem List.get?_set_eq {α : Type u_1} (a : α) (n : Nat) (l : List α) :
List.get? (List.set l n a) n = (fun (x : α) => a) <$> List.get? l n
theorem List.get?_set_eq_of_lt {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < List.length l) :
List.get? (List.set l n a) n = some a
theorem List.get?_set_ne {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : m n) :
theorem List.get?_set {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) :
List.get? (List.set l m a) n = if m = n then (fun (x : α) => a) <$> List.get? l n else List.get? l n
theorem List.get?_set_of_lt {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : n < List.length l) :
List.get? (List.set l m a) n = if m = n then some a else List.get? l n
theorem List.get?_set_of_lt' {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : m < List.length l) :
List.get? (List.set l m a) n = if m = n then some a else List.get? l n
@[simp]
theorem List.set_eq_nil {α : Type u_1} (l : List α) (n : Nat) (a : α) :
List.set l n a = [] l = []
theorem List.set_comm {α : Type u_1} (a : α) (b : α) {n : Nat} {m : Nat} (l : List α) :
n mList.set (List.set l n a) m b = List.set (List.set l m b) n a
theorem List.set_set {α : Type u_1} (a : α) (b : α) (l : List α) (n : Nat) :
List.set (List.set l n a) n b = List.set l n b
theorem List.get_set {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : n < List.length (List.set l m a)) :
List.get (List.set l m a) { val := n, isLt := h } = if m = n then a else List.get l { val := n, isLt := }
theorem List.mem_or_eq_of_mem_set {α : Type u_1} {l : List α} {n : Nat} {a : α} {b : α} :
a List.set l n ba l a = b

remove nth #

theorem List.length_removeNth {α : Type u_1} {l : List α} {i : Nat} :

tail #

@[simp]
theorem List.length_tail {α : Type u_1} (l : List α) :

all / any #

@[simp]
theorem List.contains_nil {α : Type u_1} {a : α} [BEq α] :
@[simp]
theorem List.contains_cons {α : Type u_1} {a : α} {as : List α} {x : α} [BEq α] :
List.contains (a :: as) x = (x == a || List.contains as x)
theorem List.contains_eq_any_beq {α : Type u_1} [BEq α] (l : List α) (a : α) :
List.contains l a = List.any l fun (x : α) => a == x
theorem List.not_all_eq_any_not {α : Type u_1} (l : List α) (p : αBool) :
(!List.all l p) = List.any l fun (a : α) => !p a
theorem List.not_any_eq_all_not {α : Type u_1} (l : List α) (p : αBool) :
(!List.any l p) = List.all l fun (a : α) => !p a
theorem List.or_all_distrib_left {α : Type u_1} (l : List α) (p : αBool) (q : Bool) :
(q || List.all l p) = List.all l fun (a : α) => q || p a
theorem List.or_all_distrib_right {α : Type u_1} (l : List α) (p : αBool) (q : Bool) :
(List.all l p || q) = List.all l fun (a : α) => p a || q
theorem List.and_any_distrib_left {α : Type u_1} (l : List α) (p : αBool) (q : Bool) :
(q && List.any l p) = List.any l fun (a : α) => q && p a
theorem List.and_any_distrib_right {α : Type u_1} (l : List α) (p : αBool) (q : Bool) :
(List.any l p && q) = List.any l fun (a : α) => p a && q
theorem List.any_eq_not_all_not {α : Type u_1} (l : List α) (p : αBool) :
List.any l p = !List.all l fun (x : α) => !p x
theorem List.all_eq_not_any_not {α : Type u_1} (l : List α) (p : αBool) :
List.all l p = !List.any l fun (x : α) => !p x

reverse #

@[simp]
theorem List.mem_reverseAux {α : Type u_1} {x : α} {as : List α} {bs : List α} :
x List.reverseAux as bs x as x bs
@[simp]
theorem List.mem_reverse {α : Type u_1} {x : α} {as : List α} :

insert #

@[simp]
theorem List.insert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a l) :
@[simp]
theorem List.insert_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : ¬a l) :
List.insert a l = a :: l
@[simp]
theorem List.mem_insert_iff {α : Type u_1} [DecidableEq α] {a : α} {b : α} {l : List α} :
a List.insert b l a = b a l
@[simp]
theorem List.mem_insert_self {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :
theorem List.mem_insert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {b : α} {l : List α} (h : a l) :
theorem List.eq_or_mem_of_mem_insert {α : Type u_1} [DecidableEq α] {a : α} {b : α} {l : List α} (h : a List.insert b l) :
a = b a l
@[simp]
theorem List.length_insert_of_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a l) :
@[simp]
theorem List.length_insert_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : ¬a l) :

eraseP #

@[simp]
theorem List.eraseP_nil :
∀ {α : Type u_1} {p : αBool}, List.eraseP p [] = []
theorem List.eraseP_cons {α : Type u_1} {p : αBool} (a : α) (l : List α) :
List.eraseP p (a :: l) = bif p a then l else a :: List.eraseP p l
@[simp]
theorem List.eraseP_cons_of_pos {α : Type u_1} {a : α} {l : List α} (p : αBool) (h : p a = true) :
List.eraseP p (a :: l) = l
@[simp]
theorem List.eraseP_cons_of_neg {α : Type u_1} {a : α} {l : List α} (p : αBool) (h : ¬p a = true) :
List.eraseP p (a :: l) = a :: List.eraseP p l
theorem List.eraseP_of_forall_not {α : Type u_1} {p : αBool} {l : List α} (h : ∀ (a : α), a l¬p a = true) :
theorem List.exists_of_eraseP {α : Type u_1} {p : αBool} {l : List α} {a : α} (al : a l) (pa : p a = true) :
∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁¬p b = true) p a = true l = l₁ ++ a :: l₂ List.eraseP p l = l₁ ++ l₂
theorem List.exists_or_eq_self_of_eraseP {α : Type u_1} (p : αBool) (l : List α) :
List.eraseP p l = l ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁¬p b = true) p a = true l = l₁ ++ a :: l₂ List.eraseP p l = l₁ ++ l₂
@[simp]
theorem List.length_eraseP_of_mem :
∀ {α : Type u_1} {a : α} {l : List α} {p : αBool}, a lp a = trueList.length (List.eraseP p l) = Nat.pred (List.length l)
theorem List.eraseP_append_left {α : Type u_1} {p : αBool} {a : α} (pa : p a = true) {l₁ : List α} (l₂ : List α) :
a l₁List.eraseP p (l₁ ++ l₂) = List.eraseP p l₁ ++ l₂
theorem List.eraseP_append_right {α : Type u_1} {p : αBool} {l₁ : List α} (l₂ : List α) :
(∀ (b : α), b l₁¬p b = true)List.eraseP p (l₁ ++ l₂) = l₁ ++ List.eraseP p l₂
theorem List.eraseP_sublist {α : Type u_1} {p : αBool} (l : List α) :
theorem List.eraseP_subset {α : Type u_1} {p : αBool} (l : List α) :
theorem List.Sublist.eraseP :
∀ {α : Type u_1} {l₁ l₂ : List α} {p : αBool}, List.Sublist l₁ l₂List.Sublist (List.eraseP p l₁) (List.eraseP p l₂)
theorem List.mem_of_mem_eraseP {α : Type u_1} {a : α} {p : αBool} {l : List α} :
a List.eraseP p la l
@[simp]
theorem List.mem_eraseP_of_neg {α : Type u_1} {p : αBool} {a : α} {l : List α} (pa : ¬p a = true) :
theorem List.eraseP_map {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) :
@[simp]
theorem List.extractP_eq_find?_eraseP {α : Type u_1} {p : αBool} (l : List α) :
theorem List.extractP_eq_find?_eraseP.go {α : Type u_1} {p : αBool} (l : List α) (acc : Array α) (xs : List α) :
l = acc.data ++ xsList.extractP.go p l xs acc = (List.find? p xs, acc.data ++ List.eraseP p xs)

erase #

@[simp]
theorem List.erase_nil {α : Type u_1} [BEq α] (a : α) :
List.erase [] a = []
theorem List.erase_cons {α : Type u_1} [BEq α] (a : α) (b : α) (l : List α) :
List.erase (b :: l) a = if (b == a) = true then l else b :: List.erase l a
@[simp]
theorem List.erase_cons_head {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
List.erase (a :: l) a = l
@[simp]
theorem List.erase_cons_tail {α : Type u_1} [BEq α] {a : α} {b : α} (l : List α) (h : ¬(b == a) = true) :
List.erase (b :: l) a = b :: List.erase l a
theorem List.erase_eq_eraseP {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
List.erase l a = List.eraseP (fun (x : α) => a == x) l
theorem List.Sublist.erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : List.Sublist l₁ l₂) :
theorem List.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} :
¬a lList.erase l a = l
theorem List.exists_erase_eq {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a l) :
∃ (l₁ : List α), ∃ (l₂ : List α), ¬a l₁ l = l₁ ++ a :: l₂ List.erase l a = l₁ ++ l₂
@[simp]
theorem List.length_erase_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a l) :
theorem List.erase_append_left {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a l₁) :
List.erase (l₁ ++ l₂) a = List.erase l₁ a ++ l₂
theorem List.erase_append_right {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : ¬a l₁) :
List.erase (l₁ ++ l₂) a = l₁ ++ List.erase l₂ a
theorem List.erase_sublist {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
theorem List.erase_subset {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
theorem List.sublist.erase {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : List.Sublist l₁ l₂) :
theorem List.mem_of_mem_erase {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (h : a List.erase l b) :
a l
@[simp]
theorem List.mem_erase_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (ab : a b) :
a List.erase l b a l
theorem List.erase_comm {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (b : α) (l : List α) :

filter and partition #

@[simp]
theorem List.filter_append {α : Type u_1} {p : αBool} (l₁ : List α) (l₂ : List α) :
List.filter p (l₁ ++ l₂) = List.filter p l₁ ++ List.filter p l₂
@[simp]
theorem List.filter_sublist {α : Type u_1} {p : αBool} (l : List α) :
@[simp]
theorem List.partition_eq_filter_filter {α : Type u_1} (p : αBool) (l : List α) :
theorem List.partition_eq_filter_filter.aux {α : Type u_1} (p : αBool) (l : List α) {as : List α} {bs : List α} :
theorem List.filter_congr' {α : Type u_1} {p : αBool} {q : αBool} {l : List α} :
(∀ (x : α), x l(p x = true q x = true))List.filter p l = List.filter q l

filterMap #

@[simp]
theorem List.filterMap_nil {α : Type u_1} {β : Type u_2} (f : αOption β) :
@[simp]
theorem List.filterMap_cons {α : Type u_1} {β : Type u_2} (f : αOption β) (a : α) (l : List α) :
List.filterMap f (a :: l) = match f a with | none => List.filterMap f l | some b => b :: List.filterMap f l
theorem List.filterMap_cons_none {α : Type u_1} {β : Type u_2} {f : αOption β} (a : α) (l : List α) (h : f a = none) :
theorem List.filterMap_cons_some {α : Type u_1} {β : Type u_2} (f : αOption β) (a : α) (l : List α) {b : β} (h : f a = some b) :
theorem List.filterMap_append {α : Type u_1} {β : Type u_2} (l : List α) (l' : List α) (f : αOption β) :
theorem List.filterMap_eq_map {α : Type u_1} {β : Type u_2} (f : αβ) :
theorem List.filterMap_eq_filter {α : Type u_1} (p : αBool) :
List.filterMap (Option.guard fun (x : α) => p x = true) = List.filter p
theorem List.filterMap_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption β) (g : βOption γ) (l : List α) :
List.filterMap g (List.filterMap f l) = List.filterMap (fun (x : α) => Option.bind (f x) g) l
theorem List.map_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption β) (g : βγ) (l : List α) :
List.map g (List.filterMap f l) = List.filterMap (fun (x : α) => Option.map g (f x)) l
theorem List.filterMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : βOption γ) (l : List α) :
theorem List.filter_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (p : βBool) (l : List α) :
List.filter p (List.filterMap f l) = List.filterMap (fun (x : α) => Option.filter p (f x)) l
theorem List.filterMap_filter {α : Type u_1} {β : Type u_2} (p : αBool) (f : αOption β) (l : List α) :
List.filterMap f (List.filter p l) = List.filterMap (fun (x : α) => if p x = true then f x else none) l
@[simp]
theorem List.filterMap_some {α : Type u_1} (l : List α) :
List.filterMap some l = l
theorem List.map_filterMap_some_eq_filter_map_is_some {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
List.map some (List.filterMap f l) = List.filter (fun (b : Option β) => Option.isSome b) (List.map f l)
@[simp]
theorem List.mem_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) {b : β} :
b List.filterMap f l ∃ (a : α), a l f a = some b
@[simp]
theorem List.filterMap_join {α : Type u_1} {β : Type u_2} (f : αOption β) (L : List (List α)) :
theorem List.map_filterMap_of_inv {α : Type u_1} {β : Type u_2} (f : αOption β) (g : βα) (H : ∀ (x : α), Option.map g (f x) = some x) (l : List α) :
theorem List.length_filter_le {α : Type u_1} (p : αBool) (l : List α) :
theorem List.length_filterMap_le {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
theorem List.Sublist.filterMap {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : αOption β) (s : List.Sublist l₁ l₂) :
theorem List.Sublist.filter {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : List.Sublist l₁ l₂) :
theorem List.map_filter {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) :
@[simp]
theorem List.filter_filter :
∀ {α : Type u_1} {p : αBool} (q : αBool) (l : List α), List.filter p (List.filter q l) = List.filter (fun (a : α) => decide (p a = true q a = true)) l
theorem List.filter_eq_self :
∀ {α : Type u_1} {p : αBool} {l : List α}, List.filter p l = l ∀ (a : α), a lp a = true
theorem List.filter_length_eq_length :
∀ {α : Type u_1} {p : αBool} {l : List α}, List.length (List.filter p l) = List.length l ∀ (a : α), a lp a = true

find? #

theorem List.find?_cons_of_pos :
∀ {α : Type u_1} {p : αBool} {a : α} (l : List α), p a = trueList.find? p (a :: l) = some a
theorem List.find?_cons_of_neg :
∀ {α : Type u_1} {p : αBool} {a : α} (l : List α), ¬p a = trueList.find? p (a :: l) = List.find? p l
theorem List.find?_eq_none :
∀ {α : Type u_1} {p : αBool} {l : List α}, List.find? p l = none ∀ (x : α), x l¬p x = true
theorem List.find?_some :
∀ {α : Type u_1} {p : αBool} {a : α} {l : List α}, List.find? p l = some ap a = true
@[simp]
theorem List.mem_of_find?_eq_some :
∀ {α : Type u_1} {p : αBool} {a : α} {l : List α}, List.find? p l = some aa l

findSome? #

theorem List.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αOption β} (w : List.findSome? f l = some b) :
∃ (a : α), a l f a = some b

findIdx #

@[simp]
theorem List.findIdx_nil {α : Type u_1} (p : αBool) :
theorem List.findIdx_cons {α : Type u_1} (p : αBool) (b : α) (l : List α) :
List.findIdx p (b :: l) = bif p b then 0 else List.findIdx p l + 1
theorem List.findIdx_cons.findIdx_go_succ {α : Type u_1} (p : αBool) (l : List α) (n : Nat) :
List.findIdx.go p l (n + 1) = List.findIdx.go p l n + 1
theorem List.findIdx_of_get?_eq_some {α : Type u_1} {p : αBool} {y : α} {xs : List α} (w : List.get? xs (List.findIdx p xs) = some y) :
p y = true
theorem List.findIdx_get {α : Type u_1} {p : αBool} {xs : List α} {w : List.findIdx p xs < List.length xs} :
p (List.get xs { val := List.findIdx p xs, isLt := w }) = true
theorem List.findIdx_lt_length_of_exists {α : Type u_1} {p : αBool} {xs : List α} (h : ∃ (x : α), x xs p x = true) :
theorem List.findIdx_get?_eq_get_of_exists {α : Type u_1} {p : αBool} {xs : List α} (h : ∃ (x : α), x xs p x = true) :
List.get? xs (List.findIdx p xs) = some (List.get xs { val := List.findIdx p xs, isLt := })

findIdx? #

@[simp]
theorem List.findIdx?_nil {α : Type u_1} {p : αBool} {i : Nat} :
List.findIdx? p [] i = none
@[simp]
theorem List.findIdx?_cons :
∀ {α : Type u_1} {x : α} {xs : List α} {p : αBool} {i : Nat}, List.findIdx? p (x :: xs) i = if p x = true then some i else List.findIdx? p xs (i + 1)
@[simp]
theorem List.findIdx?_succ {α : Type u_1} {xs : List α} {p : αBool} {i : Nat} :
List.findIdx? p xs (i + 1) = Option.map (fun (i : Nat) => i + 1) (List.findIdx? p xs i)
theorem List.findIdx?_eq_some_iff {α : Type u_1} {i : Nat} (xs : List α) (p : αBool) :
theorem List.findIdx?_of_eq_some {α : Type u_1} {i : Nat} {xs : List α} {p : αBool} (w : List.findIdx? p xs = some i) :
match List.get? xs i with | some a => p a = true | none => false = true
theorem List.findIdx?_of_eq_none {α : Type u_1} {xs : List α} {p : αBool} (w : List.findIdx? p xs = none) (i : Nat) :
match List.get? xs i with | some a => ¬p a = true | none => true = true
@[simp]
theorem List.findIdx?_append {α : Type u_1} {xs : List α} {ys : List α} {p : αBool} :
List.findIdx? p (xs ++ ys) = HOrElse.hOrElse (List.findIdx? p xs) fun (x : Unit) => Option.map (fun (i : Nat) => i + List.length xs) (List.findIdx? p ys)
@[simp]
theorem List.findIdx?_replicate {n : Nat} :
∀ {α : Type u_1} {a : α} {p : αBool}, List.findIdx? p (List.replicate n a) = if 0 < n p a = true then some 0 else none

pairwise #

theorem List.Pairwise.sublist :
∀ {α : Type u_1} {l₁ l₂ : List α} {R : ααProp}, List.Sublist l₁ l₂List.Pairwise R l₂List.Pairwise R l₁
theorem List.pairwise_map {α : Type u_1} :
∀ {α_1 : Type u_2} {f : αα_1} {R : α_1α_1Prop} {l : List α}, List.Pairwise R (List.map f l) List.Pairwise (fun (a b : α) => R (f a) (f b)) l
theorem List.pairwise_append {α : Type u_1} {R : ααProp} {l₁ : List α} {l₂ : List α} :
List.Pairwise R (l₁ ++ l₂) List.Pairwise R l₁ List.Pairwise R l₂ ∀ (a : α), a l₁∀ (b : α), b l₂R a b
theorem List.pairwise_reverse {α : Type u_1} {R : ααProp} {l : List α} :
List.Pairwise R (List.reverse l) List.Pairwise (fun (a b : α) => R b a) l
theorem List.Pairwise.imp {α : Type u_1} {R : ααProp} {S : ααProp} (H : ∀ {a b : α}, R a bS a b) {l : List α} :

replaceF #

theorem List.replaceF_nil :
∀ {α : Type u_1} {p : αOption α}, List.replaceF p [] = []
theorem List.replaceF_cons {α : Type u_1} {p : αOption α} (a : α) (l : List α) :
List.replaceF p (a :: l) = match p a with | none => a :: List.replaceF p l | some a' => a' :: l
theorem List.replaceF_cons_of_some {α : Type u_1} {a' : α} {a : α} {l : List α} (p : αOption α) (h : p a = some a') :
List.replaceF p (a :: l) = a' :: l
theorem List.replaceF_cons_of_none {α : Type u_1} {a : α} {l : List α} (p : αOption α) (h : p a = none) :
theorem List.replaceF_of_forall_none {α : Type u_1} {p : αOption α} {l : List α} (h : ∀ (a : α), a lp a = none) :
theorem List.exists_of_replaceF {α : Type u_1} {p : αOption α} {l : List α} {a : α} {a' : α} (al : a l) (pa : p a = some a') :
∃ (a : α), ∃ (a' : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁p b = none) p a = some a' l = l₁ ++ a :: l₂ List.replaceF p l = l₁ ++ a' :: l₂
theorem List.exists_or_eq_self_of_replaceF {α : Type u_1} (p : αOption α) (l : List α) :
List.replaceF p l = l ∃ (a : α), ∃ (a' : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁p b = none) p a = some a' l = l₁ ++ a :: l₂ List.replaceF p l = l₁ ++ a' :: l₂
@[simp]
theorem List.length_replaceF :
∀ {α : Type u_1} {f : αOption α} {l : List α}, List.length (List.replaceF f l) = List.length l

disjoint #

theorem List.disjoint_symm :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Disjoint l₁ l₂List.Disjoint l₂ l₁
theorem List.disjoint_comm :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Disjoint l₁ l₂ List.Disjoint l₂ l₁
theorem List.disjoint_left :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Disjoint l₁ l₂ ∀ ⦃a : α⦄, a l₁¬a l₂
theorem List.disjoint_right :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Disjoint l₁ l₂ ∀ ⦃a : α⦄, a l₂¬a l₁
theorem List.disjoint_iff_ne :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.Disjoint l₁ l₂ ∀ (a : α), a l₁∀ (b : α), b l₂a b
theorem List.disjoint_of_subset_left :
∀ {α : Type u_1} {l₁ l l₂ : List α}, l₁ lList.Disjoint l l₂List.Disjoint l₁ l₂
theorem List.disjoint_of_subset_right :
∀ {α : Type u_1} {l₂ l l₁ : List α}, l₂ lList.Disjoint l₁ lList.Disjoint l₁ l₂
theorem List.disjoint_of_disjoint_cons_left :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Disjoint (a :: l₁) l₂List.Disjoint l₁ l₂
theorem List.disjoint_of_disjoint_cons_right :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Disjoint l₁ (a :: l₂)List.Disjoint l₁ l₂
@[simp]
theorem List.disjoint_nil_left {α : Type u_1} (l : List α) :
@[simp]
theorem List.disjoint_nil_right {α : Type u_1} (l : List α) :
@[simp]
theorem List.singleton_disjoint :
∀ {α : Type u_1} {a : α} {l : List α}, List.Disjoint [a] l ¬a l
@[simp]
theorem List.disjoint_singleton :
∀ {α : Type u_1} {l : List α} {a : α}, List.Disjoint l [a] ¬a l
@[simp]
theorem List.disjoint_append_left :
∀ {α : Type u_1} {l₁ l₂ l : List α}, List.Disjoint (l₁ ++ l₂) l List.Disjoint l₁ l List.Disjoint l₂ l
@[simp]
theorem List.disjoint_append_right :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Disjoint l (l₁ ++ l₂) List.Disjoint l l₁ List.Disjoint l l₂
@[simp]
theorem List.disjoint_cons_left :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, List.Disjoint (a :: l₁) l₂ ¬a l₂ List.Disjoint l₁ l₂
@[simp]
theorem List.disjoint_cons_right :
∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, List.Disjoint l₁ (a :: l₂) ¬a l₁ List.Disjoint l₁ l₂
theorem List.disjoint_of_disjoint_append_left_left :
∀ {α : Type u_1} {l₁ l₂ l : List α}, List.Disjoint (l₁ ++ l₂) lList.Disjoint l₁ l
theorem List.disjoint_of_disjoint_append_left_right :
∀ {α : Type u_1} {l₁ l₂ l : List α}, List.Disjoint (l₁ ++ l₂) lList.Disjoint l₂ l
theorem List.disjoint_of_disjoint_append_right_left :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Disjoint l (l₁ ++ l₂)List.Disjoint l l₁
theorem List.disjoint_of_disjoint_append_right_right :
∀ {α : Type u_1} {l l₁ l₂ : List α}, List.Disjoint l (l₁ ++ l₂)List.Disjoint l l₂

foldl / foldr #

theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁β₂) (g : αβ₂α) (l : List β₁) (init : α) :
List.foldl g init (List.map f l) = List.foldl (fun (x : α) (y : β₁) => g x (f y)) init l
theorem List.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁α₂) (g : α₂ββ) (l : List α₁) (init : β) :
List.foldr g init (List.map f l) = List.foldr (fun (x : α₁) (y : β) => g (f x) y) init l
theorem List.foldl_hom {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁α₂) (g₁ : α₁βα₁) (g₂ : α₂βα₂) (l : List β) (init : α₁) (H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) :
List.foldl g₂ (f init) l = f (List.foldl g₁ init l)
theorem List.foldr_hom {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁β₂) (g₁ : αβ₁β₁) (g₂ : αβ₂β₂) (l : List α) (init : β₁) (H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) :
List.foldr g₂ (f init) l = f (List.foldr g₁ init l)

union #

theorem List.union_def {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
l₁ l₂ = List.foldr List.insert l₂ l₁
@[simp]
theorem List.nil_union {α : Type u_1} [DecidableEq α] (l : List α) :
[] l = l
@[simp]
theorem List.cons_union {α : Type u_1} [DecidableEq α] (a : α) (l₁ : List α) (l₂ : List α) :
a :: l₁ l₂ = List.insert a (l₁ l₂)
@[simp]
theorem List.mem_union_iff {α : Type u_1} :
∀ {x : DecidableEq α} {x_1 : α} {l₁ l₂ : List α}, x_1 l₁ l₂ x_1 l₁ x_1 l₂

inter #

theorem List.inter_def {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
l₁ l₂ = List.filter (fun (x : α) => decide (x l₂)) l₁
@[simp]
theorem List.mem_inter_iff {α : Type u_1} :
∀ {x : DecidableEq α} {x_1 : α} {l₁ l₂ : List α}, x_1 l₁ l₂ x_1 l₁ x_1 l₂

product #

theorem List.pair_mem_product {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {x : α} {y : β} :
(x, y) List.product xs ys x xs y ys

List.prod satisfies a specification of cartesian product on lists.

leftpad #

theorem List.leftpad_length {α : Type u_1} (n : Nat) (a : α) (l : List α) :

The length of the List returned by List.leftpad n a l is equal to the larger of n and l.length

theorem List.leftpad_prefix {α : Type u_1} (n : Nat) (a : α) (l : List α) :
theorem List.leftpad_suffix {α : Type u_1} (n : Nat) (a : α) (l : List α) :

monadic operations #

@[simp]
theorem List.forIn_eq_forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] :
List.forIn = forIn
theorem List.forIn_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αβm (ForInStep β)) (l : List α) (init : β) :
forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
@[simp]
theorem List.forM_append {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] [LawfulMonad m] (l₁ : List α) (l₂ : List α) (f : αm PUnit) :
List.forM (l₁ ++ l₂) f = do List.forM l₁ f List.forM l₂ f

diff #

@[simp]
theorem List.diff_nil {α : Type u_1} [DecidableEq α] (l : List α) :
List.diff l [] = l
@[simp]
theorem List.diff_cons {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) (a : α) :
List.diff l₁ (a :: l₂) = List.diff (List.erase l₁ a) l₂
theorem List.diff_cons_right {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) (a : α) :
List.diff l₁ (a :: l₂) = List.erase (List.diff l₁ l₂) a
theorem List.diff_erase {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) (a : α) :
List.erase (List.diff l₁ l₂) a = List.diff (List.erase l₁ a) l₂
@[simp]
theorem List.nil_diff {α : Type u_1} [DecidableEq α] (l : List α) :
List.diff [] l = []
theorem List.cons_diff {α : Type u_1} [DecidableEq α] (a : α) (l₁ : List α) (l₂ : List α) :
List.diff (a :: l₁) l₂ = if a l₂ then List.diff l₁ (List.erase l₂ a) else a :: List.diff l₁ l₂
theorem List.cons_diff_of_mem {α : Type u_1} [DecidableEq α] {a : α} {l₂ : List α} (h : a l₂) (l₁ : List α) :
List.diff (a :: l₁) l₂ = List.diff l₁ (List.erase l₂ a)
theorem List.cons_diff_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {l₂ : List α} (h : ¬a l₂) (l₁ : List α) :
List.diff (a :: l₁) l₂ = a :: List.diff l₁ l₂
theorem List.diff_eq_foldl {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
List.diff l₁ l₂ = List.foldl List.erase l₁ l₂
@[simp]
theorem List.diff_append {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) (l₃ : List α) :
List.diff l₁ (l₂ ++ l₃) = List.diff (List.diff l₁ l₂) l₃
theorem List.diff_sublist {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
List.Sublist (List.diff l₁ l₂) l₁
theorem List.diff_subset {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
List.diff l₁ l₂ l₁
theorem List.mem_diff_of_mem {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} :
a l₁¬a l₂a List.diff l₁ l₂
theorem List.Sublist.diff_right {α : Type u_1} [DecidableEq α] {l₁ : List α} {l₂ : List α} {l₃ : List α} :
List.Sublist l₁ l₂List.Sublist (List.diff l₁ l₃) (List.diff l₂ l₃)
theorem List.Sublist.erase_diff_erase_sublist {α : Type u_1} [DecidableEq α] {a : α} {l₁ : List α} {l₂ : List α} :
List.Sublist l₁ l₂List.Sublist (List.diff (List.erase l₂ a) (List.erase l₁ a)) (List.diff l₂ l₁)

prefix, suffix, infix #

@[simp]
theorem List.prefix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₁ <+: l₁ ++ l₂
@[simp]
theorem List.suffix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₂ <:+ l₁ ++ l₂
theorem List.infix_append {α : Type u_1} (l₁ : List α) (l₂ : List α) (l₃ : List α) :
l₂ <:+: l₁ ++ l₂ ++ l₃
@[simp]
theorem List.infix_append' {α : Type u_1} (l₁ : List α) (l₂ : List α) (l₃ : List α) :
l₂ <:+: l₁ ++ (l₂ ++ l₃)
theorem List.IsPrefix.isInfix :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂l₁ <:+: l₂
theorem List.IsSuffix.isInfix :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂l₁ <:+: l₂
theorem List.nil_prefix {α : Type u_1} (l : List α) :
[] <+: l
theorem List.nil_suffix {α : Type u_1} (l : List α) :
[] <:+ l
theorem List.nil_infix {α : Type u_1} (l : List α) :
[] <:+: l
theorem List.prefix_refl {α : Type u_1} (l : List α) :
l <+: l
theorem List.suffix_refl {α : Type u_1} (l : List α) :
l <:+ l
theorem List.infix_refl {α : Type u_1} (l : List α) :
l <:+: l
@[simp]
theorem List.suffix_cons {α : Type u_1} (a : α) (l : List α) :
l <:+ a :: l
theorem List.infix_cons :
∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂l₁ <:+: a :: l₂
theorem List.infix_concat :
∀ {α : Type u_1} {l₁ l₂ : List α} {a : α}, l₁ <:+: l₂l₁ <:+: List.concat l₂ a
theorem List.IsPrefix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <+: l₂l₂ <+: l₃l₁ <+: l₃
theorem List.IsSuffix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <:+ l₂l₂ <:+ l₃l₁ <:+ l₃
theorem List.IsInfix.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <:+: l₂l₂ <:+: l₃l₁ <:+: l₃
theorem List.IsInfix.sublist :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂List.Sublist l₁ l₂
theorem List.IsInfix.subset :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂l₁ l₂
theorem List.IsPrefix.sublist :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂List.Sublist l₁ l₂
theorem List.IsPrefix.subset :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂l₁ l₂
theorem List.IsSuffix.sublist :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂List.Sublist l₁ l₂
theorem List.IsSuffix.subset :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂l₁ l₂
@[simp]
theorem List.reverse_suffix :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.reverse l₁ <:+ List.reverse l₂ l₁ <+: l₂
@[simp]
theorem List.reverse_prefix :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.reverse l₁ <+: List.reverse l₂ l₁ <:+ l₂
@[simp]
theorem List.reverse_infix :
∀ {α : Type u_1} {l₁ l₂ : List α}, List.reverse l₁ <:+: List.reverse l₂ l₁ <:+: l₂
theorem List.IsInfix.length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂List.length l₁ List.length l₂
theorem List.IsPrefix.length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂List.length l₁ List.length l₂
theorem List.IsSuffix.length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂List.length l₁ List.length l₂
@[simp]
theorem List.infix_nil :
∀ {α : Type u_1} {l : List α}, l <:+: [] l = []
@[simp]
theorem List.prefix_nil :
∀ {α : Type u_1} {l : List α}, l <+: [] l = []
@[simp]
theorem List.suffix_nil :
∀ {α : Type u_1} {l : List α}, l <:+ [] l = []
theorem List.infix_iff_prefix_suffix {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₁ <:+: l₂ ∃ (t : List α), l₁ <+: t t <:+ l₂
theorem List.IsInfix.eq_of_length :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂List.length l₁ = List.length l₂l₁ = l₂
theorem List.IsPrefix.eq_of_length :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂List.length l₁ = List.length l₂l₁ = l₂
theorem List.IsSuffix.eq_of_length :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂List.length l₁ = List.length l₂l₁ = l₂
theorem List.prefix_of_prefix_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} :
l₁ <+: l₃l₂ <+: l₃List.length l₁ List.length l₂l₁ <+: l₂
theorem List.prefix_or_prefix_of_prefix :
∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <+: l₃l₂ <+: l₃l₁ <+: l₂ l₂ <+: l₁
theorem List.suffix_of_suffix_length_le :
∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃l₂ <:+ l₃List.length l₁ List.length l₂l₁ <:+ l₂
theorem List.suffix_or_suffix_of_suffix :
∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃l₂ <:+ l₃l₁ <:+ l₂ l₂ <:+ l₁
theorem List.suffix_cons_iff :
∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+ a :: l₂ l₁ = a :: l₂ l₁ <:+ l₂
theorem List.infix_cons_iff :
∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁ <:+: a :: l₂ l₁ <+: a :: l₂ l₁ <:+: l₂
theorem List.infix_of_mem_join {α : Type u_1} {l : List α} {L : List (List α)} :
l Ll <:+: List.join L
theorem List.prefix_append_right_inj :
∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), l ++ l₁ <+: l ++ l₂ l₁ <+: l₂
theorem List.prefix_cons_inj :
∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), a :: l₁ <+: a :: l₂ l₁ <+: l₂
theorem List.take_prefix {α : Type u_1} (n : Nat) (l : List α) :
theorem List.drop_suffix {α : Type u_1} (n : Nat) (l : List α) :
theorem List.take_sublist {α : Type u_1} (n : Nat) (l : List α) :
theorem List.drop_sublist {α : Type u_1} (n : Nat) (l : List α) :
theorem List.take_subset {α : Type u_1} (n : Nat) (l : List α) :
theorem List.drop_subset {α : Type u_1} (n : Nat) (l : List α) :
theorem List.mem_of_mem_take {α : Type u_1} {a : α} {n : Nat} {l : List α} (h : a List.take n l) :
a l
theorem List.IsPrefix.filter {α : Type u_1} (p : αBool) ⦃l₁ : List α ⦃l₂ : List α (h : l₁ <+: l₂) :
theorem List.IsSuffix.filter {α : Type u_1} (p : αBool) ⦃l₁ : List α ⦃l₂ : List α (h : l₁ <:+ l₂) :
theorem List.IsInfix.filter {α : Type u_1} (p : αBool) ⦃l₁ : List α ⦃l₂ : List α (h : l₁ <:+: l₂) :
theorem List.mem_of_mem_drop {α : Type u_1} {a : α} {n : Nat} {l : List α} (h : a List.drop n l) :
a l
theorem List.disjoint_take_drop {α : Type u_1} {m : Nat} {n : Nat} {l : List α} :
List.Nodup lm nList.Disjoint (List.take m l) (List.drop n l)

takeWhile and dropWhile #

@[simp]
theorem List.takeWhile_append_dropWhile {α : Type u_1} (p : αBool) (l : List α) :
theorem List.dropWhile_append {α : Type u_1} {p : αBool} {xs : List α} {ys : List α} :
List.dropWhile p (xs ++ ys) = if List.isEmpty (List.dropWhile p xs) = true then List.dropWhile p ys else List.dropWhile p xs ++ ys

Chain #

@[simp]
theorem List.chain_cons {α : Type u_1} {R : ααProp} {a : α} {b : α} {l : List α} :
List.Chain R a (b :: l) R a b List.Chain R b l
theorem List.rel_of_chain_cons {α : Type u_1} {R : ααProp} {a : α} {b : α} {l : List α} (p : List.Chain R a (b :: l)) :
R a b
theorem List.chain_of_chain_cons {α : Type u_1} {R : ααProp} {a : α} {b : α} {l : List α} (p : List.Chain R a (b :: l)) :
theorem List.Chain.imp' {α : Type u_1} {R : ααProp} {S : ααProp} (HRS : ∀ ⦃a b : α⦄, R a bS a b) {a : α} {b : α} (Hab : ∀ ⦃c : α⦄, R a cS b c) {l : List α} (p : List.Chain R a l) :
theorem List.Chain.imp {α : Type u_1} {R : ααProp} {S : ααProp} (H : ∀ (a b : α), R a bS a b) {a : α} {l : List α} (p : List.Chain R a l) :
theorem List.Pairwise.chain :
∀ {α : Type u_1} {R : ααProp} {a : α} {l : List α}, List.Pairwise R (a :: l)List.Chain R a l

range', range #

@[simp]
theorem List.length_range' (s : Nat) (step : Nat) (n : Nat) :
@[simp]
theorem List.range'_eq_nil {s : Nat} {n : Nat} {step : Nat} :
List.range' s n step = [] n = 0
theorem List.mem_range' {m : Nat} {s : Nat} {step : Nat} {n : Nat} :
m List.range' s n step ∃ (i : Nat), i < n m = s + step * i
@[simp]
theorem List.mem_range'_1 {m : Nat} {s : Nat} {n : Nat} :
m List.range' s n s m m < s + n
theorem List.map_add_range' (a : Nat) (s : Nat) (n : Nat) (step : Nat) :
List.map (fun (x : Nat) => a + x) (List.range' s n step) = List.range' (a + s) n step
theorem List.map_sub_range' {step : Nat} (a : Nat) (s : Nat) (n : Nat) (h : a s) :
List.map (fun (x : Nat) => x - a) (List.range' s n step) = List.range' (s - a) n step
theorem List.chain_succ_range' (s : Nat) (n : Nat) (step : Nat) :
List.Chain (fun (a b : Nat) => b = a + step) s (List.range' (s + step) n step)
theorem List.chain_lt_range' (s : Nat) (n : Nat) {step : Nat} (h : 0 < step) :
List.Chain (fun (x x_1 : Nat) => x < x_1) s (List.range' (s + step) n step)
theorem List.range'_append (s : Nat) (m : Nat) (n : Nat) (step : Nat) :
List.range' s m step ++ List.range' (s + step * m) n step = List.range' s (n + m) step
@[simp]
theorem List.range'_append_1 (s : Nat) (m : Nat) (n : Nat) :
List.range' s m ++ List.range' (s + m) n = List.range' s (n + m)
theorem List.range'_sublist_right {step : Nat} {s : Nat} {m : Nat} {n : Nat} :
List.Sublist (List.range' s m step) (List.range' s n step) m n
theorem List.range'_subset_right {step : Nat} {s : Nat} {m : Nat} {n : Nat} (step0 : 0 < step) :
List.range' s m step List.range' s n step m n
theorem List.get?_range' (s : Nat) (step : Nat) {m : Nat} {n : Nat} :
m < nList.get? (List.range' s n step) m = some (s + step * m)
@[simp]
theorem List.get_range' {n : Nat} {m : Nat} {step : Nat} (i : Nat) (H : i < List.length (List.range' n m step)) :
List.get (List.range' n m step) { val := i, isLt := H } = n + step * i
theorem List.range'_concat {step : Nat} (s : Nat) (n : Nat) :
List.range' s (n + 1) step = List.range' s n step ++ [s + step * n]
theorem List.range'_1_concat (s : Nat) (n : Nat) :
List.range' s (n + 1) = List.range' s n ++ [s + n]
theorem List.range'_eq_map_range (s : Nat) (n : Nat) :
List.range' s n = List.map (fun (x : Nat) => s + x) (List.range n)
@[simp]
@[simp]
theorem List.range_eq_nil {n : Nat} :
List.range n = [] n = 0
@[simp]
theorem List.mem_range {m : Nat} {n : Nat} :
theorem List.get?_range {m : Nat} {n : Nat} (h : m < n) :
@[simp]
theorem List.range_add (a : Nat) (b : Nat) :
List.range (a + b) = List.range a ++ List.map (fun (x : Nat) => a + x) (List.range b)
@[simp]
theorem List.mem_iota {m : Nat} {n : Nat} :
m List.iota n 1 m m n
theorem List.reverse_range' (s : Nat) (n : Nat) :
List.reverse (List.range' s n) = List.map (fun (x : Nat) => s + n - 1 - x) (List.range n)
@[simp]
theorem List.get_range {n : Nat} (i : Nat) (H : i < List.length (List.range n)) :
List.get (List.range n) { val := i, isLt := H } = i

enum, enumFrom #

@[simp]
theorem List.enumFrom_map_fst {α : Type u_1} (n : Nat) (l : List α) :
@[simp]
theorem List.enum_map_fst {α : Type u_1} (l : List α) :
@[simp]
theorem List.enumFrom_length {α : Type u_1} {n : Nat} {l : List α} :
@[simp]
theorem List.enum_length :
∀ {α : Type u_1} {l : List α}, List.length (List.enum l) = List.length l

maximum? #

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

indexOf and indexesOf #

theorem List.foldrIdx_start {α : Type u_1} {xs : List α} :
∀ {α_1 : Sort u_2} {f : Natαα_1α_1} {i : α_1} {s : Nat}, List.foldrIdx f i xs s = List.foldrIdx (fun (i : Nat) => f (i + s)) i xs
@[simp]
theorem List.foldrIdx_cons {α : Type u_1} {x : α} {xs : List α} :
∀ {α_1 : Sort u_2} {f : Natαα_1α_1} {i : α_1} {s : Nat}, List.foldrIdx f i (x :: xs) s = f s x (List.foldrIdx f i xs (s + 1))
theorem List.findIdxs_cons_aux {α : Type u_1} {xs : List α} {s : Nat} (p : αBool) :
List.foldrIdx (fun (i : Nat) (a : α) (is : List Nat) => if p a = true then (i + 1) :: is else is) [] xs s = List.map (fun (x : Nat) => x + 1) (List.foldrIdx (fun (i : Nat) (a : α) (is : List Nat) => if p a = true then i :: is else is) [] xs s)
theorem List.findIdxs_cons {α : Type u_1} {x : α} {xs : List α} {p : αBool} :
List.findIdxs p (x :: xs) = bif p x then 0 :: List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs) else List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs)
@[simp]
theorem List.indexesOf_nil {α : Type u_1} {x : α} [BEq α] :
theorem List.indexesOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] :
List.indexesOf y (x :: xs) = bif x == y then 0 :: List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs) else List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs)
@[simp]
theorem List.indexOf_nil {α : Type u_1} {x : α} [BEq α] :
theorem List.indexOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] :
List.indexOf y (x :: xs) = bif x == y then 0 else List.indexOf y xs + 1
theorem List.indexOf_mem_indexesOf {α : Type u_1} {x : α} [BEq α] [LawfulBEq α] {xs : List α} (m : x xs) :
theorem List.merge_loop_nil_left {α : Type u_1} (s : ααBool) (r : List α) (t : List α) :
theorem List.merge_loop_nil_right {α : Type u_1} (s : ααBool) (l : List α) (t : List α) :
theorem List.merge_loop {α : Type u_1} (s : ααBool) (l : List α) (r : List α) (t : List α) :
@[simp]
theorem List.merge_nil {α : Type u_1} (s : ααBool) (l : List α) :
List.merge s l [] = l
@[simp]
theorem List.nil_merge {α : Type u_1} (s : ααBool) (r : List α) :
List.merge s [] r = r
theorem List.cons_merge_cons {α : Type u_1} (s : ααBool) (a : α) (b : α) (l : List α) (r : List α) :
List.merge s (a :: l) (b :: r) = if s a b = true then a :: List.merge s l (b :: r) else b :: List.merge s (a :: l) r
@[simp]
theorem List.cons_merge_cons_pos {α : Type u_1} {a : α} {b : α} (s : ααBool) (l : List α) (r : List α) (h : s a b = true) :
List.merge s (a :: l) (b :: r) = a :: List.merge s l (b :: r)
@[simp]
theorem List.cons_merge_cons_neg {α : Type u_1} {a : α} {b : α} (s : ααBool) (l : List α) (r : List α) (h : ¬s a b = true) :
List.merge s (a :: l) (b :: r) = b :: List.merge s (a :: l) r
@[simp]
theorem List.length_merge {α : Type u_1} (s : ααBool) (l : List α) (r : List α) :
theorem List.mem_merge_left {α : Type u_1} {x : α} {l : List α} {r : List α} (s : ααBool) (h : x l) :
x List.merge s l r
theorem List.mem_merge_right {α : Type u_1} {x : α} {r : List α} {l : List α} (s : ααBool) (h : x r) :
x List.merge s l r