Basic properties of lists

instance List.uniqueOfIsEmpty {α : Type u} [IsEmpty α] : Unique (List α)

There is only one list of an empty type

Equations

• List.uniqueOfIsEmpty = let __src := instInhabitedList; { toInhabited := __src, uniq := ⋯ }

instance List.instLawfulIdentityListAppendInstAppendListNil {α : Type u} : Std.LawfulIdentity Append.append []

Equations

• ⋯ = ⋯

instance List.instAssociativeListAppendInstAppendList {α : Type u} : Std.Associative Append.append

Equations

• ⋯ = ⋯

@[simp]

theorem List.cons_injective {α : Type u} {a : α} : Function.Injective (List.cons a)

theorem List.singleton_injective {α : Type u} : Function.Injective fun (a : α) => [a]

theorem List.singleton_inj {α : Type u} {a : α} {b : α} : [a] = [b] ↔ a = b

theorem List.set_of_mem_cons {α : Type u} (l : List α) (a : α) : {x : α | x ∈ a :: l} = insert a {x : α | x ∈ l}

mem

theorem Decidable.List.eq_or_ne_mem_of_mem {α : Type u} [DecidableEq α] {a : α} {b : α} {l : List α} (h : a ∈ b :: l) : a = b ∨ a ≠ b ∧ a ∈ l

theorem List.mem_pair {α : Type u} {a : α} {b : α} {c : α} : a ∈ [b, c] ↔ a = b ∨ a = c

@[deprecated List.append_of_mem]

theorem List.mem_split {α : Type u_1} {a : α} {l : List α} : a ∈ l → ∃ (s : List α), ∃ (t : List α), l = s ++ a :: t

Alias of List.append_of_mem.

@[simp]

theorem List.mem_map_of_injective {α : Type u} {β : Type v} {f : α → β} (H : Function.Injective f) {a : α} {l : List α} : f a ∈ List.map f l ↔ a ∈ l

@[simp]

theorem Function.Involutive.exists_mem_and_apply_eq_iff {α : Type u} {f : α → α} (hf : Function.Involutive f) (x : α) (l : List α) : (∃ (y : α), y ∈ l ∧ f y = x) ↔ f x ∈ l

theorem List.mem_map_of_involutive {α : Type u} {f : α → α} (hf : Function.Involutive f) {a : α} {l : List α} : a ∈ List.map f l ↔ f a ∈ l

theorem List.map_bind {α : Type u} {β : Type v} {γ : Type w} (g : β → List γ) (f : α → β) (l : List α) : List.bind (List.map f l) g = List.bind l fun (a : α) => g (f a)

length

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

Alias of the reverse direction of List.length_pos.

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

Alias of the forward direction of List.length_pos.

theorem List.length_pos_iff_ne_nil {α : Type u} {l : List α} : 0 < List.length l ↔ l ≠ []

theorem List.exists_of_length_succ {α : Type u} {n : ℕ} (l : List α) : List.length l = n + 1 → ∃ (h : α), ∃ (t : List α), l = h :: t

@[simp]

theorem List.length_injective_iff {α : Type u} : Function.Injective List.length ↔ Subsingleton α

@[simp]

theorem List.length_injective {α : Type u} [Subsingleton α] : Function.Injective List.length

theorem List.length_eq_two {α : Type u} {l : List α} : List.length l = 2 ↔ ∃ (a : α), ∃ (b : α), l = [a, b]

theorem List.length_eq_three {α : Type u} {l : List α} : List.length l = 3 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), l = [a, b, c]

set-theoretic notation of lists

instance List.instSingletonList {α : Type u} : Singleton α (List α)

Equations

• List.instSingletonList = { singleton := fun (x : α) => [x] }

instance List.instInsertList {α : Type u} [DecidableEq α] : Insert α (List α)

Equations

• List.instInsertList = { insert := List.insert }

instance List.instIsLawfulSingletonListInstEmptyCollectionListInstInsertListInstSingletonList {α : Type u} [DecidableEq α] : IsLawfulSingleton α (List α)

Equations

• ⋯ = ⋯

theorem List.singleton_eq {α : Type u} (x : α) : {x} = [x]

theorem List.insert_neg {α : Type u} [DecidableEq α] {x : α} {l : List α} (h : ¬x ∈ l) : insert x l = x :: l

theorem List.insert_pos {α : Type u} [DecidableEq α] {x : α} {l : List α} (h : x ∈ l) : insert x l = l

theorem List.doubleton_eq {α : Type u} [DecidableEq α] {x : α} {y : α} (h : x ≠ y) : {x, y} = [x, y]

bounded quantifiers over lists

theorem List.forall_mem_of_forall_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : List α} (h : ∀ (x : α), x ∈ a :: l → p x) (x : α) : x ∈ l → p x

theorem List.exists_mem_cons_of {α : Type u} {p : α → Prop} {a : α} (l : List α) (h : p a) : ∃ (x : α), x ∈ a :: l ∧ p x

theorem List.exists_mem_cons_of_exists {α : Type u} {p : α → Prop} {a : α} {l : List α} : (∃ (x : α), x ∈ l ∧ p x) → ∃ (x : α), x ∈ a :: l ∧ p x

theorem List.or_exists_of_exists_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : List α} : (∃ (x : α), x ∈ a :: l ∧ p x) → p a ∨ ∃ (x : α), x ∈ l ∧ p x

theorem List.exists_mem_cons_iff {α : Type u} (p : α → Prop) (a : α) (l : List α) : (∃ (x : α), x ∈ a :: l ∧ p x) ↔ p a ∨ ∃ (x : α), x ∈ l ∧ p x

list subset

instance List.instIsTransListSubsetInstHasSubsetList {α : Type u} : IsTrans (List α) Subset

Equations

• ⋯ = ⋯

@[deprecated List.subset_append_of_subset_right]

theorem List.subset_append_of_subset_right' {α : Type u} (l : List α) (l₁ : List α) (l₂ : List α) : l ⊆ l₂ → l ⊆ l₁ ++ l₂

theorem List.cons_subset_of_subset_of_mem {α : Type u} {a : α} {l : List α} {m : List α} (ainm : a ∈ m) (lsubm : l ⊆ m) : a :: l ⊆ m

theorem List.append_subset_of_subset_of_subset {α : Type u} {l₁ : List α} {l₂ : List α} {l : List α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) : l₁ ++ l₂ ⊆ l

theorem List.eq_nil_of_subset_nil {α : Type u_1} {l : List α} : l ⊆ [] → l = []

Alias of the forward direction of List.subset_nil.

theorem List.map_subset_iff {α : Type u} {β : Type v} {l₁ : List α} {l₂ : List α} (f : α → β) (h : Function.Injective f) : List.map f l₁ ⊆ List.map f l₂ ↔ l₁ ⊆ l₂

append

theorem List.append_eq_has_append {α : Type u} {L₁ : List α} {L₂ : List α} : List.append L₁ L₂ = L₁ ++ L₂

@[deprecated List.append_eq_cons]

theorem List.append_eq_cons_iff : ∀ {α : 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

Alias of List.append_eq_cons.

@[deprecated List.cons_eq_append]

theorem List.cons_eq_append_iff : ∀ {α : Type u_1} {x : α} {c a b : List α}, x :: c = a ++ b ↔ a = [] ∧ b = x :: c ∨ ∃ (a' : List α), a = x :: a' ∧ c = a' ++ b

Alias of List.cons_eq_append.

@[deprecated List.append_cancel_left]

theorem List.append_left_cancel {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = as ++ cs) : bs = cs

Alias of List.append_cancel_left.

@[deprecated List.append_cancel_right]

theorem List.append_right_cancel {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = cs ++ bs) : as = cs

Alias of List.append_cancel_right.

@[simp]

theorem List.append_left_eq_self {α : Type u} {x : List α} {y : List α} : x ++ y = y ↔ x = []

@[simp]

theorem List.self_eq_append_left {α : Type u} {x : List α} {y : List α} : y = x ++ y ↔ x = []

@[simp]

theorem List.append_right_eq_self {α : Type u} {x : List α} {y : List α} : x ++ y = x ↔ y = []

@[simp]

theorem List.self_eq_append_right {α : Type u} {x : List α} {y : List α} : x = x ++ y ↔ y = []

theorem List.append_right_injective {α : Type u} (s : List α) : Function.Injective fun (t : List α) => s ++ t

theorem List.append_left_injective {α : Type u} (t : List α) : Function.Injective fun (s : List α) => s ++ t

replicate

@[simp]

theorem List.replicate_zero {α : Type u} (a : α) : List.replicate 0 a = []

theorem List.replicate_one {α : Type u} (a : α) : List.replicate 1 a = [a]

theorem List.eq_replicate_length {α : Type u} {a : α} {l : List α} : l = List.replicate (List.length l) a ↔ ∀ (b : α), b ∈ l → b = a

theorem List.replicate_add {α : Type u} (m : ℕ) (n : ℕ) (a : α) : List.replicate (m + n) a = List.replicate m a ++ List.replicate n a

theorem List.replicate_succ' {α : Type u} (n : ℕ) (a : α) : List.replicate (n + 1) a = List.replicate n a ++ [a]

theorem List.replicate_subset_singleton {α : Type u} (n : ℕ) (a : α) : List.replicate n a ⊆ [a]

theorem List.subset_singleton_iff {α : Type u} {a : α} {L : List α} : L ⊆ [a] ↔ ∃ (n : ℕ), L = List.replicate n a

@[simp]

theorem List.map_replicate {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (a : α) : List.map f (List.replicate n a) = List.replicate n (f a)

@[simp]

theorem List.tail_replicate {α : Type u} (a : α) (n : ℕ) : List.tail (List.replicate n a) = List.replicate (n - 1) a

@[simp]

theorem List.join_replicate_nil {α : Type u} (n : ℕ) : List.join (List.replicate n []) = []

theorem List.replicate_right_injective {α : Type u} {n : ℕ} (hn : n ≠ 0) : Function.Injective (List.replicate n)

theorem List.replicate_right_inj {α : Type u} {a : α} {b : α} {n : ℕ} (hn : n ≠ 0) : List.replicate n a = List.replicate n b ↔ a = b

@[simp]

theorem List.replicate_right_inj' {α : Type u} {a : α} {b : α} {n : ℕ} : List.replicate n a = List.replicate n b ↔ n = 0 ∨ a = b

theorem List.replicate_left_injective {α : Type u} (a : α) : Function.Injective fun (x : ℕ) => List.replicate x a

@[simp]

theorem List.replicate_left_inj {α : Type u} {a : α} {n : ℕ} {m : ℕ} : List.replicate n a = List.replicate m a ↔ n = m

@[simp]

theorem List.head_replicate {α : Type u} (n : ℕ) (a : α) (h : List.replicate n a ≠ []) : List.head (List.replicate n a) h = a

pure

theorem List.mem_pure {α : Type u_2} (x : α) (y : α) : x ∈ pure y ↔ x = y

bind

@[simp]

theorem List.bind_eq_bind {α : Type u_2} {β : Type u_2} (f : α → List β) (l : List α) : l >>= f = List.bind l f

concat

@[deprecated List.concat_eq_append]

theorem List.concat_eq_append' {α : Type u} (a : α) (l : List α) : List.concat l a = l ++ [a]

@[deprecated List.length_concat]

theorem List.length_concat' {α : Type u} (a : α) (l : List α) : List.length (List.concat l a) = Nat.succ (List.length l)

reverse

theorem List.reverse_cons' {α : Type u} (a : α) (l : List α) : List.reverse (a :: l) = List.concat (List.reverse l) a

theorem List.reverse_concat' {α : Type u} (l : List α) (a : α) : List.reverse (l ++ [a]) = a :: List.reverse l

theorem List.reverse_singleton {α : Type u} (a : α) : List.reverse [a] = [a]

@[simp]

theorem List.reverse_involutive {α : Type u} : Function.Involutive List.reverse

@[simp]

theorem List.reverse_injective {α : Type u} : Function.Injective List.reverse

theorem List.reverse_surjective {α : Type u} : Function.Surjective List.reverse

theorem List.reverse_bijective {α : Type u} : Function.Bijective List.reverse

@[simp]

theorem List.reverse_inj {α : Type u} {l₁ : List α} {l₂ : List α} : List.reverse l₁ = List.reverse l₂ ↔ l₁ = l₂

theorem List.reverse_eq_iff {α : Type u} {l : List α} {l' : List α} : List.reverse l = l' ↔ l = List.reverse l'

theorem List.concat_eq_reverse_cons {α : Type u} (a : α) (l : List α) : List.concat l a = List.reverse (a :: List.reverse l)

theorem List.map_reverse {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.map f (List.reverse l) = List.reverse (List.map f l)

theorem List.map_reverseAux {α : Type u} {β : Type v} (f : α → β) (l₁ : List α) (l₂ : List α) : List.map f (List.reverseAux l₁ l₂) = List.reverseAux (List.map f l₁) (List.map f l₂)

@[simp]

theorem List.reverse_replicate {α : Type u} (n : ℕ) (a : α) : List.reverse (List.replicate n a) = List.replicate n a

empty

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

dropLast

getLast

@[simp]

theorem List.getLast_cons {α : Type u} {a : α} {l : List α} (h : l ≠ []) : List.getLast (a :: l) ⋯ = List.getLast l h

theorem List.getLast_append_singleton {α : Type u} {a : α} (l : List α) : List.getLast (l ++ [a]) ⋯ = a

theorem List.getLast_append' {α : Type u} (l₁ : List α) (l₂ : List α) (h : l₂ ≠ []) : List.getLast (l₁ ++ l₂) ⋯ = List.getLast l₂ h

theorem List.getLast_concat' {α : Type u} {a : α} (l : List α) : List.getLast (List.concat l a) ⋯ = a

@[simp]

theorem List.getLast_singleton' {α : Type u} (a : α) : List.getLast [a] ⋯ = a

theorem List.getLast_cons_cons {α : Type u} (a₁ : α) (a₂ : α) (l : List α) : List.getLast (a₁ :: a₂ :: l) ⋯ = List.getLast (a₂ :: l) ⋯

theorem List.dropLast_append_getLast {α : Type u} {l : List α} (h : l ≠ []) : List.dropLast l ++ [List.getLast l h] = l

theorem List.getLast_congr {α : Type u} {l₁ : List α} {l₂ : List α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) : List.getLast l₁ h₁ = List.getLast l₂ h₂

theorem List.getLast_replicate_succ {α : Type u} (m : ℕ) (a : α) : List.getLast (List.replicate (m + 1) a) ⋯ = a

getLast?

@[simp]

theorem List.getLast?_cons_cons {α : Type u} (a : α) (b : α) (l : List α) : List.getLast? (a :: b :: l) = List.getLast? (b :: l)

@[simp]

theorem List.getLast?_isNone {α : Type u} {l : List α} : Option.isNone (List.getLast? l) = true ↔ l = []

@[simp]

theorem List.getLast?_isSome {α : Type u} {l : List α} : Option.isSome (List.getLast? l) = true ↔ l ≠ []

theorem List.mem_getLast?_eq_getLast {α : Type u} {l : List α} {x : α} : x ∈ List.getLast? l → ∃ (h : l ≠ []), x = List.getLast l h

theorem List.getLast?_eq_getLast_of_ne_nil {α : Type u} {l : List α} (h : l ≠ []) : List.getLast? l = some (List.getLast l h)

theorem List.mem_getLast?_cons {α : Type u} {x : α} {y : α} {l : List α} : x ∈ List.getLast? l → x ∈ List.getLast? (y :: l)

theorem List.mem_of_mem_getLast? {α : Type u} {l : List α} {a : α} (ha : a ∈ List.getLast? l) : a ∈ l

theorem List.dropLast_append_getLast? {α : Type u} {l : List α} (a : α) : a ∈ List.getLast? l → List.dropLast l ++ [a] = l

theorem List.getLastI_eq_getLast? {α : Type u} [Inhabited α] (l : List α) : List.getLastI l = Option.iget (List.getLast? l)

@[simp]

theorem List.getLast?_append_cons {α : Type u} (l₁ : List α) (a : α) (l₂ : List α) : List.getLast? (l₁ ++ a :: l₂) = List.getLast? (a :: l₂)

theorem List.getLast?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} : l₂ ≠ [] → List.getLast? (l₁ ++ l₂) = List.getLast? l₂

theorem List.getLast?_append {α : Type u} {l₁ : List α} {l₂ : List α} {x : α} (h : x ∈ List.getLast? l₂) : x ∈ List.getLast? (l₁ ++ l₂)

head(!?) and tail

@[simp]

theorem List.head_cons_tail {α : Type u} (x : List α) (h : x ≠ []) : List.head x h :: List.tail x = x

theorem List.head!_eq_head? {α : Type u} [Inhabited α] (l : List α) : List.head! l = Option.iget (List.head? l)

theorem List.surjective_head! {α : Type u} [Inhabited α] : Function.Surjective List.head!

theorem List.surjective_head? {α : Type u} : Function.Surjective List.head?

theorem List.surjective_tail {α : Type u} : Function.Surjective List.tail

theorem List.eq_cons_of_mem_head? {α : Type u} {x : α} {l : List α} : x ∈ List.head? l → l = x :: List.tail l

theorem List.mem_of_mem_head? {α : Type u} {x : α} {l : List α} (h : x ∈ List.head? l) : x ∈ l

@[simp]

theorem List.head!_cons {α : Type u} [Inhabited α] (a : α) (l : List α) : List.head! (a :: l) = a

@[simp]

theorem List.head!_append {α : Type u} [Inhabited α] (t : List α) {s : List α} (h : s ≠ []) : List.head! (s ++ t) = List.head! s

theorem List.head?_append {α : Type u} {s : List α} {t : List α} {x : α} (h : x ∈ List.head? s) : x ∈ List.head? (s ++ t)

theorem List.head?_append_of_ne_nil {α : Type u} (l₁ : List α) {l₂ : List α} : l₁ ≠ [] → List.head? (l₁ ++ l₂) = List.head? l₁

theorem List.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : List α} (h : l ≠ []) : List.tail (l ++ [a]) = List.tail l ++ [a]

theorem List.cons_head?_tail {α : Type u} {l : List α} {a : α} : a ∈ List.head? l → a :: List.tail l = l

theorem List.head!_mem_head? {α : Type u} [Inhabited α] {l : List α} : l ≠ [] → List.head! l ∈ List.head? l

theorem List.cons_head!_tail {α : Type u} [Inhabited α] {l : List α} (h : l ≠ []) : List.head! l :: List.tail l = l

theorem List.head!_mem_self {α : Type u} [Inhabited α] {l : List α} (h : l ≠ []) : List.head! l ∈ l

theorem List.head_mem {α : Type u} {l : List α} (h : l ≠ []) : List.head l h ∈ l

@[simp]

theorem List.head?_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.head? (List.map f l) = Option.map f (List.head? l)

theorem List.tail_append_of_ne_nil {α : Type u} (l : List α) (l' : List α) (h : l ≠ []) : List.tail (l ++ l') = List.tail l ++ l'

@[simp]

theorem List.nthLe_tail {α : Type u} (l : List α) (i : ℕ) (h : i < List.length (List.tail l)) (h' : optParam (i + 1 < List.length l) ⋯) : List.nthLe (List.tail l) i h = List.nthLe l (i + 1) h'

theorem List.nthLe_cons_aux {α : Type u} {l : List α} {a : α} {n : ℕ} (hn : n ≠ 0) (h : n < List.length (a :: l)) : n - 1 < List.length l

theorem List.nthLe_cons {α : Type u} {l : List α} {a : α} {n : ℕ} (hl : n < List.length (a :: l)) : List.nthLe (a :: l) n hl = if hn : n = 0 then a else List.nthLe l (n - 1) ⋯

@[simp]

theorem List.modifyHead_modifyHead {α : Type u} (l : List α) (f : α → α) (g : α → α) : List.modifyHead g (List.modifyHead f l) = List.modifyHead (g ∘ f) l

Induction from the right

def List.reverseRecOn {α : Type u} {motive : List α → Sort u_2} (l : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : motive l

Induction principle from the right for lists: if a property holds for the empty list, and for l ++ [a] if it holds for l, then it holds for all lists. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem List.reverseRecOn_nil {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : List.reverseRecOn [] nil append_singleton = nil

@[simp]

theorem List.reverseRecOn_concat {α : Type u} {motive : List α → Sort u_2} (x : α) (xs : List α) (nil : motive []) (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) : List.reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (List.reverseRecOn xs nil append_singleton)

def List.bidirectionalRec {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (l : List α) : motive l

Bidirectional induction principle for lists: if a property holds for the empty list, the singleton list, and a :: (l ++ [b]) from l, then it holds for all lists. This can be used to prove statements about palindromes. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

• One or more equations did not get rendered due to their size.
• List.bidirectionalRec nil singleton cons_append [] = nil
• List.bidirectionalRec nil singleton cons_append [a] = singleton a

@[simp]

theorem List.bidirectionalRec_nil {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) : List.bidirectionalRec nil singleton cons_append [] = nil

@[simp]

theorem List.bidirectionalRec_singleton {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a : α) : List.bidirectionalRec nil singleton cons_append [a] = singleton a

@[simp]

theorem List.bidirectionalRec_cons_append {α : Type u} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a]) (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (a : α) (l : List α) (b : α) : List.bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) = cons_append a l b (List.bidirectionalRec nil singleton cons_append l)

@[inline, reducible]

abbrev List.bidirectionalRecOn {α : Type u} {C : List α → Sort u_2} (l : List α) (H0 : C []) (H1 : (a : α) → C [a]) (Hn : (a : α) → (l : List α) → (b : α) → C l → C (a :: (l ++ [b]))) : C l

Like bidirectionalRec, but with the list parameter placed first.

Equations

• List.bidirectionalRecOn l H0 H1 Hn = List.bidirectionalRec H0 H1 Hn l

sublists

theorem List.Sublist.cons_cons {α : Type u} {l₁ : List α} {l₂ : List α} (a : α) (s : List.Sublist l₁ l₂) : List.Sublist (a :: l₁) (a :: l₂)

theorem List.sublist_cons_of_sublist {α : Type u} {l₁ : List α} {l₂ : List α} (a : α) (h : List.Sublist l₁ l₂) : List.Sublist l₁ (a :: l₂)

theorem List.sublist_of_cons_sublist_cons {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} : List.Sublist (a :: l₁) (a :: l₂) → List.Sublist l₁ l₂

theorem List.cons_sublist_cons_iff {α : Type u} {l₁ : List α} {l₂ : List α} {a : α} : List.Sublist (a :: l₁) (a :: l₂) ↔ List.Sublist l₁ l₂

theorem List.eq_nil_of_sublist_nil {α : Type u} {l : List α} (s : List.Sublist l []) : l = []

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

Alias of List.sublist_nil.

@[simp]

theorem List.sublist_singleton {α : Type u} {l : List α} {a : α} : List.Sublist l [a] ↔ l = [] ∨ l = [a]

theorem List.sublist_replicate_iff {α : Type u} {l : List α} {a : α} {n : ℕ} : List.Sublist l (List.replicate n a) ↔ ∃ (k : ℕ), k ≤ n ∧ l = List.replicate k a

theorem List.Sublist.antisymm {α : Type u} {l₁ : List α} {l₂ : List α} (s₁ : List.Sublist l₁ l₂) (s₂ : List.Sublist l₂ l₁) : l₁ = l₂

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

Equations

• List.decidableSublist [] x = isTrue ⋯
• List.decidableSublist (head :: tail) [] = isFalse ⋯
• List.decidableSublist (a :: l₁) (b :: l₂) = if h : a = b then decidable_of_decidable_of_iff ⋯ else decidable_of_decidable_of_iff ⋯

indexOf

@[simp]

theorem List.indexOf_cons_self {α : Type u} [DecidableEq α] (a : α) (l : List α) : List.indexOf a (a :: l) = 0

theorem List.indexOf_cons_eq {α : Type u} [DecidableEq α] {a : α} {b : α} (l : List α) : b = a → List.indexOf a (b :: l) = 0

@[simp]

theorem List.indexOf_cons_ne {α : Type u} [DecidableEq α] {a : α} {b : α} (l : List α) : b ≠ a → List.indexOf a (b :: l) = Nat.succ (List.indexOf a l)

theorem List.indexOf_eq_length {α : Type u} [DecidableEq α] {a : α} {l : List α} : List.indexOf a l = List.length l ↔ ¬a ∈ l

@[simp]

theorem List.indexOf_of_not_mem {α : Type u} [DecidableEq α] {l : List α} {a : α} : ¬a ∈ l → List.indexOf a l = List.length l

theorem List.indexOf_le_length {α : Type u} [DecidableEq α] {a : α} {l : List α} : List.indexOf a l ≤ List.length l

theorem List.indexOf_lt_length {α : Type u} [DecidableEq α] {a : α} {l : List α} : List.indexOf a l < List.length l ↔ a ∈ l

theorem List.indexOf_append_of_mem {α : Type u} {l₁ : List α} {l₂ : List α} [DecidableEq α] {a : α} (h : a ∈ l₁) : List.indexOf a (l₁ ++ l₂) = List.indexOf a l₁

theorem List.indexOf_append_of_not_mem {α : Type u} {l₁ : List α} {l₂ : List α} [DecidableEq α] {a : α} (h : ¬a ∈ l₁) : List.indexOf a (l₁ ++ l₂) = List.length l₁ + List.indexOf a l₂

nth element

@[deprecated List.get_of_mem]

theorem List.nthLe_of_mem {α : Type u} {a : α} {l : List α} (h : a ∈ l) : ∃ (n : ℕ), ∃ (h : n < List.length l), List.nthLe l n h = a

@[deprecated List.get?_eq_get]

theorem List.nthLe_get? {α : Type u} {l : List α} {n : ℕ} (h : n < List.length l) : List.get? l n = some (List.nthLe l n h)

@[simp]

theorem List.get?_length {α : Type u} (l : List α) : List.get? l (List.length l) = none

@[deprecated List.get?_eq_some]

theorem List.get?_eq_some' {α : Type u} {l : List α} {n : ℕ} {a : α} : List.get? l n = some a ↔ ∃ (h : n < List.length l), List.nthLe l n h = a

@[deprecated List.get_mem]

theorem List.nthLe_mem {α : Type u} (l : List α) (n : ℕ) (h : n < List.length l) : List.nthLe l n h ∈ l

@[deprecated List.mem_iff_get]

theorem List.mem_iff_nthLe {α : Type u} {a : α} {l : List α} : a ∈ l ↔ ∃ (n : ℕ), ∃ (h : n < List.length l), List.nthLe l n h = a

theorem List.get?_injective {α : Type u} {xs : List α} {i : ℕ} {j : ℕ} (h₀ : i < List.length xs) (h₁ : List.Nodup xs) (h₂ : List.get? xs i = List.get? xs j) : i = j

@[deprecated List.get_map]

theorem List.nthLe_map {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : ℕ} (H1 : n < List.length (List.map f l)) (H2 : n < List.length l) : List.nthLe (List.map f l) n H1 = f (List.nthLe l n H2)

theorem List.get_map_rev {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : Fin (List.length l)} : f (List.get l n) = List.get (List.map f l) { val := ↑n, isLt := ⋯ }

A version of get_map that can be used for rewriting.

@[deprecated List.get_map_rev]

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

A version of nthLe_map that can be used for rewriting.

@[simp, deprecated List.get_map]

theorem List.nthLe_map' {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : ℕ} (H : n < List.length (List.map f l)) : List.nthLe (List.map f l) n H = f (List.nthLe l n ⋯)

@[deprecated List.get_of_eq]

theorem List.nthLe_of_eq {α : Type u} {L : List α} {L' : List α} (h : L = L') {i : ℕ} (hi : i < List.length L) : List.nthLe L i hi = List.nthLe L' i ⋯

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

@[simp, deprecated List.get_singleton]

theorem List.nthLe_singleton {α : Type u} (a : α) {n : ℕ} (hn : n < 1) : List.nthLe [a] n hn = a

@[deprecated]

theorem List.nthLe_zero {α : Type u} [Inhabited α] {L : List α} (h : 0 < List.length L) : List.nthLe L 0 h = List.head! L

@[deprecated List.get_append]

theorem List.nthLe_append {α : Type u} {l₁ : List α} {l₂ : List α} {n : ℕ} (hn₁ : n < List.length (l₁ ++ l₂)) (hn₂ : n < List.length l₁) : List.nthLe (l₁ ++ l₂) n hn₁ = List.nthLe l₁ n hn₂

@[deprecated List.get_append_right']

theorem List.nthLe_append_right {α : Type u} {l₁ : List α} {l₂ : List α} {n : ℕ} (h₁ : List.length l₁ ≤ n) (h₂ : n < List.length (l₁ ++ l₂)) : List.nthLe (l₁ ++ l₂) n h₂ = List.nthLe l₂ (n - List.length l₁) ⋯

@[deprecated List.get_replicate]

theorem List.nthLe_replicate {α : Type u} (a : α) {n : ℕ} {m : ℕ} (h : m < List.length (List.replicate n a)) : List.nthLe (List.replicate n a) m h = a

@[deprecated List.getLast_eq_get]

theorem List.getLast_eq_nthLe {α : Type u} (l : List α) (h : l ≠ []) : List.getLast l h = List.nthLe l (List.length l - 1) ⋯

theorem List.get_length_sub_one {α : Type u} {l : List α} (h : List.length l - 1 < List.length l) : List.get l { val := List.length l - 1, isLt := h } = List.getLast l ⋯

@[deprecated List.get_length_sub_one]

theorem List.nthLe_length_sub_one {α : Type u} {l : List α} (h : List.length l - 1 < List.length l) : List.nthLe l (List.length l - 1) h = List.getLast l ⋯

@[deprecated List.get_cons_length]

theorem List.nthLe_cons_length {α : Type u} (x : α) (xs : List α) (n : ℕ) (h : n = List.length xs) : List.nthLe (x :: xs) n ⋯ = List.getLast (x :: xs) ⋯

theorem List.take_one_drop_eq_of_lt_length {α : Type u} {l : List α} {n : ℕ} (h : n < List.length l) : List.take 1 (List.drop n l) = [List.get l { val := n, isLt := h }]

@[deprecated List.take_one_drop_eq_of_lt_length]

theorem List.take_one_drop_eq_of_lt_length' {α : Type u} {l : List α} {n : ℕ} (h : n < List.length l) : List.take 1 (List.drop n l) = [List.nthLe l n h]

theorem List.ext_get? {α : Type u_1} {l₁ : List α} {l₂ : List α} : (∀ (n : ℕ), List.get? l₁ n = List.get? l₂ n) → l₁ = l₂

Alias of List.ext.

theorem List.ext_get?' {α : Type u} {l₁ : List α} {l₂ : List α} (h' : ∀ (n : ℕ), n < max (List.length l₁) (List.length l₂) → List.get? l₁ n = List.get? l₂ n) : l₁ = l₂

theorem List.ext_get?_iff {α : Type u} {l₁ : List α} {l₂ : List α} : l₁ = l₂ ↔ ∀ (n : ℕ), List.get? l₁ n = List.get? l₂ n

theorem List.ext_get_iff {α : Type u} {l₁ : List α} {l₂ : List α} : l₁ = l₂ ↔ List.length l₁ = List.length l₂ ∧ ∀ (n : ℕ) (h₁ : n < List.length l₁) (h₂ : n < List.length l₂), List.get l₁ { val := n, isLt := h₁ } = List.get l₂ { val := n, isLt := h₂ }

theorem List.ext_get?_iff' {α : Type u} {l₁ : List α} {l₂ : List α} : l₁ = l₂ ↔ ∀ (n : ℕ), n < max (List.length l₁) (List.length l₂) → List.get? l₁ n = List.get? l₂ n

@[deprecated List.ext_get]

theorem List.ext_nthLe {α : Type u} {l₁ : List α} {l₂ : List α} (hl : List.length l₁ = List.length l₂) (h : ∀ (n : ℕ) (h₁ : n < List.length l₁) (h₂ : n < List.length l₂), List.nthLe l₁ n h₁ = List.nthLe l₂ n h₂) : l₁ = l₂

@[simp]

theorem List.indexOf_get {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : List.indexOf a l < List.length l) : List.get l { val := List.indexOf a l, isLt := h } = a

@[simp, deprecated List.indexOf_get]

theorem List.indexOf_nthLe {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : List.indexOf a l < List.length l) : List.nthLe l (List.indexOf a l) h = a

@[simp]

theorem List.indexOf_get? {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : List.get? l (List.indexOf a l) = some a

@[deprecated]

theorem List.get_reverse_aux₁ {α : Type u} (l : List α) (r : List α) (i : ℕ) (h1 : i + List.length l < List.length (List.reverseAux l r)) (h2 : i < List.length r) : List.get (List.reverseAux l r) { val := i + List.length l, isLt := h1 } = List.get r { val := i, isLt := h2 }

theorem List.indexOf_inj {α : Type u} [DecidableEq α] {l : List α} {x : α} {y : α} (hx : x ∈ l) (hy : y ∈ l) : List.indexOf x l = List.indexOf y l ↔ x = y

theorem List.get_reverse_aux₂ {α : Type u} (l : List α) (r : List α) (i : ℕ) (h1 : List.length l - 1 - i < List.length (List.reverseAux l r)) (h2 : i < List.length l) : List.get (List.reverseAux l r) { val := List.length l - 1 - i, isLt := h1 } = List.get l { val := i, isLt := h2 }

@[simp]

theorem List.get_reverse {α : Type u} (l : List α) (i : ℕ) (h1 : List.length l - 1 - i < List.length (List.reverse l)) (h2 : i < List.length l) : List.get (List.reverse l) { val := List.length l - 1 - i, isLt := h1 } = List.get l { val := i, isLt := h2 }

@[simp, deprecated List.get_reverse]

theorem List.nthLe_reverse {α : Type u} (l : List α) (i : ℕ) (h1 : List.length l - 1 - i < List.length (List.reverse l)) (h2 : i < List.length l) : List.nthLe (List.reverse l) (List.length l - 1 - i) h1 = List.nthLe l i h2

@[deprecated List.get_reverse']

theorem List.nthLe_reverse' {α : Type u} (l : List α) (n : ℕ) (hn : n < List.length (List.reverse l)) (hn' : List.length l - 1 - n < List.length l) : List.nthLe (List.reverse l) n hn = List.nthLe l (List.length l - 1 - n) hn'

theorem List.get_reverse' {α : Type u} (l : List α) (n : Fin (List.length (List.reverse l))) (hn' : List.length l - 1 - ↑n < List.length l) : List.get (List.reverse l) n = List.get l { val := List.length l - 1 - ↑n, isLt := hn' }

theorem List.eq_cons_of_length_one {α : Type u} {l : List α} (h : List.length l = 1) : l = [List.nthLe l 0 ⋯]

theorem List.get_eq_iff {α : Type u} {l : List α} {n : Fin (List.length l)} {x : α} : List.get l n = x ↔ List.get? l ↑n = some x

@[deprecated List.get_eq_iff]

theorem List.nthLe_eq_iff {α : Type u} {l : List α} {n : ℕ} {x : α} {h : n < List.length l} : List.nthLe l n h = x ↔ List.get? l n = some x

@[deprecated List.get?_eq_get]

theorem List.some_nthLe_eq {α : Type u} {l : List α} {n : ℕ} {h : n < List.length l} : some (List.nthLe l n h) = List.get? l n

theorem List.modifyNthTail_modifyNthTail {α : Type u} {f : List α → List α} {g : List α → List α} (m : ℕ) (n : ℕ) (l : List α) : List.modifyNthTail g (m + n) (List.modifyNthTail f n l) = List.modifyNthTail (fun (l : List α) => List.modifyNthTail g m (f l)) n l

theorem List.modifyNthTail_modifyNthTail_le {α : Type u} {f : List α → List α} {g : List α → List α} (m : ℕ) (n : ℕ) (l : List α) (h : n ≤ m) : List.modifyNthTail g m (List.modifyNthTail f n l) = List.modifyNthTail (fun (l : List α) => List.modifyNthTail g (m - n) (f l)) n l

theorem List.modifyNthTail_modifyNthTail_same {α : Type u} {f : List α → List α} {g : List α → List α} (n : ℕ) (l : List α) : List.modifyNthTail g n (List.modifyNthTail f n l) = List.modifyNthTail (g ∘ f) n l

theorem List.removeNth_eq_nthTail {α : Type u} (n : ℕ) (l : List α) : List.removeNth l n = List.modifyNthTail List.tail n l

theorem List.modifyNth_eq_set {α : Type u} (f : α → α) (n : ℕ) (l : List α) : List.modifyNth f n l = Option.getD ((fun (a : α) => List.set l n (f a)) <$> List.get? l n) l

theorem List.length_modifyNthTail {α : Type u} (f : List α → List α) (H : ∀ (l : List α), List.length (f l) = List.length l) (n : ℕ) (l : List α) : List.length (List.modifyNthTail f n l) = List.length l

theorem List.length_modifyNth {α : Type u} (f : α → α) (n : ℕ) (l : List α) : List.length (List.modifyNth f n l) = List.length l

@[simp, deprecated List.get_set_eq]

theorem List.nthLe_set_eq {α : Type u} (l : List α) (i : ℕ) (a : α) (h : i < List.length (List.set l i a)) : List.nthLe (List.set l i a) i h = a

@[simp]

theorem List.get_set_of_ne {α : Type u} {l : List α} {i : ℕ} {j : ℕ} (h : i ≠ j) (a : α) (hj : j < List.length (List.set l i a)) : List.get (List.set l i a) { val := j, isLt := hj } = List.get l { val := j, isLt := ⋯ }

@[simp, deprecated List.get_set_of_ne]

theorem List.nthLe_set_of_ne {α : Type u} {l : List α} {i : ℕ} {j : ℕ} (h : i ≠ j) (a : α) (hj : j < List.length (List.set l i a)) : List.nthLe (List.set l i a) j hj = List.nthLe l j ⋯

map

theorem List.map_eq_foldr {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.map f l = List.foldr (fun (a : α) (bs : List β) => f a :: bs) [] l

theorem List.map_congr {α : Type u} {β : Type v} {f : α → β} {g : α → β} {l : List α} : (∀ (x : α), x ∈ l → f x = g x) → List.map f l = List.map g l

theorem List.map_eq_map_iff {α : Type u} {β : Type v} {f : α → β} {g : α → β} {l : List α} : List.map f l = List.map g l ↔ ∀ (x : α), x ∈ l → f x = g x

theorem List.map_concat {α : Type u} {β : Type v} (f : α → β) (a : α) (l : List α) : List.map f (List.concat l a) = List.concat (List.map f l) (f a)

theorem List.map_id'' {α : Type u} {f : α → α} (h : ∀ (x : α), f x = x) (l : List α) : List.map f l = l

theorem List.eq_nil_of_map_eq_nil {α : Type u} {β : Type v} {f : α → β} {l : List α} (h : List.map f l = []) : l = []

@[simp]

theorem List.map_join {α : Type u} {β : Type v} (f : α → β) (L : List (List α)) : List.map f (List.join L) = List.join (List.map (List.map f) L)

theorem List.bind_pure_eq_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.bind l (pure ∘ f) = List.map f l

@[deprecated List.bind_pure_eq_map]

theorem List.bind_ret_eq_map {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.bind l (List.ret ∘ f) = List.map f l

theorem List.bind_congr {α : Type u} {β : Type v} {l : List α} {f : α → List β} {g : α → List β} (h : ∀ (x : α), x ∈ l → f x = g x) : List.bind l f = List.bind l g

@[simp]

theorem List.map_eq_map {α : Type u_2} {β : Type u_2} (f : α → β) (l : List α) : f <$> l = List.map f l

@[simp]

theorem List.map_tail {α : Type u} {β : Type v} (f : α → β) (l : List α) : List.map f (List.tail l) = List.tail (List.map f l)

theorem List.comp_map {α : Type u} {β : Type v} {γ : Type w} (h : β → γ) (g : α → β) (l : List α) : List.map (h ∘ g) l = List.map h (List.map g l)

A single List.map of a composition of functions is equal to composing a List.map with another List.map, fully applied. This is the reverse direction of List.map_map.

@[simp]

theorem List.map_comp_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) : List.map g ∘ List.map f = List.map (g ∘ f)

Composing a List.map with another List.map is equal to a single List.map of composed functions.

theorem Function.LeftInverse.list_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) : Function.LeftInverse (List.map f) (List.map g)

theorem Function.RightInverse.list_map {α : Type u} {β : Type v} {f : α → β} {g : β → α} (h : Function.RightInverse f g) : Function.RightInverse (List.map f) (List.map g)

theorem Function.Involutive.list_map {α : Type u} {f : α → α} (h : Function.Involutive f) : Function.Involutive (List.map f)

@[simp]

theorem List.map_leftInverse_iff {α : Type u} {β : Type v} {f : α → β} {g : β → α} : Function.LeftInverse (List.map f) (List.map g) ↔ Function.LeftInverse f g

@[simp]

theorem List.map_rightInverse_iff {α : Type u} {β : Type v} {f : α → β} {g : β → α} : Function.RightInverse (List.map f) (List.map g) ↔ Function.RightInverse f g

@[simp]

theorem List.map_involutive_iff {α : Type u} {f : α → α} : Function.Involutive (List.map f) ↔ Function.Involutive f

theorem Function.Injective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Function.Injective f) : Function.Injective (List.map f)

@[simp]

theorem List.map_injective_iff {α : Type u} {β : Type v} {f : α → β} : Function.Injective (List.map f) ↔ Function.Injective f

theorem Function.Surjective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Function.Surjective f) : Function.Surjective (List.map f)

@[simp]

theorem List.map_surjective_iff {α : Type u} {β : Type v} {f : α → β} : Function.Surjective (List.map f) ↔ Function.Surjective f

theorem Function.Bijective.list_map {α : Type u} {β : Type v} {f : α → β} (h : Function.Bijective f) : Function.Bijective (List.map f)

@[simp]

theorem List.map_bijective_iff {α : Type u} {β : Type v} {f : α → β} : Function.Bijective (List.map f) ↔ Function.Bijective f

theorem List.map_filter_eq_foldr {α : Type u} {β : Type v} (f : α → β) (p : α → Bool) (as : List α) : List.map f (List.filter p as) = List.foldr (fun (a : α) (bs : List β) => bif p a then f a :: bs else bs) [] as

theorem List.getLast_map {α : Type u} {β : Type v} (f : α → β) {l : List α} (hl : l ≠ []) : List.getLast (List.map f l) ⋯ = f (List.getLast l hl)

theorem List.map_eq_replicate_iff {α : Type u} {β : Type v} {l : List α} {f : α → β} {b : β} : List.map f l = List.replicate (List.length l) b ↔ ∀ (x : α), x ∈ l → f x = b

@[simp]

theorem List.map_const {α : Type u} {β : Type v} (l : List α) (b : β) : List.map (Function.const α b) l = List.replicate (List.length l) b

@[simp]

theorem List.map_const' {α : Type u} {β : Type v} (l : List α) (b : β) : List.map (fun (x : α) => b) l = List.replicate (List.length l) b

theorem List.eq_of_mem_map_const {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {l : List α} (h : b₁ ∈ List.map (Function.const α b₂) l) : b₁ = b₂

zipWith

theorem List.nil_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : List β) : List.zipWith f [] l = []

theorem List.zipWith_nil {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : List α) : List.zipWith f l [] = []

@[simp]

theorem List.zipWith_flip {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (as : List α) (bs : List β) : List.zipWith (flip f) bs as = List.zipWith f as bs

take, drop

theorem List.take_cons {α : Type u} (n : ℕ) (a : α) (l : List α) : List.take (Nat.succ n) (a :: l) = a :: List.take n l

@[deprecated List.get_take]

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

@[deprecated List.get_take']

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

@[simp]

theorem List.drop_tail {α : Type u} (l : List α) (n : ℕ) : List.drop n (List.tail l) = List.drop (n + 1) l

theorem List.cons_get_drop_succ {α : Type u} {l : List α} {n : Fin (List.length l)} : List.get l n :: List.drop (↑n + 1) l = List.drop (↑n) l

@[deprecated List.cons_get_drop_succ]

theorem List.cons_nthLe_drop_succ {α : Type u} {l : List α} {n : ℕ} (hn : n < List.length l) : List.nthLe l n hn :: List.drop (n + 1) l = List.drop n l

@[deprecated List.get_drop]

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

@[deprecated List.get_drop']

theorem List.nthLe_drop' {α : Type u} (L : List α) {i : ℕ} {j : ℕ} (h : j < List.length (List.drop i L)) : List.nthLe (List.drop i L) j h = List.nthLe L (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.modifyNth_nil {α : Type u} (f : α → α) (n : ℕ) : List.modifyNth f n [] = []

@[simp]

theorem List.modifyNth_zero_cons {α : Type u} (f : α → α) (a : α) (l : List α) : List.modifyNth f 0 (a :: l) = f a :: l

@[simp]

theorem List.modifyNth_succ_cons {α : Type u} (f : α → α) (n : ℕ) (a : α) (l : List α) : List.modifyNth f (n + 1) (a :: l) = a :: List.modifyNth f n l

@[simp]

theorem List.takeI_length {α : Type u} [Inhabited α] (n : ℕ) (l : List α) : List.length (List.takeI n l) = n

@[simp]

theorem List.takeI_nil {α : Type u} [Inhabited α] (n : ℕ) : List.takeI n [] = List.replicate n default

theorem List.takeI_eq_take {α : Type u} [Inhabited α] {n : ℕ} {l : List α} : n ≤ List.length l → List.takeI n l = List.take n l

@[simp]

theorem List.takeI_left {α : Type u} [Inhabited α] (l₁ : List α) (l₂ : List α) : List.takeI (List.length l₁) (l₁ ++ l₂) = l₁

theorem List.takeI_left' {α : Type u} [Inhabited α] {l₁ : List α} {l₂ : List α} {n : ℕ} (h : List.length l₁ = n) : List.takeI n (l₁ ++ l₂) = l₁

@[simp]

theorem List.takeD_length {α : Type u} (n : ℕ) (l : List α) (a : α) : List.length (List.takeD n l a) = n

theorem List.takeD_eq_take {α : Type u} {n : ℕ} {l : List α} (a : α) : n ≤ List.length l → List.takeD n l a = List.take n l

@[simp]

theorem List.takeD_left {α : Type u} (l₁ : List α) (l₂ : List α) (a : α) : List.takeD (List.length l₁) (l₁ ++ l₂) a = l₁

theorem List.takeD_left' {α : Type u} {l₁ : List α} {l₂ : List α} {n : ℕ} {a : α} (h : List.length l₁ = n) : List.takeD n (l₁ ++ l₂) a = l₁

foldl, foldr

theorem List.foldl_ext {α : Type u} {β : Type v} (f : α → β → α) (g : α → β → α) (a : α) {l : List β} (H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b) : List.foldl f a l = List.foldl g a l

theorem List.foldr_ext {α : Type u} {β : Type v} (f : α → β → β) (g : α → β → β) (b : β) {l : List α} (H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b) : List.foldr f b l = List.foldr g b l

theorem List.foldl_concat {α : Type u} {β : Type v} (f : β → α → β) (b : β) (x : α) (xs : List α) : List.foldl f b (xs ++ [x]) = f (List.foldl f b xs) x

theorem List.foldr_concat {α : Type u} {β : Type v} (f : α → β → β) (b : β) (x : α) (xs : List α) : List.foldr f b (xs ++ [x]) = List.foldr f (f x b) xs

theorem List.foldl_fixed' {α : Type u} {β : Type v} {f : α → β → α} {a : α} (hf : ∀ (b : β), f a b = a) (l : List β) : List.foldl f a l = a

theorem List.foldr_fixed' {α : Type u} {β : Type v} {f : α → β → β} {b : β} (hf : ∀ (a : α), f a b = b) (l : List α) : List.foldr f b l = b

@[simp]

theorem List.foldl_fixed {α : Type u} {β : Type v} {a : α} (l : List β) : List.foldl (fun (a : α) (x : β) => a) a l = a

@[simp]

theorem List.foldr_fixed {α : Type u} {β : Type v} {b : β} (l : List α) : List.foldr (fun (x : α) (b : β) => b) b l = b

@[simp]

theorem List.foldl_join {α : Type u} {β : Type v} (f : α → β → α) (a : α) (L : List (List β)) : List.foldl f a (List.join L) = List.foldl (List.foldl f) a L

@[simp]

theorem List.foldr_join {α : Type u} {β : Type v} (f : α → β → β) (b : β) (L : List (List α)) : List.foldr f b (List.join L) = List.foldr (fun (l : List α) (b : β) => List.foldr f b l) b L

theorem List.foldr_eta {α : Type u} (l : List α) : List.foldr List.cons [] l = l

@[simp]

theorem List.reverse_foldl {α : Type u} {l : List α} : List.reverse (List.foldl (fun (t : List α) (h : α) => h :: t) [] l) = l

theorem List.foldl_map' {α : Type u} {β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldl f' (g a) (List.map g l) = g (List.foldl f a l)

theorem List.foldr_map' {α : Type u} {β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : List.foldr f' (g a) (List.map g l) = g (List.foldr f a l)

theorem List.foldl_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β) (op₃ : γ → ι → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i) : List.foldl op₃ (f a b) l = f (List.foldl op₁ a l) (List.foldl op₂ b l)

theorem List.foldr_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : ι → α → α) (op₂ : ι → β → β) (op₃ : ι → γ → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)) : List.foldr op₃ (f a b) l = f (List.foldr op₁ a l) (List.foldr op₂ b l)

theorem List.injective_foldl_comp {α : Type u_2} {l : List (α → α)} {f : α → α} (hl : ∀ (f : α → α), f ∈ l → Function.Injective f) (hf : Function.Injective f) : Function.Injective (List.foldl Function.comp f l)

def List.foldrRecOn {α : Type u} {β : Type v} {C : β → Sort u_2} (l : List α) (op : α → β → β) (b : β) (hb : C b) (hl : (b : β) → C b → (a : α) → a ∈ l → C (op a b)) : C (List.foldr op b l)

Induction principle for values produced by a foldr: if a property holds for the seed element b : β and for all incremental op : α → β → β performed on the elements (a : α) ∈ l. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

• One or more equations did not get rendered due to their size.

def List.foldlRecOn {α : Type u} {β : Type v} {C : β → Sort u_2} (l : List α) (op : β → α → β) (b : β) (hb : C b) (hl : (b : β) → C b → (a : α) → a ∈ l → C (op b a)) : C (List.foldl op b l)

Induction principle for values produced by a foldl: if a property holds for the seed element b : β and for all incremental op : β → α → β performed on the elements (a : α) ∈ l. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem List.foldrRecOn_nil {α : Type u} {β : Type v} {C : β → Sort u_2} (op : α → β → β) (b : β) (hb : C b) (hl : (b : β) → C b → (a : α) → a ∈ [] → C (op a b)) : List.foldrRecOn [] op b hb hl = hb

@[simp]

theorem List.foldrRecOn_cons {α : Type u} {β : Type v} {C : β → Sort u_2} (x : α) (l : List α) (op : α → β → β) (b : β) (hb : C b) (hl : (b : β) → C b → (a : α) → a ∈ x :: l → C (op a b)) : List.foldrRecOn (x :: l) op b hb hl = hl (List.foldr op b l) (List.foldrRecOn l op b hb fun (b : β) (hb : C b) (a : α) (ha : a ∈ l) => hl b hb a ⋯) x ⋯

@[simp]

theorem List.foldlRecOn_nil {α : Type u} {β : Type v} {C : β → Sort u_2} (op : β → α → β) (b : β) (hb : C b) (hl : (b : β) → C b → (a : α) → a ∈ [] → C (op b a)) : List.foldlRecOn [] op b hb hl = hb

theorem List.append_cons_inj_of_not_mem {α : Type u} {x₁ : List α} {x₂ : List α} {z₁ : List α} {z₂ : List α} {a₁ : α} {a₂ : α} (notin_x : ¬a₂ ∈ x₁) (notin_z : ¬a₂ ∈ z₁) : x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Consider two lists l₁ and l₂ with designated elements a₁ and a₂ somewhere in them: l₁ = x₁ ++ [a₁] ++ z₁ and l₂ = x₂ ++ [a₂] ++ z₂. Assume the designated element a₂ is present in neither x₁ nor z₁. We conclude that the lists are equal (l₁ = l₂) if and only if their respective parts are equal (x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂).

theorem List.length_scanl {α : Type u} {β : Type v} {f : β → α → β} (a : β) (l : List α) : List.length (List.scanl f a l) = List.length l + 1

@[simp]

theorem List.scanl_nil {α : Type u} {β : Type v} {f : β → α → β} (b : β) : List.scanl f b [] = [b]

@[simp]

theorem List.scanl_cons {α : Type u} {β : Type v} {f : β → α → β} {b : β} {a : α} {l : List α} : List.scanl f b (a :: l) = [b] ++ List.scanl f (f b a) l

@[simp]

theorem List.get?_zero_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} : List.get? (List.scanl f b l) 0 = some b

@[simp]

theorem List.get_zero_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {h : 0 < List.length (List.scanl f b l)} : List.get (List.scanl f b l) { val := 0, isLt := h } = b

@[simp, deprecated List.get_zero_scanl]

theorem List.nthLe_zero_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {h : 0 < List.length (List.scanl f b l)} : List.nthLe (List.scanl f b l) 0 h = b

theorem List.get?_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {i : ℕ} : List.get? (List.scanl f b l) (i + 1) = Option.bind (List.get? (List.scanl f b l) i) fun (x : β) => Option.map (fun (y : α) => f x y) (List.get? l i)

@[deprecated List.get_succ_scanl]

theorem List.nthLe_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {i : ℕ} {h : i + 1 < List.length (List.scanl f b l)} : List.nthLe (List.scanl f b l) (i + 1) h = f (List.nthLe (List.scanl f b l) i ⋯) (List.nthLe l i ⋯)

theorem List.get_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : List α} {i : ℕ} {h : i + 1 < List.length (List.scanl f b l)} : List.get (List.scanl f b l) { val := i + 1, isLt := h } = f (List.get (List.scanl f b l) { val := i, isLt := ⋯ }) (List.get l { val := i, isLt := ⋯ })

@[simp]

theorem List.scanr_nil {α : Type u} {β : Type v} (f : α → β → β) (b : β) : List.scanr f b [] = [b]

@[simp]

theorem List.scanr_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : List α) : List.scanr f b (a :: l) = List.foldr f b (a :: l) :: List.scanr f b l

theorem List.foldl1_eq_foldr1 {α : Type u} {f : α → α → α} (hassoc : Associative f) (a : α) (b : α) (l : List α) : List.foldl f a (l ++ [b]) = List.foldr f b (a :: l)

theorem List.foldl_eq_of_comm_of_assoc {α : Type u} {f : α → α → α} (hcomm : Commutative f) (hassoc : Associative f) (a : α) (b : α) (l : List α) : List.foldl f a (b :: l) = f b (List.foldl f a l)

theorem List.foldl_eq_foldr {α : Type u} {f : α → α → α} (hcomm : Commutative f) (hassoc : Associative f) (a : α) (l : List α) : List.foldl f a l = List.foldr f a l

theorem List.foldl_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (b : β) (l : List β) : List.foldl f a (b :: l) = f (List.foldl f a l) b

theorem List.foldl_eq_foldr' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (l : List β) : List.foldl f a l = List.foldr (flip f) a l

theorem List.foldr_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → β} (hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)) (a : β) (b : α) (l : List α) : List.foldr f a (b :: l) = List.foldr f (f b a) l

theorem List.foldl_assoc {α : Type u} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ : α} {a₂ : α} : List.foldl op (op a₁ a₂) l = op a₁ (List.foldl op a₂ l)

theorem List.foldl_op_eq_op_foldr_assoc {α : Type u} {op : α → α → α} [ha : Std.Associative op] {l : List α} {a₁ : α} {a₂ : α} : op (List.foldl op a₁ l) a₂ = op a₁ (List.foldr (fun (x x_1 : α) => op x x_1) a₂ l)

theorem List.foldl_assoc_comm_cons {α : Type u} {op : α → α → α} [ha : Std.Associative op] [hc : Std.Commutative op] {l : List α} {a₁ : α} {a₂ : α} : List.foldl op a₂ (a₁ :: l) = op a₁ (List.foldl op a₂ l)

foldlM, foldrM, mapM

theorem List.foldrM_eq_foldr {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : α → β → m β) (b : β) (l : List α) : List.foldrM f b l = List.foldr (fun (a : α) (mb : m β) => mb >>= f a) (pure b) l

theorem List.foldlM_eq_foldl {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (f : β → α → m β) (b : β) (l : List α) : List.foldlM f b l = List.foldl (fun (mb : m β) (a : α) => do let b ← mb f b a) (pure b) l

intersperse

@[simp]

theorem List.intersperse_singleton {α : Type u} (a : α) (b : α) : List.intersperse a [b] = [b]

@[simp]

theorem List.intersperse_cons_cons {α : Type u} (a : α) (b : α) (c : α) (tl : List α) : List.intersperse a (b :: c :: tl) = b :: a :: List.intersperse a (c :: tl)

splitAt and splitOn

@[simp]

theorem List.splitAt_eq_take_drop {α : Type u} (n : ℕ) (l : List α) : List.splitAt n l = (List.take n l, List.drop n l)

theorem List.splitAt_eq_take_drop.go_eq_take_drop {α : Type u} (n : ℕ) (l : List α) (xs : List α) (acc : Array α) : List.splitAt.go l xs n acc = if n < List.length xs then (Array.toList acc ++ List.take n xs, List.drop n xs) else (l, [])

@[simp]

theorem List.splitOn_nil {α : Type u} [DecidableEq α] (a : α) : List.splitOn a [] = [[]]

@[simp]

theorem List.splitOnP_nil {α : Type u} (p : α → Bool) : List.splitOnP p [] = [[]]

theorem List.splitOnP.go_ne_nil {α : Type u} (p : α → Bool) (xs : List α) (acc : List α) : List.splitOnP.go p xs acc ≠ []

theorem List.splitOnP.go_acc {α : Type u} (p : α → Bool) (xs : List α) (acc : List α) : List.splitOnP.go p xs acc = List.modifyHead (fun (x : List α) => List.reverse acc ++ x) (List.splitOnP p xs)

theorem List.splitOnP_ne_nil {α : Type u} (p : α → Bool) (xs : List α) : List.splitOnP p xs ≠ []

@[simp]

theorem List.splitOnP_cons {α : Type u} (p : α → Bool) (x : α) (xs : List α) : List.splitOnP p (x :: xs) = if p x = true then [] :: List.splitOnP p xs else List.modifyHead (List.cons x) (List.splitOnP p xs)

theorem List.splitOnP_spec {α : Type u} (p : α → Bool) (as : List α) : List.join (List.zipWith (fun (x x_1 : List α) => x ++ x_1) (List.splitOnP p as) (List.map (fun (x : α) => [x]) (List.filter p as) ++ [[]])) = as

The original list L can be recovered by joining the lists produced by splitOnP p L, interspersed with the elements L.filter p.

theorem List.splitOnP_spec.join_zipWith {α : Type u} {xs : List (List α)} {ys : List (List α)} {a : α} (hxs : xs ≠ []) (hys : ys ≠ []) : List.join (List.zipWith (fun (x x_1 : List α) => x ++ x_1) (List.modifyHead (List.cons a) xs) ys) = a :: List.join (List.zipWith (fun (x x_1 : List α) => x ++ x_1) xs ys)

theorem List.splitOnP_eq_single {α : Type u} (p : α → Bool) (xs : List α) (h : ∀ (x : α), x ∈ xs → ¬p x = true) : List.splitOnP p xs = [xs]

If no element satisfies p in the list xs, then xs.splitOnP p = [xs]

theorem List.splitOnP_first {α : Type u} (p : α → Bool) (xs : List α) (h : ∀ (x : α), x ∈ xs → ¬p x = true) (sep : α) (hsep : p sep = true) (as : List α) : List.splitOnP p (xs ++ sep :: as) = xs :: List.splitOnP p as

When a list of the form [...xs, sep, ...as] is split on p, the first element is xs, assuming no element in xs satisfies p but sep does satisfy p

theorem List.intercalate_splitOn {α : Type u} (xs : List α) (x : α) [DecidableEq α] : List.intercalate [x] (List.splitOn x xs) = xs

intercalate [x] is the left inverse of splitOn x

theorem List.splitOn_intercalate {α : Type u} (ls : List (List α)) [DecidableEq α] (x : α) (hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l) (hls : ls ≠ []) : List.splitOn x (List.intercalate [x] ls) = ls

splitOn x is the left inverse of intercalate [x], on the domain consisting of each nonempty list of lists ls whose elements do not contain x

modifyLast

theorem List.modifyLast.go_append_one {α : Type u} (f : α → α) (a : α) (tl : List α) (r : Array α) : List.modifyLast.go f (tl ++ [a]) r = Array.toListAppend r (List.modifyLast.go f (tl ++ [a]) #[])

theorem List.modifyLast_append_one {α : Type u} (f : α → α) (a : α) (l : List α) : List.modifyLast f (l ++ [a]) = l ++ [f a]

theorem List.modifyLast_append {α : Type u} (f : α → α) (l₁ : List α) (l₂ : List α) : l₂ ≠ [] → List.modifyLast f (l₁ ++ l₂) = l₁ ++ List.modifyLast f l₂

map for partial functions

@[simp]

theorem List.attach_nil {α : Type u} : List.attach [] = []

theorem List.sizeOf_lt_sizeOf_of_mem {α : Type u} [SizeOf α] {x : α} {l : List α} (hx : x ∈ l) : sizeOf x < sizeOf l

@[simp]

theorem List.pmap_eq_map {α : Type u} {β : Type v} (p : α → Prop) (f : α → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) : List.pmap (fun (a : α) (x : p a) => f a) l H = List.map f l

theorem List.pmap_congr {α : Type u} {β : Type v} {p : α → Prop} {q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (l : List α) {H₁ : ∀ (a : α), a ∈ l → p a} {H₂ : ∀ (a : α), a ∈ l → q a} (h : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) : List.pmap f l H₁ = List.pmap g l H₂

theorem List.map_pmap {α : Type u} {β : Type v} {γ : Type w} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) : List.map g (List.pmap f l H) = List.pmap (fun (a : α) (h : p a) => g (f a h)) l H

theorem List.pmap_map {α : Type u} {β : Type v} {γ : Type w} {p : β → Prop} (g : (b : β) → p b → γ) (f : α → β) (l : List α) (H : ∀ (a : β), a ∈ List.map f l → p a) : List.pmap g (List.map f l) H = List.pmap (fun (a : α) (h : p (f a)) => g (f a) h) l ⋯

theorem List.pmap_eq_map_attach {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) : List.pmap f l H = List.map (fun (x : { x : α // x ∈ l }) => f ↑x ⋯) (List.attach l)

theorem List.attach_map_coe' {α : Type u} {β : Type v} (l : List α) (f : α → β) : List.map (fun (i : { i : α // i ∈ l }) => f ↑i) (List.attach l) = List.map f l

theorem List.attach_map_val' {α : Type u} {β : Type v} (l : List α) (f : α → β) : List.map (fun (i : { x : α // x ∈ l }) => f ↑i) (List.attach l) = List.map f l

@[simp]

theorem List.attach_map_val {α : Type u} (l : List α) : List.map Subtype.val (List.attach l) = l

@[simp]

theorem List.mem_attach {α : Type u} (l : List α) (x : { x : α // x ∈ l }) : x ∈ List.attach l

@[simp]

theorem List.mem_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ (a : α), a ∈ l → p a} {b : β} : b ∈ List.pmap f l H ↔ ∃ (a : α), ∃ (h : a ∈ l), f a ⋯ = b

@[simp]

theorem List.length_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ (a : α), a ∈ l → p a} : List.length (List.pmap f l H) = List.length l

@[simp]

theorem List.length_attach {α : Type u} (L : List α) : List.length (List.attach L) = List.length L

@[simp]

theorem List.pmap_eq_nil {α : Type u} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {l : List α} {H : ∀ (a : α), a ∈ l → p a} : List.pmap f l H = [] ↔ l = []

@[simp]

theorem List.attach_eq_nil {α : Type u} (l : List α) : List.attach l = [] ↔ l = []

theorem List.getLast_pmap {α : Type u_2} {β : Type u_3} (p : α → Prop) (f : (a : α) → p a → β) (l : List α) (hl₁ : ∀ (a : α), a ∈ l → p a) (hl₂ : l ≠ []) : List.getLast (List.pmap f l hl₁) ⋯ = f (List.getLast l hl₂) ⋯

theorem List.get?_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ (a : α), a ∈ l → p a) (n : ℕ) : List.get? (List.pmap f l h) n = Option.pmap f (List.get? l n) ⋯

theorem List.get_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ (a : α), a ∈ l → p a) {n : ℕ} (hn : n < List.length (List.pmap f l h)) : List.get (List.pmap f l h) { val := n, isLt := hn } = f (List.get l { val := n, isLt := ⋯ }) ⋯

@[deprecated List.get_pmap]

theorem List.nthLe_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (h : ∀ (a : α), a ∈ l → p a) {n : ℕ} (hn : n < List.length (List.pmap f l h)) : List.nthLe (List.pmap f l h) n hn = f (List.nthLe l n ⋯) ⋯

theorem List.pmap_append {ι : Type u_1} {α : Type u} {p : ι → Prop} (f : (a : ι) → p a → α) (l₁ : List ι) (l₂ : List ι) (h : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a) : List.pmap f (l₁ ++ l₂) h = List.pmap f l₁ ⋯ ++ List.pmap f l₂ ⋯

theorem List.pmap_append' {α : Type u_2} {β : Type u_3} {p : α → Prop} (f : (a : α) → p a → β) (l₁ : List α) (l₂ : List α) (h₁ : ∀ (a : α), a ∈ l₁ → p a) (h₂ : ∀ (a : α), a ∈ l₂ → p a) : List.pmap f (l₁ ++ l₂) ⋯ = List.pmap f l₁ h₁ ++ List.pmap f l₂ h₂

find

@[simp]

theorem List.find?_mem {α : Type u} {p : α → Bool} {l : List α} {a : α} (H : List.find? p l = some a) : a ∈ l

lookmap

theorem List.lookmap.go_append {α : Type u} (f : α → Option α) (l : List α) (acc : Array α) : List.lookmap.go f l acc = Array.toListAppend acc (List.lookmap f l)

@[simp]

theorem List.lookmap_nil {α : Type u} (f : α → Option α) : List.lookmap f [] = []

@[simp]

theorem List.lookmap_cons_none {α : Type u} (f : α → Option α) {a : α} (l : List α) (h : f a = none) : List.lookmap f (a :: l) = a :: List.lookmap f l

@[simp]

theorem List.lookmap_cons_some {α : Type u} (f : α → Option α) {a : α} {b : α} (l : List α) (h : f a = some b) : List.lookmap f (a :: l) = b :: l

theorem List.lookmap_some {α : Type u} (l : List α) : List.lookmap some l = l

theorem List.lookmap_none {α : Type u} (l : List α) : List.lookmap (fun (x : α) => none) l = l

theorem List.lookmap_congr {α : Type u} {f : α → Option α} {g : α → Option α} {l : List α} : (∀ (a : α), a ∈ l → f a = g a) → List.lookmap f l = List.lookmap g l

theorem List.lookmap_of_forall_not {α : Type u} (f : α → Option α) {l : List α} (H : ∀ (a : α), a ∈ l → f a = none) : List.lookmap f l = l

theorem List.lookmap_map_eq {α : Type u} {β : Type v} (f : α → Option α) (g : α → β) (h : ∀ (a b : α), b ∈ f a → g a = g b) (l : List α) : List.map g (List.lookmap f l) = List.map g l

theorem List.lookmap_id' {α : Type u} (f : α → Option α) (h : ∀ (a b : α), b ∈ f a → a = b) (l : List α) : List.lookmap f l = l

theorem List.length_lookmap {α : Type u} (f : α → Option α) (l : List α) : List.length (List.lookmap f l) = List.length l

filter

filterMap

theorem List.Sublist.map {α : Type u} {β : Type v} (f : α → β) {l₁ : List α} {l₂ : List α} (s : List.Sublist l₁ l₂) : List.Sublist (List.map f l₁) (List.map f l₂)

filter

theorem List.filter_singleton {α : Type u} {p : α → Bool} {a : α} : List.filter p [a] = bif p a then [a] else []

theorem List.filter_eq_foldr {α : Type u} (p : α → Bool) (l : List α) : List.filter p l = List.foldr (fun (a : α) (out : List α) => bif p a then a :: out else out) [] l

@[simp]

theorem List.filter_subset {α : Type u} {p : α → Bool} (l : List α) : List.filter p l ⊆ l

theorem List.of_mem_filter {α : Type u} {p : α → Bool} {a : α} {l : List α} (h : a ∈ List.filter p l) : p a = true

theorem List.mem_of_mem_filter {α : Type u} {p : α → Bool} {a : α} {l : List α} (h : a ∈ List.filter p l) : a ∈ l

theorem List.mem_filter_of_mem {α : Type u} {p : α → Bool} {a : α} {l : List α} (h₁ : a ∈ l) (h₂ : p a = true) : a ∈ List.filter p l

theorem List.monotone_filter_left {α : Type u} (p : α → Bool) ⦃l : List α⦄ ⦃l' : List α⦄ (h : l ⊆ l') : List.filter p l ⊆ List.filter p l'

theorem List.monotone_filter_right {α : Type u} (l : List α) ⦃p : α → Bool⦄ ⦃q : α → Bool⦄ (h : ∀ (a : α), p a = true → q a = true) : List.Sublist (List.filter p l) (List.filter q l)

theorem List.map_filter' {α : Type u} {β : Type v} (p : α → Bool) {f : α → β} (hf : Function.Injective f) (l : List α) [DecidablePred fun (b : β) => ∃ (a : α), p a = true ∧ f a = b] : List.map f (List.filter p l) = List.filter (fun (b : β) => decide (∃ (a : α), p a = true ∧ f a = b)) (List.map f l)

theorem List.filter_attach' {α : Type u} (l : List α) (p : { a : α // a ∈ l } → Bool) [DecidableEq α] : List.filter p (List.attach l) = List.map (Subtype.map id ⋯) (List.attach (List.filter (fun (x : α) => decide (∃ (h : x ∈ l), p { val := x, property := h } = true)) l))

theorem List.filter_attach {α : Type u} (l : List α) (p : α → Bool) : List.filter (fun (x : { x : α // x ∈ l }) => p ↑x) (List.attach l) = List.map (Subtype.map id ⋯) (List.attach (List.filter p l))

theorem List.filter_comm {α : Type u} (p : α → Bool) (q : α → Bool) (l : List α) : List.filter p (List.filter q l) = List.filter q (List.filter p l)

@[simp]

theorem List.filter_true {α : Type u} (l : List α) : List.filter (fun (x : α) => true) l = l

@[simp]

theorem List.filter_false {α : Type u} (l : List α) : List.filter (fun (x : α) => false) l = []

theorem List.span.loop_eq_take_drop {α : Type u} (p : α → Bool) (l₁ : List α) (l₂ : List α) : List.span.loop p l₁ l₂ = (List.reverse l₂ ++ List.takeWhile p l₁, List.dropWhile p l₁)

@[simp]

theorem List.span_eq_take_drop {α : Type u} (p : α → Bool) (l : List α) : List.span p l = (List.takeWhile p l, List.dropWhile p l)

theorem List.dropWhile_nthLe_zero_not {α : Type u} (p : α → Bool) (l : List α) (hl : 0 < List.length (List.dropWhile p l)) : ¬p (List.nthLe (List.dropWhile p l) 0 hl) = true

@[simp]

theorem List.dropWhile_eq_nil_iff {α : Type u} {p : α → Bool} {l : List α} : List.dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.takeWhile_nil {α : Type u} {p : α → Bool} : List.takeWhile p [] = []

theorem List.takeWhile_cons {α : Type u} {p : α → Bool} {l : List α} {x : α} : List.takeWhile p (x :: l) = match p x with | true => x :: List.takeWhile p l | false => []

theorem List.takeWhile_cons_of_pos {α : Type u} {p : α → Bool} {l : List α} {x : α} (h : p x = true) : List.takeWhile p (x :: l) = x :: List.takeWhile p l

theorem List.takeWhile_cons_of_neg {α : Type u} {p : α → Bool} {l : List α} {x : α} (h : ¬p x = true) : List.takeWhile p (x :: l) = []

@[simp]

theorem List.takeWhile_eq_self_iff {α : Type u} {p : α → Bool} {l : List α} : List.takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true

@[simp]

theorem List.takeWhile_eq_nil_iff {α : Type u} {p : α → Bool} {l : List α} : List.takeWhile p l = [] ↔ ∀ (hl : 0 < List.length l), ¬p (List.nthLe l 0 hl) = true

theorem List.mem_takeWhile_imp {α : Type u} {p : α → Bool} {l : List α} {x : α} (hx : x ∈ List.takeWhile p l) : p x = true

theorem List.takeWhile_takeWhile {α : Type u} (p : α → Bool) (q : α → Bool) (l : List α) : List.takeWhile p (List.takeWhile q l) = List.takeWhile (fun (a : α) => decide (p a = true ∧ q a = true)) l

theorem List.takeWhile_idem {α : Type u} {p : α → Bool} {l : List α} : List.takeWhile p (List.takeWhile p l) = List.takeWhile p l

erasep

@[simp]

theorem List.length_eraseP_add_one {α : Type u} {p : α → Bool} {l : List α} {a : α} (al : a ∈ l) (pa : p a = true) : List.length (List.eraseP p l) + 1 = List.length l

erase

@[simp]

theorem List.length_erase_add_one {α : Type u} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : List.length (List.erase l a) + 1 = List.length l

theorem List.map_erase {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {a : α} (l : List α) : List.map f (List.erase l a) = List.erase (List.map f l) (f a)

theorem List.map_foldl_erase {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {l₁ : List α} {l₂ : List α} : List.map f (List.foldl List.erase l₁ l₂) = List.foldl (fun (l : List β) (a : α) => List.erase l (f a)) (List.map f l₁) l₂

theorem List.erase_get {ι : Type u_1} [DecidableEq ι] {l : List ι} (i : Fin (List.length l)) : List.Perm (List.erase l (List.get l i)) (List.eraseIdx l ↑i)

theorem List.eraseIdx_eq_take_drop_succ {ι : Type u_1} {l : List ι} {i : ℕ} : List.eraseIdx l i = List.take i l ++ List.drop (Nat.succ i) l

diff

@[simp]

theorem List.map_diff {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {l₁ : List α} {l₂ : List α} : List.map f (List.diff l₁ l₂) = List.diff (List.map f l₁) (List.map f l₂)

theorem List.erase_diff_erase_sublist_of_sublist {α : Type u} [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₁)

theorem List.choose_spec {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) : List.choose p l hp ∈ l ∧ p (List.choose p l hp)

theorem List.choose_mem {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) : List.choose p l hp ∈ l

theorem List.choose_property {α : Type u} (p : α → Prop) [DecidablePred p] (l : List α) (hp : ∃ (a : α), a ∈ l ∧ p a) : p (List.choose p l hp)

map₂Left'

@[simp]

theorem List.map₂Left'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) : List.map₂Left' f as [] = (List.map (fun (a : α) => f a none) as, [])

map₂Right'

@[simp]

theorem List.map₂Right'_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (bs : List β) : List.map₂Right' f [] bs = (List.map (f none) bs, [])

@[simp]

theorem List.map₂Right'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) : List.map₂Right' f as [] = ([], as)

theorem List.map₂Right'_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (b : β) (bs : List β) : List.map₂Right' f [] (b :: bs) = (f none b :: List.map (f none) bs, [])

@[simp]

theorem List.map₂Right'_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (a : α) (as : List α) (b : β) (bs : List β) : List.map₂Right' f (a :: as) (b :: bs) = let r := List.map₂Right' f as bs; (f (some a) b :: r.1, r.2)

zipLeft'

@[simp]

theorem List.zipLeft'_nil_right {α : Type u} {β : Type v} (as : List α) : List.zipLeft' as [] = (List.map (fun (a : α) => (a, none)) as, [])

@[simp]

theorem List.zipLeft'_nil_left {α : Type u} {β : Type v} (bs : List β) : List.zipLeft' [] bs = ([], bs)

theorem List.zipLeft'_cons_nil {α : Type u} {β : Type v} (a : α) (as : List α) : List.zipLeft' (a :: as) [] = ((a, none) :: List.map (fun (a : α) => (a, none)) as, [])

@[simp]

theorem List.zipLeft'_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : List.zipLeft' (a :: as) (b :: bs) = let r := List.zipLeft' as bs; ((a, some b) :: r.1, r.2)

zipRight'

@[simp]

theorem List.zipRight'_nil_left {α : Type u} {β : Type v} (bs : List β) : List.zipRight' [] bs = (List.map (fun (b : β) => (none, b)) bs, [])

@[simp]

theorem List.zipRight'_nil_right {α : Type u} {β : Type v} (as : List α) : List.zipRight' as [] = ([], as)

theorem List.zipRight'_nil_cons {α : Type u} {β : Type v} (b : β) (bs : List β) : List.zipRight' [] (b :: bs) = ((none, b) :: List.map (fun (b : β) => (none, b)) bs, [])

@[simp]

theorem List.zipRight'_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : List.zipRight' (a :: as) (b :: bs) = let r := List.zipRight' as bs; ((some a, b) :: r.1, r.2)

map₂Left

@[simp]

theorem List.map₂Left_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) : List.map₂Left f as [] = List.map (fun (a : α) => f a none) as

theorem List.map₂Left_eq_map₂Left' {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) (bs : List β) : List.map₂Left f as bs = (List.map₂Left' f as bs).1

theorem List.map₂Left_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → Option β → γ) (as : List α) (bs : List β) : List.length as ≤ List.length bs → List.map₂Left f as bs = List.zipWith (fun (a : α) (b : β) => f a (some b)) as bs

map₂Right

@[simp]

theorem List.map₂Right_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (bs : List β) : List.map₂Right f [] bs = List.map (f none) bs

@[simp]

theorem List.map₂Right_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) : List.map₂Right f as [] = []

theorem List.map₂Right_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (b : β) (bs : List β) : List.map₂Right f [] (b :: bs) = f none b :: List.map (f none) bs

@[simp]

theorem List.map₂Right_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (a : α) (as : List α) (b : β) (bs : List β) : List.map₂Right f (a :: as) (b :: bs) = f (some a) b :: List.map₂Right f as bs

theorem List.map₂Right_eq_map₂Right' {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) (bs : List β) : List.map₂Right f as bs = (List.map₂Right' f as bs).1

theorem List.map₂Right_eq_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (as : List α) (bs : List β) (h : List.length bs ≤ List.length as) : List.map₂Right f as bs = List.zipWith (fun (a : α) (b : β) => f (some a) b) as bs

zipLeft

@[simp]

theorem List.zipLeft_nil_right {α : Type u} {β : Type v} (as : List α) : List.zipLeft as [] = List.map (fun (a : α) => (a, none)) as

@[simp]

theorem List.zipLeft_nil_left {α : Type u} {β : Type v} (bs : List β) : List.zipLeft [] bs = []

theorem List.zipLeft_cons_nil {α : Type u} {β : Type v} (a : α) (as : List α) : List.zipLeft (a :: as) [] = (a, none) :: List.map (fun (a : α) => (a, none)) as

@[simp]

theorem List.zipLeft_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : List.zipLeft (a :: as) (b :: bs) = (a, some b) :: List.zipLeft as bs

theorem List.zipLeft_eq_zipLeft' {α : Type u} {β : Type v} (as : List α) (bs : List β) : List.zipLeft as bs = (List.zipLeft' as bs).1

zipRight

@[simp]

theorem List.zipRight_nil_left {α : Type u} {β : Type v} (bs : List β) : List.zipRight [] bs = List.map (fun (b : β) => (none, b)) bs

@[simp]

theorem List.zipRight_nil_right {α : Type u} {β : Type v} (as : List α) : List.zipRight as [] = []

theorem List.zipRight_nil_cons {α : Type u} {β : Type v} (b : β) (bs : List β) : List.zipRight [] (b :: bs) = (none, b) :: List.map (fun (b : β) => (none, b)) bs

@[simp]

theorem List.zipRight_cons_cons {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β) : List.zipRight (a :: as) (b :: bs) = (some a, b) :: List.zipRight as bs

theorem List.zipRight_eq_zipRight' {α : Type u} {β : Type v} (as : List α) (bs : List β) : List.zipRight as bs = (List.zipRight' as bs).1

toChunks

Forall

@[simp]

theorem List.forall_cons {α : Type u} (p : α → Prop) (x : α) (l : List α) : List.Forall p (x :: l) ↔ p x ∧ List.Forall p l

theorem List.forall_iff_forall_mem {α : Type u} {p : α → Prop} {l : List α} : List.Forall p l ↔ ∀ (x : α), x ∈ l → p x

theorem List.Forall.imp {α : Type u} {p : α → Prop} {q : α → Prop} (h : ∀ (x : α), p x → q x) {l : List α} : List.Forall p l → List.Forall q l

@[simp]

theorem List.forall_map_iff {α : Type u} {β : Type v} {l : List α} {p : β → Prop} (f : α → β) : List.Forall p (List.map f l) ↔ List.Forall (p ∘ f) l

instance List.instDecidablePredListForall {α : Type u} (p : α → Prop) [DecidablePred p] : DecidablePred (List.Forall p)

Equations

• List.instDecidablePredListForall p x = decidable_of_iff' (∀ (x_1 : α), x_1 ∈ x → p x_1) ⋯

Miscellaneous lemmas

theorem List.getLast_reverse {α : Type u} {l : List α} (hl : List.reverse l ≠ []) (hl' : optParam (0 < List.length l) ⋯) : List.getLast (List.reverse l) hl = List.get l { val := 0, isLt := hl' }

@[deprecated]

theorem List.ilast'_mem {α : Type u} (a : α) (l : List α) : List.ilast' a l ∈ a :: l

@[simp]

theorem List.get_attach {α : Type u} (L : List α) (i : Fin (List.length (List.attach L))) : ↑(List.get (List.attach L) i) = List.get L { val := ↑i, isLt := ⋯ }

@[simp, deprecated List.get_attach]

theorem List.nthLe_attach {α : Type u} (L : List α) (i : ℕ) (H : i < List.length (List.attach L)) : ↑(List.nthLe (List.attach L) i H) = List.nthLe L i ⋯

@[simp]

theorem List.mem_map_swap {α : Type u} {β : Type v} (x : α) (y : β) (xs : List (α × β)) : (y, x) ∈ List.map Prod.swap xs ↔ (x, y) ∈ xs

theorem List.dropSlice_eq {α : Type u} (xs : List α) (n : ℕ) (m : ℕ) : List.dropSlice n m xs = List.take n xs ++ List.drop (n + m) xs

theorem List.sizeOf_dropSlice_lt {α : Type u} [SizeOf α] (i : ℕ) (j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < List.length xs) : sizeOf (List.dropSlice i j xs) < sizeOf xs

theorem List.disjoint_pmap {α : Type u_2} {β : Type u_3} {p : α → Prop} {f : (a : α) → p a → β} {s : List α} {t : List α} (hs : ∀ (a : α), a ∈ s → p a) (ht : ∀ (a : α), a ∈ t → p a) (hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a') (h : List.Disjoint s t) : List.Disjoint (List.pmap f s hs) (List.pmap f t ht)

The images of disjoint lists under a partially defined map are disjoint

theorem List.disjoint_map {α : Type u_2} {β : Type u_3} {f : α → β} {s : List α} {t : List α} (hf : Function.Injective f) (h : List.Disjoint s t) : List.Disjoint (List.map f s) (List.map f t)

The images of disjoint lists under an injective map are disjoint