Basic properties of Lists

theorem List.cons_ne_nil {α : Type u_1} (a : α) (l : List α) : a :: l ≠ []

@[simp]

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 : α) : [a].length = 1

theorem List.length_pos_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → 0 < l.length

theorem List.exists_mem_of_length_pos {α : Type u_1} {l : List α} : 0 < l.length → ∃ (a : α), a ∈ l

theorem List.length_pos_iff_exists_mem {α : Type u_1} {l : List α} : 0 < l.length ↔ ∃ (a : α), a ∈ l

theorem List.exists_cons_of_length_pos {α : Type u_1} {l : List α} : 0 < l.length → ∃ (h : α), ∃ (t : List α), l = h :: t

theorem List.length_pos_iff_exists_cons {α : Type u_1} {l : List α} : 0 < l.length ↔ ∃ (h : α), ∃ (t : List α), l = h :: t

theorem List.exists_cons_of_length_succ {α : Type u_1} {n : Nat} {l : List α} : l.length = n + 1 → ∃ (h : α), ∃ (t : List α), l = h :: t

@[simp]

theorem List.length_pos {α : Type u_1} {l : List α} : 0 < l.length ↔ 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 α} : l.length = 1 ↔ ∃ (a : α), l = [a]

mem

theorem List.mem_nil_iff {α : Type u_1} (a : α) : a ∈ [] ↔ False

@[simp]

theorem List.mem_toArray {α : Type u_1} {a : α} {l : List α} : a ∈ List.toArray l ↔ a ∈ l

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 :: l → b ∈ l → a ∈ 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

theorem List.elem_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : List α} : List.elem a as = true ↔ a ∈ as

@[simp]

theorem List.elem_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (as : List α) : List.elem a as = decide (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 :: l → a ≠ 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 :: l → a ≠ y ∧ ¬a ∈ l

drop

@[simp]

theorem List.drop_one {α : Type u_1} (l : List α) : List.drop 1 l = l.tail

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 l₁.length (l₁ ++ l₂) = l₂

theorem List.drop_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) : List.drop n (l₁ ++ l₂) = l₂

isEmpty

@[simp]

theorem List.isEmpty_nil {α : Type u_1} : [].isEmpty = true

@[simp]

theorem List.isEmpty_cons {α : Type u_1} {x : α} {xs : List α} : (x :: xs).isEmpty = false

append

theorem List.append_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.append 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 : α) : [].concat a = [a]

theorem List.concat_cons {α : Type u_1} (a : α) (b : α) (l : List α) : (a :: l).concat b = a :: l.concat b

theorem List.init_eq_of_concat_eq {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} : l₁.concat a = l₂.concat a → l₁ = l₂

theorem List.last_eq_of_concat_eq {α : Type u_1} {a : α} {b : α} {l : List α} : l.concat a = l.concat b → a = b

theorem List.concat_ne_nil {α : Type u_1} (a : α) (l : List α) : l.concat a ≠ []

theorem List.concat_append {α : Type u_1} (a : α) (l₁ : List α) (l₂ : List α) : l₁.concat a ++ l₂ = l₁ ++ a :: l₂

theorem List.append_concat {α : Type u_1} (a : α) (l₁ : List α) (l₂ : List α) : l₁ ++ l₂.concat a = (l₁ ++ l₂).concat 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 l → P i) ↔ ∀ (j : α), j ∈ l → P (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.zipWith f l₁ l₂).length = min l₁.length l₂.length

@[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 (l₁.zip 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 (l₁.zip 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.zipWith f l l').tail = List.zipWith f l.tail l'.tail

theorem List.zipWith_append {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l : List α) (la : List α) (l' : List β) (lb : List β) (h : l.length = l'.length) : 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 β) : (l₁.zip l₂).length = min l₁.length l₂.length

theorem List.zip_map {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (l₁ : List α) (l₂ : List β) : (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)

theorem List.zip_map_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : α → γ) (l₁ : List α) (l₂ : List β) : (List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)

theorem List.zip_map_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (l₁ : List α) (l₂ : List β) : l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)

theorem List.zip_append {α : Type u_1} {β : Type u_2} {l₁ : List α} {r₁ : List α} {l₂ : List β} {r₂ : List β} (_h : l₁.length = l₂.length) : (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂

theorem List.zip_map' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) (l : List α) : (List.map f l).zip (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) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂

theorem List.map_fst_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : l₁.length ≤ l₂.length → List.map Prod.fst (l₁.zip l₂) = l₁

theorem List.map_snd_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : l₂.length ≤ l₁.length → List.map Prod.snd (l₁.zip l₂) = l₂

join

theorem List.mem_join {α : Type u_1} {a : α} {L : List (List α)} : a ∈ L.join ↔ ∃ (l : List α), l ∈ L ∧ a ∈ l

theorem List.exists_of_mem_join : ∀ {α : Type u_1} {a : α} {L : List (List α)}, a ∈ L.join → ∃ (l : List α), l ∈ L ∧ a ∈ l

theorem List.mem_join_of_mem : ∀ {α : Type u_1} {l : List α} {L : List (List α)} {a : α}, l ∈ L → a ∈ l → a ∈ L.join

bind

theorem List.mem_bind {α : Type u_1} {β : Type u_2} {f : α → List β} {b : β} {l : List α} : b ∈ l.bind 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 ∈ l.bind 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) : b ∈ l.bind f

theorem List.bind_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (g : α → List β) (l : List α) : List.map f (l.bind g) = l.bind 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.instTransMemSubset_batteries {α : Type u_1} : Trans Membership.mem Subset Membership.mem

Equations

• List.instTransMemSubset_batteries = { trans := ⋯ }

instance List.instTransSubset_batteries {α : Type u_1} : Trans Subset Subset Subset

Equations

• List.instTransSubset_batteries = { 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) : List.replicate (n + 1) a = a :: List.replicate n a

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 ∈ l → b = a) → l = List.replicate l.length a

theorem List.eq_replicate {α : Type u_1} {a : α} {n : Nat} {l : List α} : l = List.replicate n a ↔ l.length = n ∧ ∀ (b : α), b ∈ l → b = a

getLast

theorem List.getLast_cons' {α : Type u_1} {a : α} {l : List α} (h₁ : a :: l ≠ []) (h₂ : l ≠ []) : (a :: l).getLast h₁ = l.getLast h₂

@[simp]

theorem List.getLast_append {α : Type u_1} {a : α} (l : List α) (h : l ++ [a] ≠ []) : (l ++ [a]).getLast h = a

theorem List.getLast_concat : ∀ {α : Type u_1} {l : List α} {a : α} (h : l.concat a ≠ []), (l.concat a).getLast 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 α) : [].Sublist l

@[simp]

theorem List.Sublist.refl {α : Type u_1} (l : List α) : l.Sublist l

theorem List.Sublist.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁.Sublist l₂) (h₂ : l₂.Sublist l₃) : l₁.Sublist l₃

instance List.instTransSublist {α : Type u_1} : Trans List.Sublist List.Sublist List.Sublist

Equations

• List.instTransSublist = { trans := ⋯ }

@[simp]

theorem List.sublist_cons {α : Type u_1} (a : α) (l : List α) : l.Sublist (a :: l)

theorem List.sublist_of_cons_sublist : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist l₂ → l₁.Sublist l₂

@[simp]

theorem List.sublist_append_left {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₁.Sublist (l₁ ++ l₂)

@[simp]

theorem List.sublist_append_right {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₂.Sublist (l₁ ++ l₂)

theorem List.sublist_append_of_sublist_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Sublist l₁ → l.Sublist (l₁ ++ l₂)

theorem List.sublist_append_of_sublist_right : ∀ {α : Type u_1} {l l₂ l₁ : List α}, l.Sublist l₂ → l.Sublist (l₁ ++ l₂)

@[simp]

theorem List.cons_sublist_cons : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist (a :: l₂) ↔ l₁.Sublist l₂

@[simp]

theorem List.append_sublist_append_left : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Sublist (l ++ l₂) ↔ l₁.Sublist l₂

theorem List.Sublist.append_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (l : List α), (l ++ l₁).Sublist (l ++ l₂)

theorem List.Sublist.append_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → ∀ (l : List α), (l₁ ++ l).Sublist (l₂ ++ l)

theorem List.sublist_or_mem_of_sublist : ∀ {α : Type u_1} {l l₁ : List α} {a : α} {l₂ : List α}, l.Sublist (l₁ ++ a :: l₂) → l.Sublist (l₁ ++ l₂) ∨ a ∈ l

theorem List.Sublist.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.reverse.Sublist l₂.reverse

@[simp]

theorem List.reverse_sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse.Sublist l₂.reverse ↔ l₁.Sublist l₂

@[simp]

theorem List.append_sublist_append_right : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l₁ ++ l).Sublist (l₂ ++ l) ↔ l₁.Sublist l₂

theorem List.Sublist.append : ∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, l₁.Sublist l₂ → r₁.Sublist r₂ → (l₁ ++ r₁).Sublist (l₂ ++ r₂)

theorem List.Sublist.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁ ⊆ l₂

instance List.instTransSublistSubset {α : Type u_1} : Trans List.Sublist Subset Subset

Equations

• List.instTransSublistSubset = { trans := ⋯ }

instance List.instTransSubsetSublist {α : Type u_1} : Trans Subset List.Sublist Subset

Equations

• List.instTransSubsetSublist = { trans := ⋯ }

instance List.instTransMemSublist {α : Type u_1} : Trans Membership.mem List.Sublist Membership.mem

Equations

• List.instTransMemSublist = { trans := ⋯ }

theorem List.Sublist.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length

@[simp]

theorem List.sublist_nil {α : Type u_1} {l : List α} : l.Sublist [] ↔ l = []

theorem List.Sublist.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.Sublist.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.length ≤ l₁.length → l₁ = l₂

@[simp]

theorem List.singleton_sublist {α : Type u_1} {a : α} {l : List α} : [a].Sublist l ↔ a ∈ l

@[simp]

theorem List.replicate_sublist_replicate {α : Type u_1} {m : Nat} {n : Nat} (a : α) : (List.replicate m a).Sublist (List.replicate n a) ↔ m ≤ n

theorem List.isSublist_iff_sublist {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ : List α} {l₂ : List α} : l₁.isSublist l₂ = true ↔ l₁.Sublist l₂

instance List.instDecidableSublistOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) : Decidable (l₁.Sublist l₂)

Equations

• l₁.instDecidableSublistOfDecidableEq l₂ = decidable_of_iff (l₁.isSublist l₂ = true) ⋯

head

theorem List.head!_of_head? {α : Type u_1} {a : α} [Inhabited α] {l : List α} : l.head? = some a → l.head! = a

theorem List.head?_eq_head {α : Type u_1} (l : List α) (h : l ≠ []) : l.head? = some (l.head h)

tail

@[simp]

theorem List.tailD_eq_tail? {α : Type u_1} (l : List α) (l' : List α) : l.tailD l' = l.tail?.getD l'

theorem List.tail_eq_tailD {α : Type u_1} (l : List α) : l.tail = l.tailD []

theorem List.tail_eq_tail? {α : Type u_1} (l : List α) : l.tail = l.tail?.getD []

next?

@[simp]

theorem List.next?_nil {α : Type u_1} : [].next? = none

@[simp]

theorem List.next?_cons {α : Type u_1} (a : α) (l : List α) : (a :: l).next? = some (a, l)

getLast

@[simp]

theorem List.getLastD_nil {α : Type u_1} (a : α) : [].getLastD a = a

@[simp]

theorem List.getLastD_cons {α : Type u_1} (a : α) (b : α) (l : List α) : (b :: l).getLastD a = l.getLastD b

theorem List.getLast_eq_getLastD {α : Type u_1} (a : α) (l : List α) (h : a :: l ≠ []) : (a :: l).getLast h = l.getLastD a

theorem List.getLastD_eq_getLast? {α : Type u_1} (a : α) (l : List α) : l.getLastD a = l.getLast?.getD a

@[simp]

theorem List.getLast_singleton {α : Type u_1} (a : α) (h : [a] ≠ []) : [a].getLast h = a

theorem List.getLast!_cons {α : Type u_1} {a : α} {l : List α} [Inhabited α] : (a :: l).getLast! = l.getLastD a

theorem List.getLast?_cons {α : Type u_1} {a : α} {l : List α} : (a :: l).getLast? = some (l.getLastD a)

@[simp]

theorem List.getLast?_singleton {α : Type u_1} (a : α) : [a].getLast? = some a

theorem List.getLast_mem {α : Type u_1} {l : List α} (h : l ≠ []) : l.getLast h ∈ l

theorem List.getLastD_mem_cons {α : Type u_1} (l : List α) (a : α) : l.getLastD a ∈ a :: l

@[simp]

theorem List.getLast?_reverse {α : Type u_1} (l : List α) : l.reverse.getLast? = l.head?

@[simp]

theorem List.head?_reverse {α : Type u_1} (l : List α) : l.reverse.head? = l.getLast?

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 ≠ []) : (x :: l).dropLast = x :: l.dropLast

@[simp]

theorem List.dropLast_append_of_ne_nil {α : Type u} {l : List α} (l' : List α) : l ≠ [] → (l' ++ l).dropLast = l' ++ l.dropLast

theorem List.dropLast_append_cons : ∀ {α : Type u_1} {l₁ : List α} {b : α} {l₂ : List α}, (l₁ ++ b :: l₂).dropLast = l₁ ++ (b :: l₂).dropLast

@[simp]

theorem List.dropLast_concat : ∀ {α : Type u_1} {l₁ : List α} {b : α}, (l₁ ++ [b]).dropLast = l₁

@[simp]

theorem List.length_dropLast {α : Type u_1} (xs : List α) : xs.dropLast.length = xs.length - 1

@[simp]

theorem List.get_dropLast {α : Type u_1} (xs : List α) (i : Fin xs.dropLast.length) : xs.dropLast.get i = xs.get ⟨↑i, ⋯⟩

nth element

theorem List.get_eq_iff : ∀ {α : Type u_1} {l : List α} {n : Fin l.length} {x : α}, l.get n = x ↔ l.get? ↑n = some x

@[simp]

theorem List.get_cons_cons_one : ∀ {α : Type u_1} {a₁ a₂ : α} {as : List α}, (a₁ :: a₂ :: as).get 1 = a₂

theorem List.get!_cons_succ {α : Type u_1} [Inhabited α] (l : List α) (a : α) (n : Nat) : (a :: l).get! (n + 1) = l.get! n

theorem List.get!_cons_zero {α : Type u_1} [Inhabited α] (l : List α) (a : α) : (a :: l).get! 0 = a

theorem List.get!_nil {α : Type u_1} [Inhabited α] (n : Nat) : [].get! n = default

theorem List.get!_len_le {α : Type u_1} [Inhabited α] {l : List α} {n : Nat} : l.length ≤ n → l.get! n = default

theorem List.get?_of_mem {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ (n : Nat), l.get? n = some a

theorem List.get?_mem {α : Type u_1} {l : List α} {n : Nat} {a : α} (e : l.get? n = some a) : a ∈ l

theorem List.Fin.exists_iff {n : Nat} (p : Fin n → Prop) : (∃ (i : Fin n), p i) ↔ ∃ (i : Nat), ∃ (h : i < n), p ⟨i, h⟩

theorem List.mem_iff_get? {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : Nat), l.get? n = some a

theorem List.get?_zero {α : Type u_1} (l : List α) : l.get? 0 = l.head?

@[simp]

theorem List.getElem_eq_get {α : Type u_1} (l : List α) (i : Nat) (h : i < l.length) : l[i] = l.get ⟨i, h⟩

@[simp]

theorem List.getElem?_eq_get? {α : Type u_1} (l : List α) (i : Nat) : l[i]? = l.get? i

theorem List.get?_inj {i : Nat} : ∀ {α : Type u_1} {xs : List α} {j : Nat}, i < xs.length → xs.Nodup → xs.get? i = xs.get? j → i = j

theorem List.get_of_eq {α : Type u_1} {l : List α} {l' : List α} (h : l = l') (i : Fin l.length) : l.get i = l'.get ⟨↑i, ⋯⟩

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) : [a].get n = a

theorem List.get_mk_zero {α : Type u_1} {l : List α} (h : 0 < l.length) : l.get ⟨0, h⟩ = l.head ⋯

theorem List.get_append_right_aux {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length

theorem List.get_append_right' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, ⋯⟩

theorem List.get_of_append_proof {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < l.length

theorem List.get_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : l.get ⟨n, ⋯⟩ = a

@[simp]

theorem List.get_replicate {α : Type u_1} (a : α) {n : Nat} (m : Fin (List.replicate n a).length) : (List.replicate n a).get m = a

@[simp]

theorem List.getLastD_concat {α : Type u_1} (a : α) (b : α) (l : List α) : (l ++ [b]).getLastD a = b

theorem List.get_cons_length {α : Type u_1} (x : α) (xs : List α) (n : Nat) (h : n = xs.length) : (x :: xs).get ⟨n, ⋯⟩ = (x :: xs).getLast ⋯

theorem List.get!_of_get? {α : Type u_1} {a : α} [Inhabited α] {l : List α} {n : Nat} : l.get? n = some a → l.get! n = a

@[simp]

theorem List.get!_eq_getD {α : Type u_1} [Inhabited α] (l : List α) (n : Nat) : l.get! n = l.getD 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 α) : (List.take i l).length = min i l.length

theorem List.length_take_le {α : Type u_1} (n : Nat) (l : List α) : (List.take n l).length ≤ n

theorem List.length_take_le' {α : Type u_1} (n : Nat) (l : List α) : (List.take n l).length ≤ l.length

theorem List.length_take_of_le {n : Nat} : ∀ {α : Type u_1} {l : List α}, n ≤ l.length → (List.take n l).length = n

theorem List.take_all_of_le {α : Type u_1} {n : Nat} {l : List α} (h : l.length ≤ n) : List.take n l = l

@[simp]

theorem List.take_left {α : Type u_1} (l₁ : List α) (l₂ : List α) : List.take l₁.length (l₁ ++ l₂) = l₁

theorem List.take_left' {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : l₁.length = n) : List.take n (l₁ ++ l₂) = l₁

theorem List.take_take {α : Type u_1} (n : Nat) (m : Nat) (l : List α) : List.take n (List.take m l) = List.take (min n m) l

theorem List.take_replicate {α : Type u_1} (a : α) (n : Nat) (m : Nat) : List.take n (List.replicate m a) = List.replicate (min n m) a

theorem List.map_take {α : Type u_1} {β : Type u_2} (f : α → β) (L : List α) (i : Nat) : List.map f (List.take i L) = List.take i (List.map f L)

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 - l₁.length) l₂

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

theorem List.take_append_of_le_length {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : n ≤ l₁.length) : List.take n (l₁ ++ l₂) = List.take n l₁

theorem List.take_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (i : Nat) : List.take (l₁.length + 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 < L.length) (hj : i < j) : L.get ⟨i, hi⟩ = (List.take j L).get ⟨i, ⋯⟩

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

theorem List.get_take' {α : Type u_1} (L : List α) {j : Nat} {i : Fin (List.take j L).length} : (List.take j L).get i = L.get ⟨↑i, ⋯⟩

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

theorem List.get?_take {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : m < n) : (List.take n l).get? m = l.get? m

theorem List.get?_take_eq_none {α : Type u_1} {l : List α} {n : Nat} {m : Nat} (h : n ≤ m) : (List.take n l).get? m = none

theorem List.get?_take_eq_if {α : Type u_1} {l : List α} {n : Nat} {m : Nat} : (List.take n l).get? m = if m < n then l.get? m else none

@[simp]

theorem List.nth_take_of_succ {α : Type u_1} {l : List α} {n : Nat} : (List.take (n + 1) l).get? n = l.get? n

theorem List.take_succ {α : Type u_1} {l : List α} {n : Nat} : List.take (n + 1) l = List.take n l ++ (l.get? n).toList

@[simp]

theorem List.take_eq_nil_iff {α : Type u_1} {l : List α} {k : Nat} : List.take k l = [] ↔ l = [] ∨ k = 0

@[simp]

theorem List.take_eq_take {α : Type u_1} {l : List α} {m : Nat} {n : Nat} : List.take m l = List.take n l ↔ min m l.length = min n l.length

theorem List.take_add {α : Type u_1} (l : List α) (m : Nat) (n : Nat) : List.take (m + n) l = List.take m l ++ List.take n (List.drop m l)

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_eq_take {α : Type u_1} (l : List α) : l.dropLast = List.take l.length.pred l

theorem List.dropLast_take {α : Type u_1} {n : Nat} {l : List α} (h : n < l.length) : (List.take n l).dropLast = List.take n.pred 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

@[simp]

theorem List.drop_eq_nil_iff_le {α : Type u_1} {l : List α} {k : Nat} : List.drop k l = [] ↔ l.length ≤ k

theorem List.tail_drop {α : Type u_1} (l : List α) (n : Nat) : (List.drop n l).tail = List.drop (n + 1) l

theorem List.drop_length_cons {α : Type u_1} {l : List α} (h : l ≠ []) (a : α) : List.drop l.length (a :: l) = [l.getLast h]

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 - l₁.length) l₂

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

theorem List.drop_append_of_le_length {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (h : n ≤ l₁.length) : List.drop n (l₁ ++ l₂) = List.drop n l₁ ++ l₂

@[simp]

theorem List.drop_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (i : Nat) : List.drop (l₁.length + 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) : sizeOf (List.drop n l) ≤ sizeOf l

theorem List.lt_length_drop {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (h : i + j < L.length) : j < (List.drop i L).length

theorem List.get_drop {α : Type u_1} (L : List α) {i : Nat} {j : Nat} (h : i + j < L.length) : L.get ⟨i + j, h⟩ = (List.drop i L).get ⟨j, ⋯⟩

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

theorem List.get_drop' {α : Type u_1} (L : List α) {i : Nat} {j : Fin (List.drop i L).length} : (List.drop i L).get j = L.get ⟨i + ↑j, ⋯⟩

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

@[simp]

theorem List.get?_drop {α : Type u_1} (L : List α) (i : Nat) (j : Nat) : (List.drop i L).get? j = L.get? (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.take_drop {α : Type u_1} (m : Nat) (n : Nat) (l : List α) : List.take n (List.drop m l) = List.drop m (List.take (m + n) l)

theorem List.drop_take {α : Type u_1} (m : Nat) (n : Nat) (l : List α) : List.drop n (List.take m l) = List.take (m - n) (List.drop n l)

theorem List.map_drop {α : Type u_1} {β : Type u_2} (f : α → β) (L : List α) (i : Nat) : List.map f (List.drop i L) = List.drop i (List.map f L)

theorem List.reverse_take {α : Type u_1} {xs : List α} (n : Nat) (h : n ≤ xs.length) : List.take n xs.reverse = (List.drop (xs.length - n) xs).reverse

@[simp]

theorem List.get_cons_drop {α : Type u_1} (l : List α) (i : Fin l.length) : l.get 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 < l.length) : List.drop n l = l.get ⟨n, 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 ≠ []

modifyNth

theorem List.modifyNthTail_id {α : Type u_1} (n : Nat) (l : List α) : List.modifyNthTail id n l = l

theorem List.eraseIdx_eq_modifyNthTail {α : Type u_1} (n : Nat) (l : List α) : l.eraseIdx n = List.modifyNthTail List.tail n l

@[deprecated List.eraseIdx_eq_modifyNthTail]

theorem List.removeNth_eq_nth_tail {α : Type u_1} (n : Nat) (l : List α) : l.eraseIdx n = List.modifyNthTail List.tail n l

Alias of List.eraseIdx_eq_modifyNthTail.

theorem List.get?_modifyNth {α : Type u_1} (f : α → α) (n : Nat) (l : List α) (m : Nat) : (List.modifyNth f n l).get? m = (fun (a : α) => if n = m then f a else a) <$> l.get? m

theorem List.modifyNthTail_length {α : Type u_1} (f : List α → List α) (H : ∀ (l : List α), (f l).length = l.length) (n : Nat) (l : List α) : (List.modifyNthTail f n l).length = l.length

theorem List.modifyNthTail_add {α : Type u_1} (f : List α → List α) (n : Nat) (l₁ : List α) (l₂ : List α) : List.modifyNthTail f (l₁.length + 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 ≤ l.length) : ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l₂ ∧ l₁.length = n ∧ List.modifyNthTail f n l = l₁ ++ f l₂

@[simp]

theorem List.modify_get?_length {α : Type u_1} (f : α → α) (n : Nat) (l : List α) : (List.modifyNth f n l).length = l.length

@[simp]

theorem List.get?_modifyNth_eq {α : Type u_1} (f : α → α) (n : Nat) (l : List α) : (List.modifyNth f n l).get? n = f <$> l.get? n

@[simp]

theorem List.get?_modifyNth_ne {α : Type u_1} (f : α → α) {m : Nat} {n : Nat} (l : List α) (h : m ≠ n) : (List.modifyNth f m l).get? n = l.get? n

theorem List.exists_of_modifyNth {α : Type u_1} (f : α → α) {n : Nat} {l : List α} (h : n < l.length) : ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ l₁.length = 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 α) : List.modifyNthTail f n l = List.take n l ++ f (List.drop n l)

theorem List.modifyNth_eq_take_drop {α : Type u_1} (f : α → α) (n : Nat) (l : List α) : List.modifyNth f n l = List.take n l ++ List.modifyHead f (List.drop n l)

theorem List.modifyNth_eq_take_cons_drop {α : Type u_1} (f : α → α) {n : Nat} {l : List α} (h : n < l.length) : List.modifyNth f n l = List.take n l ++ f (l.get ⟨n, h⟩) :: List.drop (n + 1) l

set

theorem List.set_eq_modifyNth {α : Type u_1} (a : α) (n : Nat) (l : List α) : l.set 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 < l.length) : l.set 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 = ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l

theorem List.modifyNth_eq_set_get {α : Type u_1} (f : α → α) {n : Nat} {l : List α} (h : n < l.length) : List.modifyNth f n l = l.set n (f (l.get ⟨n, h⟩))

theorem List.exists_of_set {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < l.length) : ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂

theorem List.exists_of_set' {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < l.length) : ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l.get ⟨n, h⟩ :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂

@[simp]

theorem List.get?_set_eq {α : Type u_1} (a : α) (n : Nat) (l : List α) : (l.set n a).get? n = (fun (x : α) => a) <$> l.get? n

theorem List.get?_set_eq_of_lt {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) : (l.set n a).get? n = some a

@[simp]

theorem List.get?_set_ne {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : m ≠ n) : (l.set m a).get? n = l.get? n

theorem List.get?_set {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) : (l.set m a).get? n = if m = n then (fun (x : α) => a) <$> l.get? n else l.get? n

theorem List.get?_set_of_lt {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : n < l.length) : (l.set m a).get? n = if m = n then some a else l.get? n

theorem List.get?_set_of_lt' {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : m < l.length) : (l.set m a).get? n = if m = n then some a else l.get? n

@[simp]

theorem List.set_eq_nil {α : Type u_1} (l : List α) (n : Nat) (a : α) : l.set n a = [] ↔ l = []

theorem List.set_comm {α : Type u_1} (a : α) (b : α) {n : Nat} {m : Nat} (l : List α) : n ≠ m → (l.set n a).set m b = (l.set m b).set n a

@[simp]

theorem List.set_set {α : Type u_1} (a : α) (b : α) (l : List α) (n : Nat) : (l.set n a).set n b = l.set n b

theorem List.get_set {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : n < (l.set m a).length) : (l.set m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, ⋯⟩

theorem List.mem_or_eq_of_mem_set {α : Type u_1} {l : List α} {n : Nat} {a : α} {b : α} : a ∈ l.set n b → a ∈ l ∨ a = b

theorem List.drop_set_of_lt {α : Type u_1} (a : α) {n : Nat} {m : Nat} (l : List α) (h : n < m) : List.drop m (l.set n a) = List.drop m l

theorem List.take_set_of_lt {α : Type u_1} (a : α) {n : Nat} {m : Nat} (l : List α) (h : m < n) : List.take m (l.set n a) = List.take m l

removeNth

theorem List.length_eraseIdx {α : Type u_1} {l : List α} {i : Nat} : i < l.length → (l.eraseIdx i).length = l.length - 1

@[deprecated List.length_eraseIdx]

theorem List.length_removeNth {α : Type u_1} {l : List α} {i : Nat} : i < l.length → (l.eraseIdx i).length = l.length - 1

Alias of List.length_eraseIdx.

tail

@[simp]

theorem List.length_tail {α : Type u_1} (l : List α) : l.tail.length = l.length - 1

all / any

@[simp]

theorem List.contains_nil {α : Type u_1} {a : α} [BEq α] : [].contains a = false

@[simp]

theorem List.contains_cons {α : Type u_1} {a : α} {as : List α} {x : α} [BEq α] : (a :: as).contains x = (x == a || as.contains x)

theorem List.contains_eq_any_beq {α : Type u_1} [BEq α] (l : List α) (a : α) : l.contains a = l.any fun (x : α) => a == x

theorem List.not_all_eq_any_not {α : Type u_1} (l : List α) (p : α → Bool) : (!l.all p) = l.any fun (a : α) => !p a

theorem List.not_any_eq_all_not {α : Type u_1} (l : List α) (p : α → Bool) : (!l.any p) = l.all fun (a : α) => !p a

theorem List.or_all_distrib_left {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (q || l.all p) = l.all fun (a : α) => q || p a

theorem List.or_all_distrib_right {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (l.all p || q) = l.all fun (a : α) => p a || q

theorem List.and_any_distrib_left {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (q && l.any p) = l.any fun (a : α) => q && p a

theorem List.and_any_distrib_right {α : Type u_1} (l : List α) (p : α → Bool) (q : Bool) : (l.any p && q) = l.any fun (a : α) => p a && q

theorem List.any_eq_not_all_not {α : Type u_1} (l : List α) (p : α → Bool) : l.any p = !l.all fun (x : α) => !p x

theorem List.all_eq_not_any_not {α : Type u_1} (l : List α) (p : α → Bool) : l.all p = !l.any fun (x : α) => !p x

reverse

@[simp]

theorem List.mem_reverseAux {α : Type u_1} {x : α} {as : List α} {bs : List α} : x ∈ as.reverseAux bs ↔ x ∈ as ∨ x ∈ bs

@[simp]

theorem List.mem_reverse {α : Type u_1} {x : α} {as : List α} : x ∈ as.reverse ↔ x ∈ as

insert

@[simp]

theorem List.insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : List.insert a l = l

@[simp]

theorem List.insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) : List.insert a l = a :: l

@[simp]

theorem List.mem_insert_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} : a ∈ List.insert b l ↔ a = b ∨ a ∈ l

@[simp]

theorem List.mem_insert_self {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : a ∈ List.insert a l

theorem List.mem_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (h : a ∈ l) : a ∈ List.insert b l

theorem List.eq_or_mem_of_mem_insert {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (h : a ∈ List.insert b l) : a = b ∨ a ∈ l

@[simp]

theorem List.length_insert_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : (List.insert a l).length = l.length

@[simp]

theorem List.length_insert_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : ¬a ∈ l) : (List.insert a l).length = l.length + 1

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) : List.eraseP p l = l

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 ∈ l → p a = true → (List.eraseP p l).length = l.length.pred

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 α) : (List.eraseP p l).Sublist l

theorem List.eraseP_subset {α : Type u_1} {p : α → Bool} (l : List α) : List.eraseP p l ⊆ l

theorem List.Sublist.eraseP : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool}, l₁.Sublist l₂ → (List.eraseP p l₁).Sublist (List.eraseP p l₂)

theorem List.mem_of_mem_eraseP {α : Type u_1} {a : α} {p : α → Bool} {l : List α} : a ∈ List.eraseP p l → a ∈ l

@[simp]

theorem List.mem_eraseP_of_neg {α : Type u_1} {p : α → Bool} {a : α} {l : List α} (pa : ¬p a = true) : a ∈ List.eraseP p l ↔ a ∈ l

theorem List.eraseP_map {β : Type u_1} {α : Type u_2} {p : α → Bool} (f : β → α) (l : List β) : List.eraseP p (List.map f l) = List.map f (List.eraseP (p ∘ f) l)

@[simp]

theorem List.extractP_eq_find?_eraseP {α : Type u_1} {p : α → Bool} (l : List α) : List.extractP p l = (List.find? p l, List.eraseP p l)

theorem List.extractP_eq_find?_eraseP.go {α : Type u_1} {p : α → Bool} (l : List α) (acc : Array α) (xs : List α) : l = acc.data ++ xs → List.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 : α) : [].erase a = []

theorem List.erase_cons {α : Type u_1} [BEq α] (a : α) (b : α) (l : List α) : (b :: l).erase a = if (b == a) = true then l else b :: l.erase a

@[simp]

theorem List.erase_cons_head {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l

@[simp]

theorem List.erase_cons_tail {α : Type u_1} [BEq α] {a : α} {b : α} (l : List α) (h : ¬(b == a) = true) : (b :: l).erase a = b :: l.erase a

theorem List.erase_eq_eraseP' {α : Type u_1} [BEq α] (a : α) (l : List α) : l.erase a = List.eraseP (fun (x : α) => x == a) l

theorem List.erase_eq_eraseP {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : l.erase a = List.eraseP (fun (x : α) => a == x) l

theorem List.erase_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} : ¬a ∈ l → l.erase 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₂ ∧ l.erase a = l₁ ++ l₂

@[simp]

theorem List.length_erase_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) : (l.erase a).length = l.length.pred

theorem List.erase_append_left {α : Type u_1} [BEq α] {a : α} [LawfulBEq α] {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) : (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

theorem List.erase_append_right {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : ¬a ∈ l₁) : (l₁ ++ l₂).erase a = l₁ ++ l₂.erase a

theorem List.erase_sublist {α : Type u_1} [BEq α] (a : α) (l : List α) : (l.erase a).Sublist l

theorem List.erase_subset {α : Type u_1} [BEq α] (a : α) (l : List α) : l.erase a ⊆ l

theorem List.Sublist.erase {α : Type u_1} [BEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) : (l₁.erase a).Sublist (l₂.erase a)

@[deprecated List.Sublist.erase]

theorem List.sublist.erase {α : Type u_1} [BEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) : (l₁.erase a).Sublist (l₂.erase a)

Alias of List.Sublist.erase.

theorem List.mem_of_mem_erase {α : Type u_1} [BEq α] {a : α} {b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l

@[simp]

theorem List.mem_erase_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} {l : List α} (ab : a ≠ b) : a ∈ l.erase b ↔ a ∈ l

theorem List.erase_comm {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (b : α) (l : List α) : (l.erase a).erase b = (l.erase b).erase a

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 α) : (List.filter p l).Sublist l

@[simp]

theorem List.partition_eq_filter_filter {α : Type u_1} (p : α → Bool) (l : List α) : List.partition p l = (List.filter p l, List.filter (not ∘ p) l)

theorem List.partition_eq_filter_filter.aux {α : Type u_1} (p : α → Bool) (l : List α) {as : List α} {bs : List α} : List.partition.loop p l (as, bs) = (as.reverse ++ List.filter p l, bs.reverse ++ List.filter (not ∘ p) l)

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 β) : List.filterMap f [] = []

@[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) : List.filterMap f (a :: l) = List.filterMap f l

theorem List.filterMap_cons_some {α : Type u_1} {β : Type u_2} (f : α → Option β) (a : α) (l : List α) {b : β} (h : f a = some b) : List.filterMap f (a :: l) = b :: List.filterMap f l

theorem List.filterMap_append {α : Type u_1} {β : Type u_2} (l : List α) (l' : List α) (f : α → Option β) : List.filterMap f (l ++ l') = List.filterMap f l ++ List.filterMap f l'

@[simp]

theorem List.filterMap_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) : List.filterMap (some ∘ f) = List.map f

@[simp]

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 : α) => (f x).bind 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

@[simp]

theorem List.filterMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → Option γ) (l : List α) : List.filterMap g (List.map f l) = List.filterMap (g ∘ f) l

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 β) => b.isSome) (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 α)) : List.filterMap f L.join = (List.map (List.filterMap f) L).join

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 α) : List.map g (List.filterMap f l) = l

theorem List.length_filter_le {α : Type u_1} (p : α → Bool) (l : List α) : (List.filter p l).length ≤ l.length

theorem List.length_filterMap_le {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : (List.filterMap f l).length ≤ l.length

theorem List.Sublist.filterMap {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : α → Option β) (s : l₁.Sublist l₂) : (List.filterMap f l₁).Sublist (List.filterMap f l₂)

theorem List.Sublist.filter {α : Type u_1} (p : α → Bool) {l₁ : List α} {l₂ : List α} (s : l₁.Sublist l₂) : (List.filter p l₁).Sublist (List.filter p l₂)

theorem List.map_filter {β : Type u_1} {α : Type u_2} {p : α → Bool} (f : β → α) (l : List β) : List.filter p (List.map f l) = List.map f (List.filter (p ∘ f) l)

@[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

@[simp]

theorem List.filter_eq_self : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = l ↔ ∀ (a : α), a ∈ l → p a = true

@[simp]

theorem List.filter_length_eq_length : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.filter p l).length = l.length ↔ ∀ (a : α), a ∈ l → p a = true

find?

theorem List.find?_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), p a = true → List.find? p (a :: l) = some a

theorem List.find?_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), ¬p a = true → List.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 a → p a = true

@[simp]

theorem List.mem_of_find?_eq_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → a ∈ 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) : List.findIdx p [] = 0

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 : xs.get? (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 < xs.length} : p (xs.get ⟨List.findIdx p xs, w⟩) = true

theorem List.findIdx_lt_length_of_exists {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∃ (x : α), x ∈ xs ∧ p x = true) : List.findIdx p xs < xs.length

theorem List.findIdx_get?_eq_get_of_exists {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∃ (x : α), x ∈ xs ∧ p x = true) : xs.get? (List.findIdx p xs) = some (xs.get ⟨List.findIdx p xs, ⋯⟩)

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) : List.findIdx? p xs = some i ↔ List.map p (List.take (i + 1) xs) = List.replicate i false ++ [true]

theorem List.findIdx?_of_eq_some {α : Type u_1} {i : Nat} {xs : List α} {p : α → Bool} (w : List.findIdx? p xs = some i) : match xs.get? 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 xs.get? 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 + xs.length) (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}, l₁.Sublist l₂ → List.Pairwise R l₂ → List.Pairwise R l₁

theorem List.pairwise_map {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α_1} {R : α_1 → α_1 → Prop} {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 l.reverse ↔ 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 b → S a b) {l : List α} : List.Pairwise R l → List.Pairwise S l

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) : List.replaceF p (a :: l) = a :: List.replaceF p l

theorem List.replaceF_of_forall_none {α : Type u_1} {p : α → Option α} {l : List α} (h : ∀ (a : α), a ∈ l → p a = none) : List.replaceF p l = l

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.replaceF f l).length = l.length

disjoint

theorem List.disjoint_symm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ → l₂.Disjoint l₁

theorem List.disjoint_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ l₂.Disjoint l₁

theorem List.disjoint_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₁ → ¬a ∈ l₂

theorem List.disjoint_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₂ → ¬a ∈ l₁

theorem List.disjoint_iff_ne : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → a ≠ b

theorem List.disjoint_of_subset_left : ∀ {α : Type u_1} {l₁ l l₂ : List α}, l₁ ⊆ l → l.Disjoint l₂ → l₁.Disjoint l₂

theorem List.disjoint_of_subset_right : ∀ {α : Type u_1} {l₂ l l₁ : List α}, l₂ ⊆ l → l₁.Disjoint l → l₁.Disjoint l₂

theorem List.disjoint_of_disjoint_cons_left : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂ → l₁.Disjoint l₂

theorem List.disjoint_of_disjoint_cons_right : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁.Disjoint (a :: l₂) → l₁.Disjoint l₂

@[simp]

theorem List.disjoint_nil_left {α : Type u_1} (l : List α) : [].Disjoint l

@[simp]

theorem List.disjoint_nil_right {α : Type u_1} (l : List α) : l.Disjoint []

@[simp]

theorem List.singleton_disjoint : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Disjoint l ↔ ¬a ∈ l

@[simp]

theorem List.disjoint_singleton : ∀ {α : Type u_1} {l : List α} {a : α}, l.Disjoint [a] ↔ ¬a ∈ l

@[simp]

theorem List.disjoint_append_left : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l ↔ l₁.Disjoint l ∧ l₂.Disjoint l

@[simp]

theorem List.disjoint_append_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) ↔ l.Disjoint l₁ ∧ l.Disjoint l₂

@[simp]

theorem List.disjoint_cons_left : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂ ↔ ¬a ∈ l₂ ∧ l₁.Disjoint l₂

@[simp]

theorem List.disjoint_cons_right : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁.Disjoint (a :: l₂) ↔ ¬a ∈ l₁ ∧ l₁.Disjoint l₂

theorem List.disjoint_of_disjoint_append_left_left : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l → l₁.Disjoint l

theorem List.disjoint_of_disjoint_append_left_right : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l → l₂.Disjoint l

theorem List.disjoint_of_disjoint_append_right_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) → l.Disjoint l₁

theorem List.disjoint_of_disjoint_append_right_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) → l.Disjoint l₂

foldl / foldr

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} [BEq α] (l₁ : List α) (l₂ : List α) : l₁ ∪ l₂ = List.foldr List.insert l₂ l₁

@[simp]

theorem List.nil_union {α : Type u_1} [BEq α] (l : List α) : [] ∪ l = l

@[simp]

theorem List.cons_union {α : Type u_1} [BEq α] (a : α) (l₁ : List α) (l₂ : List α) : a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂)

@[simp]

theorem List.mem_union_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {l₁ : List α} {l₂ : List α} : x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂

inter

theorem List.inter_def {α : Type u_1} [BEq α] (l₁ : List α) (l₂ : List α) : l₁ ∩ l₂ = List.filter (fun (x : α) => List.elem x l₂) l₁

@[simp]

theorem List.mem_inter_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {l₁ : List α} {l₂ : List α} : x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂

product

@[simp]

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

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

leftpad

@[simp]

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

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 α) : List.replicate (n - l.length) a <+: List.leftpad n a l

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

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) : (l₁ ++ l₂).forM f = do l₁.forM f l₂.forM f

diff

@[simp]

theorem List.diff_nil {α : Type u_1} [BEq α] (l : List α) : l.diff [] = l

@[simp]

theorem List.diff_cons {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.erase a).diff l₂

theorem List.diff_cons_right {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.diff l₂).erase a

theorem List.diff_erase {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (l₂ : List α) (a : α) : (l₁.diff l₂).erase a = (l₁.erase a).diff l₂

@[simp]

theorem List.nil_diff {α : Type u_1} [BEq α] [LawfulBEq α] (l : List α) : [].diff l = []

theorem List.cons_diff {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l₁ : List α) (l₂ : List α) : (a :: l₁).diff l₂ = if a ∈ l₂ then l₁.diff (l₂.erase a) else a :: l₁.diff l₂

theorem List.cons_diff_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₂ : List α} (h : a ∈ l₂) (l₁ : List α) : (a :: l₁).diff l₂ = l₁.diff (l₂.erase a)

theorem List.cons_diff_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₂ : List α} (h : ¬a ∈ l₂) (l₁ : List α) : (a :: l₁).diff l₂ = a :: l₁.diff l₂

theorem List.diff_eq_foldl {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (l₂ : List α) : l₁.diff l₂ = List.foldl List.erase l₁ l₂

@[simp]

theorem List.diff_append {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (l₂ : List α) (l₃ : List α) : l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃

theorem List.diff_sublist {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (l₂ : List α) : (l₁.diff l₂).Sublist l₁

theorem List.diff_subset {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (l₂ : List α) : l₁.diff l₂ ⊆ l₁

theorem List.mem_diff_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} {l₂ : List α} : a ∈ l₁ → ¬a ∈ l₂ → a ∈ l₁.diff l₂

theorem List.Sublist.diff_right {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ : List α} {l₂ : List α} {l₃ : List α} : l₁.Sublist l₂ → (l₁.diff l₃).Sublist (l₂.diff l₃)

theorem List.Sublist.erase_diff_erase_sublist {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {l₁ : List α} {l₂ : List α} : l₁.Sublist l₂ → ((l₂.erase a).diff (l₁.erase a)).Sublist (l₂.diff 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₁ <:+: l₂.concat 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₂ → l₁.Sublist 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₂ → l₁.Sublist 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₂ → l₁.Sublist 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 α}, l₁.reverse <:+ l₂.reverse ↔ l₁ <+: l₂

@[simp]

theorem List.reverse_prefix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂

@[simp]

theorem List.reverse_infix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <:+: l₂.reverse ↔ l₁ <:+: l₂

theorem List.IsInfix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.length ≤ l₂.length

theorem List.IsPrefix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length ≤ l₂.length

theorem List.IsSuffix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length ≤ l₂.length

@[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₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.IsPrefix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.IsSuffix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length = l₂.length → l₁ = l₂

theorem List.prefix_of_prefix_length_le {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} : l₁ <+: l₃ → l₂ <+: l₃ → l₁.length ≤ l₂.length → 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₃ → l₁.length ≤ l₂.length → 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 ∈ L → l <:+: L.join

theorem List.prefix_append_right_inj : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂

@[simp]

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 α) : List.take n l <+: l

theorem List.drop_suffix {α : Type u_1} (n : Nat) (l : List α) : List.drop n l <:+ l

theorem List.take_sublist {α : Type u_1} (n : Nat) (l : List α) : (List.take n l).Sublist l

theorem List.drop_sublist {α : Type u_1} (n : Nat) (l : List α) : (List.drop n l).Sublist l

theorem List.take_subset {α : Type u_1} (n : Nat) (l : List α) : List.take n l ⊆ l

theorem List.drop_subset {α : Type u_1} (n : Nat) (l : List α) : List.drop n l ⊆ l

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₂) : List.filter p l₁ <+: List.filter p l₂

theorem List.IsSuffix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+ l₂) : List.filter p l₁ <:+ List.filter p l₂

theorem List.IsInfix.filter {α : Type u_1} (p : α → Bool) ⦃l₁ : List α⦄ ⦃l₂ : List α⦄ (h : l₁ <:+: l₂) : List.filter p l₁ <:+: List.filter p l₂

drop

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 α} : l.Nodup → m ≤ n → (List.take m l).Disjoint (List.drop n l)

takeWhile and dropWhile

@[simp]

theorem List.takeWhile_append_dropWhile {α : Type u_1} (p : α → Bool) (l : List α) : List.takeWhile p l ++ List.dropWhile p l = l

theorem List.dropWhile_append {α : Type u_1} {p : α → Bool} {xs : List α} {ys : List α} : List.dropWhile p (xs ++ ys) = if (List.dropWhile p xs).isEmpty = 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)) : List.Chain R b l

theorem List.Chain.imp' {α : Type u_1} {R : α → α → Prop} {S : α → α → Prop} (HRS : ∀ ⦃a b : α⦄, R a b → S a b) {a : α} {b : α} (Hab : ∀ ⦃c : α⦄, R a c → S b c) {l : List α} (p : List.Chain R a l) : List.Chain S b l

theorem List.Chain.imp {α : Type u_1} {R : α → α → Prop} {S : α → α → Prop} (H : ∀ (a b : α), R a b → S a b) {a : α} {l : List α} (p : List.Chain R a l) : List.Chain S 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) : (List.range' s n step).length = n

@[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

@[simp]

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.range' s m step).Sublist (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.range'_subset_right_1 {s : Nat} {m : Nat} {n : Nat} : List.range' s m ⊆ List.range' s n ↔ m ≤ n

theorem List.get?_range' (s : Nat) (step : Nat) {m : Nat} {n : Nat} : m < n → (List.range' s n step).get? m = some (s + step * m)

@[simp]

theorem List.get_range' {n : Nat} {m : Nat} {step : Nat} (i : Nat) (H : i < (List.range' n m step).length) : (List.range' n m step).get ⟨i, 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_loop_range' (s : Nat) (n : Nat) : List.range.loop s (List.range' s n) = List.range' 0 (n + s)

theorem List.range_eq_range' (n : Nat) : List.range n = List.range' 0 n

theorem List.range_succ_eq_map (n : Nat) : List.range (n + 1) = 0 :: List.map Nat.succ (List.range 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]

theorem List.length_range (n : Nat) : (List.range n).length = n

@[simp]

theorem List.range_eq_nil {n : Nat} : List.range n = [] ↔ n = 0

@[simp]

theorem List.range_sublist {m : Nat} {n : Nat} : (List.range m).Sublist (List.range n) ↔ m ≤ n

@[simp]

theorem List.range_subset {m : Nat} {n : Nat} : List.range m ⊆ List.range n ↔ m ≤ n

@[simp]

theorem List.mem_range {m : Nat} {n : Nat} : m ∈ List.range n ↔ m < n

theorem List.not_mem_range_self {n : Nat} : ¬n ∈ List.range n

theorem List.self_mem_range_succ (n : Nat) : n ∈ List.range (n + 1)

theorem List.get?_range {m : Nat} {n : Nat} (h : m < n) : (List.range n).get? m = some m

theorem List.range_succ (n : Nat) : List.range n.succ = List.range n ++ [n]

@[simp]

theorem List.range_zero : List.range 0 = []

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)

theorem List.iota_eq_reverse_range' (n : Nat) : List.iota n = (List.range' 1 n).reverse

@[simp]

theorem List.length_iota (n : Nat) : (List.iota n).length = n

@[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.range' s n).reverse = List.map (fun (x : Nat) => s + n - 1 - x) (List.range n)

@[simp]

theorem List.get_range {n : Nat} (i : Nat) (H : i < (List.range n).length) : (List.range n).get ⟨i, H⟩ = i

enum, enumFrom

@[simp]

theorem List.enumFrom_map_fst {α : Type u_1} (n : Nat) (l : List α) : List.map Prod.fst (List.enumFrom n l) = List.range' n l.length

@[simp]

theorem List.enum_map_fst {α : Type u_1} (l : List α) : List.map Prod.fst l.enum = List.range l.length

@[simp]

theorem List.enumFrom_length {α : Type u_1} {n : Nat} {l : List α} : (List.enumFrom n l).length = l.length

@[simp]

theorem List.enum_length : ∀ {α : Type u_1} {l : List α}, l.enum.length = l.length

maximum?

@[simp]

theorem List.maximum?_nil {α : Type u_1} [Max α] : [].maximum? = none

theorem List.maximum?_cons {α : Type u_1} {x : α} [Max α] {xs : List α} : (x :: xs).maximum? = some (List.foldl max x xs)

@[simp]

theorem List.maximum?_eq_none_iff {α : Type u_1} {xs : List α} [Max α] : xs.maximum? = 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 α} : xs.maximum? = some a → a ∈ 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 α} : xs.maximum? = some a → ∀ (x : α), a ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ 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 α} : xs.maximum? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a

theorem List.maximum?_eq_some_iff' {a : Nat} {xs : List Nat} : xs.maximum? = some a ↔ a ∈ xs ∧ ∀ (b : Nat), b ∈ xs → b ≤ 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 α] : List.indexesOf x [] = []

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 α] : List.indexOf x [] = 0

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) : List.indexOf x xs ∈ List.indexesOf x xs

theorem List.merge_loop_nil_left {α : Type u_1} (s : α → α → Bool) (r : List α) (t : List α) : List.merge.loop s [] r t = t.reverseAux r

theorem List.merge_loop_nil_right {α : Type u_1} (s : α → α → Bool) (l : List α) (t : List α) : List.merge.loop s l [] t = t.reverseAux l

theorem List.merge_loop {α : Type u_1} (s : α → α → Bool) (l : List α) (r : List α) (t : List α) : List.merge.loop s l r t = t.reverseAux (List.merge s l r)

@[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 α) : (List.merge s l r).length = l.length + r.length

@[simp]

theorem List.mem_merge {α : Type u_1} {x : α} {l : List α} {r : List α} {s : α → α → Bool} : x ∈ List.merge s l r ↔ x ∈ l ∨ x ∈ r

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

lt

theorem List.lt_irrefl' {α : Type u_1} [LT α] (lt_irrefl : ∀ (x : α), ¬x < x) (l : List α) : ¬l < l

theorem List.lt_trans' {α : Type u_1} [LT α] [DecidableRel LT.lt] (lt_trans : ∀ {x y z : α}, x < y → y < z → x < z) (le_trans : ∀ {x y z : α}, ¬x < y → ¬y < z → ¬x < z) {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃

theorem List.lt_antisymm' {α : Type u_1} [LT α] (lt_antisymm : ∀ {x y : α}, ¬x < y → ¬y < x → x = y) {l₁ : List α} {l₂ : List α} (h₁ : ¬l₁ < l₂) (h₂ : ¬l₂ < l₁) : l₁ = l₂