Basic properties of Lists

ink

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

ink

theorem List.cons_ne_self {α : Type u_1} (a : α) (l : List α) : a :: l ≠ l

ink

theorem List.head_eq_of_cons_eq : ∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → h₁ = h₂

ink

theorem List.tail_eq_of_cons_eq : ∀ {α : Type u_1} {h₁ : α} {t₁ : List α} {h₂ : α} {t₂ : List α}, h₁ :: t₁ = h₂ :: t₂ → t₁ = t₂

ink

theorem List.cons_inj {α : Type u_1} (a : α) {l : List α} {l' : List α} : a :: l = a :: l' ↔ l = l'

ink

theorem List.exists_cons_of_ne_nil {α : Type u_1} {l : List α} : l ≠ [] → ∃ b L, l = b :: L

length

ink

@[simp]

theorem List.length_singleton {α : Type u_1} (a : α) : List.length [a] = 1

ink

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

ink

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

ink

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

ink

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

ink

theorem List.exists_mem_of_ne_nil {α : Type u_1} (l : List α) (h : l ≠ []) : ∃ x, x ∈ l

ink

theorem List.length_eq_one {α : Type u_1} {l : List α} : List.length l = 1 ↔ ∃ a, l = [a]

mem

ink

@[simp]

theorem List.not_mem_nil {α : Type u_1} (a : α) : ¬a ∈ []

ink

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

ink

@[simp]

theorem List.mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l ↔ a = b ∨ a ∈ l

ink

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

ink

theorem List.mem_cons_of_mem {α : Type u_1} (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l

ink

theorem List.mem_singleton_self {α : Type u_1} (a : α) : a ∈ [a]

ink

theorem List.eq_of_mem_singleton {α : Type u_1} {a : α} {b : α} : a ∈ [b] → a = b

ink

@[simp]

theorem List.mem_singleton {α : Type u_1} {a : α} {b : α} : a ∈ [b] ↔ a = b

ink

theorem List.mem_of_mem_cons_of_mem {α : Type u_1} {a : α} {b : α} {l : List α} : a ∈ b :: l → b ∈ l → a ∈ l

ink

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

ink

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

ink

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

append

ink

theorem List.append_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, List.append l₁ l₂ = l₁ ++ l₂

ink

@[simp]

theorem List.append_eq_nil : ∀ {α : Type u_1} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []

ink

theorem List.append_ne_nil_of_ne_nil_left {α : Type u_1} (s : List α) (t : List α) : s ≠ [] → s ++ t ≠ []

ink

theorem List.append_ne_nil_of_ne_nil_right {α : Type u_1} (s : List α) (t : List α) : t ≠ [] → s ++ t ≠ []

ink

@[simp]

theorem List.nil_eq_append : ∀ {α : Type u_1} {a b : List α}, [] = a ++ b ↔ a = [] ∧ b = []

ink

theorem List.append_ne_nil_of_left_ne_nil {α : Type u_1} (a : List α) (b : List α) (h0 : a ≠ []) : a ++ b ≠ []

ink

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

ink

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

ink

theorem List.append_eq_append_iff {α : Type u_1} {a : List α} {b : List α} {c : List α} {d : List α} : a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b

ink

@[simp]

theorem List.mem_append {α : Type u_1} {a : α} {s : List α} {t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

ink

theorem List.mem_append_eq {α : Type u_1} (a : α) (s : List α) (t : List α) : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t)

ink

theorem List.mem_append_left {α : Type u_1} {a : α} {l₁ : List α} (l₂ : List α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂

ink

theorem List.mem_append_right {α : Type u_1} {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂

map

ink

theorem List.map_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : List.map f [a] = [f a]

ink

theorem List.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {l : List α} : b ∈ List.map f l ↔ ∃ a, a ∈ l ∧ b = f a

ink

theorem List.mem_map_of_mem {α : Type u_1} {β : Type u_2} {a : α} {l : List α} (f : α → β) (h : a ∈ l) : f a ∈ List.map f l

ink

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, a ∈ l ∧ b = f a

ink

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)

ink

@[simp]

theorem List.map_eq_nil {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} : List.map f l = [] ↔ l = []

ink

@[simp]

theorem List.length_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (l₁ : List α) (l₂ : List β) : List.length (List.zipWith f l₁ l₂) = min (List.length l₁) (List.length l₂)

join

ink

theorem List.join_nil {α : Type u_1} : List.join [] = []

ink

theorem List.join_cons {α : Type u_1} {a : List α} {l : List (List α)} : List.join (a :: l) = a ++ List.join l

ink

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

ink

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

ink

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

bind

ink

theorem List.mem_bind {α : Type u_1} {β : Type u_2} {f : α → List β} {b : β} {l : List α} : b ∈ List.bind l f ↔ ∃ a, a ∈ l ∧ b ∈ f a

ink

theorem List.exists_of_mem_bind {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : α → List β} : b ∈ List.bind l f → ∃ a, a ∈ l ∧ b ∈ f a

ink

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 ∈ List.bind l f

ink

theorem List.bind_map {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (g : α → List β) (l : List α) : List.map f (List.bind l g) = List.bind l fun a => List.map f (g a)

set-theoretic notation of Lists

ink

@[simp]

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

bounded quantifiers over Lists

ink

theorem List.exists_mem_nil {α : Type u_1} (p : α → Prop) : ¬∃ x, x ∈ [] ∧ p x

ink

theorem List.forall_mem_nil {α : Type u_1} (p : α → Prop) (x : α) : x ∈ [] → p x

ink

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

ink

theorem List.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : List α} : ((x : α) → x ∈ a :: l → p x) ↔ p a ∧ ((x : α) → x ∈ l → p x)

ink

theorem List.forall_mem_singleton {α : Type u_1} {p : α → Prop} {a : α} : ((x : α) → x ∈ [a] → p x) ↔ p a

ink

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

ink

theorem List.subset_def {α : Type u_1} {l₁ : List α} {l₂ : List α} : l₁ ⊆ l₂ ↔ ∀ {a : α}, a ∈ l₁ → a ∈ l₂

ink

@[simp]

theorem List.nil_subset {α : Type u_1} (l : List α) : [] ⊆ l

ink

@[simp]

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

ink

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

ink

@[simp]

theorem List.subset_cons {α : Type u_1} (a : α) (l : List α) : l ⊆ a :: l

ink

theorem List.subset_of_cons_subset {α : Type u_1} {a : α} {l₁ : List α} {l₂ : List α} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂

ink

theorem List.subset_cons_of_subset {α : Type u_1} (a : α) {l₁ : List α} {l₂ : List α} : l₁ ⊆ l₂ → l₁ ⊆ a :: l₂

ink

theorem List.cons_subset_cons {α : Type u_1} {l₁ : List α} {l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a :: l₁ ⊆ a :: l₂

ink

@[simp]

theorem List.subset_append_left {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₁ ⊆ l₁ ++ l₂

ink

@[simp]

theorem List.subset_append_right {α : Type u_1} (l₁ : List α) (l₂ : List α) : l₂ ⊆ l₁ ++ l₂

ink

theorem List.subset_append_of_subset_left {α : Type u_1} {l : List α} {l₁ : List α} (l₂ : List α) : l ⊆ l₁ → l ⊆ l₁ ++ l₂

ink

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

ink

@[simp]

theorem List.cons_subset : ∀ {α : Type u_1} {a : α} {l m : List α}, a :: l ⊆ m ↔ a ∈ m ∧ l ⊆ m

ink

@[simp]

theorem List.append_subset {α : Type u_1} {l₁ : List α} {l₂ : List α} {l : List α} : l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l

ink

theorem List.subset_nil {α : Type u_1} {l : List α} : l ⊆ [] ↔ l = []

ink

theorem List.eq_nil_iff_forall_not_mem {α : Type u_1} {l : List α} : l = [] ↔ ∀ (a : α), ¬a ∈ l

ink

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

ink

theorem List.replicate_succ {α : Type u_1} (a : α) (n : Nat) : List.replicate (n + 1) a = a :: List.replicate n a

ink

theorem List.mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} : b ∈ List.replicate n a ↔ n ≠ 0 ∧ b = a

ink

theorem List.eq_of_mem_replicate {α : Type u_1} {a : α} {b : α} {n : Nat} (h : b ∈ List.replicate n a) : b = a

getLast

ink

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

ink

@[simp]

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

ink

theorem List.getLast_concat : ∀ {α : Type u_1} {l : List α} {a : α} (h : List.concat l a ≠ []), List.getLast (List.concat l a) h = a

sublists

ink

@[simp]

theorem List.nil_sublist {α : Type u_1} (l : List α) : List.Sublist [] l

ink

@[simp]

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

ink

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

ink

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

Equations

• List.instTransListSublist = { trans := (_ : ∀ {a b c : List α}, List.Sublist a b → List.Sublist b c → List.Sublist a c) }

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

head

ink

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

ink

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

tail

ink

@[simp]

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

ink

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

ink

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

next?

ink

@[simp]

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

ink

@[simp]

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

getLast

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

dropLast

ink

@[simp]

theorem List.dropLast_nil {α : Type u_1} : List.dropLast [] = []

ink

@[simp]

theorem List.dropLast_single : ∀ {α : Type u_1} {a : α}, List.dropLast [a] = []

ink

@[simp]

theorem List.dropLast_cons₂ : ∀ {α : Type u_1} {a b : α} {l : List α}, List.dropLast (a :: b :: l) = a :: List.dropLast (b :: l)

ink

@[simp]

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

ink

@[simp]

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

nth element

ink

@[simp]

theorem List.get_cons_zero {α : Type u_1} {a : α} {as : List α} : List.get (a :: as) { val := 0, isLt := (_ : 0 < Nat.succ (List.length as)) } = a

ink

@[simp]

theorem List.get_cons_succ {α : Type u_1} {i : Nat} {a : α} {as : List α} {h : i + 1 < List.length (a :: as)} : List.get (a :: as) { val := i + 1, isLt := h } = List.get as { val := i, isLt := (_ : i < List.length as) }

ink

theorem List.get_of_mem {α : Type u_1} {a : α} {l : List α} : a ∈ l → ∃ n, List.get l n = a

ink

theorem List.get?_eq_get {α : Type u_1} {l : List α} {n : Nat} (h : n < List.length l) : List.get? l n = some (List.get l { val := n, isLt := h })

ink

theorem List.get?_len_le {α : Type u_1} {l : List α} {n : Nat} : List.length l ≤ n → List.get? l n = none

ink

theorem List.get?_eq_some : ∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, List.get? l n = some a ↔ ∃ h, List.get l { val := n, isLt := h } = a

ink

@[simp]

theorem List.get?_eq_none : ∀ {α : Type u_1} {l : List α} {n : Nat}, List.get? l n = none ↔ List.length l ≤ n

ink

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

ink

theorem List.get_mem {α : Type u_1} (l : List α) (n : Nat) (h : n < List.length l) : List.get l { val := n, isLt := h } ∈ l

ink

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

ink

theorem List.mem_iff_get {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ n, List.get l n = a

ink

theorem List.Fin.exists_iff {n : Nat} (p : Fin n → Prop) : (∃ i, p i) ↔ ∃ i h, p { val := i, isLt := h }

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

theorem List.get?_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (n : Nat) : List.get? (List.map f l) n = Option.map f (List.get? l n)

ink

@[simp]

theorem List.get_map {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Fin (List.length (List.map f l))} : List.get (List.map f l) n = f (List.get l { val := n.val, isLt := (_ : n.val < List.length l) })

ink

theorem List.get_of_eq {α : Type u_1} {l : List α} {l' : List α} (h : l = l') (i : Fin (List.length l)) : List.get l i = List.get l' { val := i.val, isLt := (_ : i.val < List.length l') }

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).

ink

@[simp]

theorem List.get_singleton {α : Type u_1} (a : α) (n : Fin 1) : List.get [a] n = a

ink

theorem List.get_zero {α : Type u_1} {l : List α} (h : 0 < List.length l) : some (List.get l { val := 0, isLt := h }) = List.head? l

ink

theorem List.get_append {α : Type u_1} {l₁ : List α} {l₂ : List α} (n : Nat) (h : n < List.length l₁) : List.get (l₁ ++ l₂) { val := n, isLt := (_ : n < List.length (l₁ ++ l₂)) } = List.get l₁ { val := n, isLt := h }

ink

theorem List.get?_append_right {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} : List.length l₁ ≤ n → List.get? (l₁ ++ l₂) n = List.get? l₂ (n - List.length l₁)

ink

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

ink

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

ink

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

ink

theorem List.get_of_append {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α} {n : Nat} {l : List α} (eq : l = l₁ ++ a :: l₂) (h : List.length l₁ = n) : List.get l { val := n, isLt := (_ : n < List.length l) } = a

ink

@[simp]

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

ink

theorem List.get?_append {α : Type u_1} {l₁ : List α} {l₂ : List α} {n : Nat} (hn : n < List.length l₁) : List.get? (l₁ ++ l₂) n = List.get? l₁ n

ink

theorem List.getLast_eq_get {α : Type u_1} (l : List α) (h : l ≠ []) : List.getLast l h = List.get l { val := List.length l - 1, isLt := (_ : List.length l - 1 < List.length l) }

ink

theorem List.getLast?_eq_get? {α : Type u_1} (l : List α) : List.getLast? l = List.get? l (List.length l - 1)

ink

@[simp]

theorem List.get?_concat_length {α : Type u_1} (l : List α) (a : α) : List.get? (l ++ [a]) (List.length l) = some a

ink

@[simp]

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

ink

theorem List.get_cons_length {α : Type u_1} (x : α) (xs : List α) (n : Nat) (h : n = List.length xs) : List.get (x :: xs) { val := n, isLt := (_ : n < Nat.succ (List.length xs)) } = List.getLast (x :: xs) (_ : x :: xs ≠ [])

ink

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

ink

theorem List.ext_get {α : Type u_1} {l₁ : List α} {l₂ : List α} (hl : List.length l₁ = List.length l₂) (h : ∀ (n : Nat) (h₁ : n < List.length l₁) (h₂ : n < List.length l₂), List.get l₁ { val := n, isLt := h₁ } = List.get l₂ { val := n, isLt := h₂ }) : l₁ = l₂

ink

theorem List.get?_reverse' {α : Type u_1} {l : List α} (i : Nat) (j : Nat) : i + j + 1 = List.length l → List.get? (List.reverse l) i = List.get? l j

ink

theorem List.get?_reverse {α : Type u_1} {l : List α} (i : Nat) (h : i < List.length l) : List.get? (List.reverse l) i = List.get? l (List.length l - 1 - i)

ink

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

ink

theorem List.getD_eq_get? {α : Type u_1} (l : List α) (n : Nat) (a : α) : List.getD l n a = Option.getD (List.get? l n) a

take and drop

ink

@[simp]

theorem List.length_take {α : Type u_1} (i : Nat) (l : List α) : List.length (List.take i l) = min i (List.length l)

ink

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

ink

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

ink

theorem List.get_cons_drop {α : Type u_1} (l : List α) (i : Fin (List.length l)) : List.get l i :: List.drop (i.val + 1) l = List.drop i.val l

ink

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₁ l₂, l = l₁ ++ l₂ ∧ List.map f l₁ = s₁ ∧ List.map f l₂ = s₂

ink

theorem List.mem_of_mem_drop {α : Type u_1} {a : α} {n : Nat} {l : List α} : a ∈ List.drop n l → a ∈ l

modify nth

ink

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

ink

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

ink

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

ink

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

ink

theorem List.modifyNthTail_add {α : Type u_1} (f : List α → List α) (n : Nat) (l₁ : List α) (l₂ : List α) : List.modifyNthTail f (List.length l₁ + n) (l₁ ++ l₂) = l₁ ++ List.modifyNthTail f n l₂

ink

theorem List.exists_of_modifyNthTail {α : Type u_1} (f : List α → List α) {n : Nat} {l : List α} (h : n ≤ List.length l) : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.length l₁ = n ∧ List.modifyNthTail f n l = l₁ ++ f l₂

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem List.exists_of_modifyNth {α : Type u_1} (f : α → α) {n : Nat} {l : List α} (h : n < List.length l) : ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ List.length l₁ = n ∧ List.modifyNth f n l = l₁ ++ f a :: l₂

set

ink

theorem List.set_eq_modifyNth {α : Type u_1} (a : α) (n : Nat) (l : List α) : List.set l n a = List.modifyNth (fun x => a) n l

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

theorem List.set_succ {α : Type u_1} (x : α) (xs : List α) (n : Nat) (a : α) : List.set (x :: xs) (Nat.succ n) a = x :: List.set xs n a

ink

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

ink

@[simp]

theorem List.get_set_eq {α : Type u_1} (l : List α) (i : Nat) (a : α) (h : i < List.length (List.set l i a)) : List.get (List.set l i a) { val := i, isLt := h } = a

ink

@[simp]

theorem List.get_set_ne {α : Type u_1} {l : List α} {i : Nat} {j : Nat} (h : i ≠ j) (a : α) (hj : j < List.length (List.set l i a)) : List.get (List.set l i a) { val := j, isLt := hj } = List.get l { val := j, isLt := (_ : j < List.length l) }

ink

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

ink

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

remove nth

ink

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

tail

ink

@[simp]

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

all / any

ink

@[simp]

theorem List.all_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : List.all l p = true ↔ ∀ (x : α), x ∈ l → p x = true

ink

@[simp]

theorem List.any_eq_true {α : Type u_1} {p : α → Bool} {l : List α} : List.any l p = true ↔ ∃ x, x ∈ l ∧ p x = true

reverse

ink

@[simp]

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

ink

@[simp]

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

insert

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

eraseP

ink

@[simp]

theorem List.eraseP_nil : ∀ {α : Type u_1} {p : α → Bool}, List.eraseP p [] = []

ink

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

ink

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

ink

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

ink

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

ink

theorem List.exists_of_eraseP {α : Type u_1} {p : α → Bool} {l : List α} {a : α} (al : a ∈ l) (pa : p a = true) : ∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂

ink

theorem List.exists_or_eq_self_of_eraseP {α : Type u_1} (p : α → Bool) (l : List α) : List.eraseP p l = l ∨ ∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁ ++ a :: l₂ ∧ List.eraseP p l = l₁ ++ l₂

ink

@[simp]

theorem List.length_eraseP_of_mem : ∀ {α : Type u_1} {a : α} {l : List α} {p : α → Bool}, a ∈ l → p a = true → List.length (List.eraseP p l) = Nat.pred (List.length l)

ink

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₂

ink

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₂

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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)

ink

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

ink

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

ink

@[simp]

theorem List.erase_nil {α : Type u_1} [inst : DecidableEq α] (a : α) : List.erase [] a = []

ink

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

ink

@[simp]

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

ink

@[simp]

theorem List.erase_cons_tail {α : Type u_1} [inst : DecidableEq α] {a : α} {b : α} (l : List α) (h : b ≠ a) : List.erase (b :: l) a = b :: List.erase l a

ink

theorem List.erase_eq_eraseP {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) : List.erase l a = List.eraseP (fun b => decide (a = b)) l

ink

theorem List.erase_of_not_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α} : ¬a ∈ l → List.erase l a = l

ink

theorem List.exists_erase_eq {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ List.erase l a = l₁ ++ l₂

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

filter and partition

ink

theorem List.mem_filter : ∀ {α : Type u_1} {x : α} {p : α → Bool} {as : List α}, x ∈ List.filter p as ↔ x ∈ as ∧ p x = true

ink

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

ink

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) = (List.reverse as ++ List.filter p l, List.reverse bs ++ List.filter (not ∘ p) l)

pairwise

ink

theorem List.Pairwise.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α} {R : α → α → Prop}, List.Sublist l₁ l₂ → List.Pairwise R l₂ → List.Pairwise R l₁

ink

theorem List.pairwise_map {α : Type u_1} : ∀ {α : Type u_2} {f : α → α} {R : α → α → Prop} {l : List α}, List.Pairwise R (List.map f l) ↔ List.Pairwise (fun a b => R (f a) (f b)) l

ink

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)

ink

theorem List.pairwise_reverse {α : Type u_1} {R : α → α → Prop} {l : List α} : List.Pairwise R (List.reverse l) ↔ List.Pairwise (fun a b => R b a) l

ink

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

ink

@[simp]

theorem List.length_replaceF : ∀ {α : Type u_1} {f : α → Option α} {l : List α}, List.length (List.replaceF f l) = List.length l

disjoint

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

theorem List.disjoint_take_drop {α : Type u_1} {m : Nat} {n : Nat} {l : List α} : List.Nodup l → m ≤ n → List.Disjoint (List.take m l) (List.drop n l)

foldl / foldr

ink

theorem List.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) : List.foldl g init (List.map f l) = List.foldl (fun x y => g x (f y)) init l

ink

theorem List.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) : List.foldr g init (List.map f l) = List.foldr (fun x y => g (f x) y) init l

ink

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)

ink

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

ink

@[simp]

theorem List.nil_union {α : Type u_1} [inst : DecidableEq α] (l : List α) : List.union [] l = l

ink

@[simp]

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

ink

@[simp]

theorem List.mem_union_iff {α : Type u_1} [inst : DecidableEq α] {x : α} {l₁ : List α} {l₂ : List α} : x ∈ List.union l₁ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂

inter

ink

@[simp]

theorem List.mem_inter_iff {α : Type u_1} [inst : DecidableEq α] {x : α} {l₁ : List α} {l₂ : List α} : x ∈ List.inter l₁ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂

product

ink

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

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

leftpad

ink

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

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

ink

theorem List.leftpad_prefix {α : Type u_1} (n : Nat) (a : α) (l : List α) : List.replicate (n - List.length l) a <+: List.leftpad n a l

ink

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

monadic operations

ink

@[simp]

theorem List.forIn_eq_forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] : List.forIn = forIn

ink

theorem List.forIn_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [inst : LawfulMonad m] (f : α → β → m (ForInStep β)) (l : List α) (init : β) : forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)

ink

@[simp]

theorem List.forM_append {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] [inst : LawfulMonad m] (l₁ : List α) (l₂ : List α) (f : α → m PUnit) : List.forM (l₁ ++ l₂) f = do List.forM l₁ f List.forM l₂ f