# Documentation

## Batteries.Data.List.Lemmas

### mem #

@[simp]
theorem List.mem_toArray {α : Type u_1} {a : α} {l : List α} :
a l

### drop #

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

### zipWith #

theorem List.zipWith_distrib_tail :
∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : αα_1α_2} {l : List α} {l' : List α_1}, (List.zipWith f l l').tail = List.zipWith f l.tail l'.tail

### List subset #

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

### sublists #

@[simp]
theorem List.nil_sublist {α : Type u_1} (l : List α) :
[].Sublist l
@[simp]
theorem List.Sublist.refl {α : Type u_1} (l : List α) :
l.Sublist l
theorem List.Sublist.trans {α : Type u_1} {l₁ : List α} {l₂ : List α} {l₃ : List α} (h₁ : l₁.Sublist l₂) (h₂ : l₂.Sublist l₃) :
l₁.Sublist l₃
instance List.instTransSublist {α : Type u_1} :
Trans List.Sublist List.Sublist List.Sublist
Equations
• List.instTransSublist = { trans := }
@[simp]
theorem List.sublist_cons {α : Type u_1} (a : α) (l : List α) :
l.Sublist (a :: l)
theorem List.sublist_of_cons_sublist :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist l₂l₁.Sublist l₂
@[simp]
theorem List.sublist_append_left {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₁.Sublist (l₁ ++ l₂)
@[simp]
theorem List.sublist_append_right {α : Type u_1} (l₁ : List α) (l₂ : List α) :
l₂.Sublist (l₁ ++ l₂)
theorem List.sublist_append_of_sublist_left :
∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Sublist l₁l.Sublist (l₁ ++ l₂)
theorem List.sublist_append_of_sublist_right :
∀ {α : Type u_1} {l l₂ l₁ : List α}, l.Sublist l₂l.Sublist (l₁ ++ l₂)
@[simp]
theorem List.cons_sublist_cons :
∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Sublist (a :: l₂) l₁.Sublist l₂
@[simp]
theorem List.append_sublist_append_left :
∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Sublist (l ++ l₂) l₁.Sublist l₂
theorem List.Sublist.append_left :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂∀ (l : List α), (l ++ l₁).Sublist (l ++ l₂)
theorem List.Sublist.append_right :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂∀ (l : List α), (l₁ ++ l).Sublist (l₂ ++ l)
theorem List.sublist_or_mem_of_sublist :
∀ {α : Type u_1} {l l₁ : List α} {a : α} {l₂ : List α}, l.Sublist (l₁ ++ a :: l₂)l.Sublist (l₁ ++ l₂) a l
theorem List.Sublist.reverse :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₁.reverse.Sublist l₂.reverse
@[simp]
theorem List.reverse_sublist :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse.Sublist l₂.reverse l₁.Sublist l₂
@[simp]
theorem List.append_sublist_append_right :
∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l₁ ++ l).Sublist (l₂ ++ l) l₁.Sublist l₂
theorem List.Sublist.append :
∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, l₁.Sublist l₂r₁.Sublist r₂(l₁ ++ r₁).Sublist (l₂ ++ r₂)
theorem List.Sublist.subset :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₁ l₂
instance List.instTransSublistSubset {α : Type u_1} :
Trans List.Sublist Subset Subset
Equations
• List.instTransSublistSubset = { trans := }
instance List.instTransSubsetSublist {α : Type u_1} :
Trans Subset List.Sublist Subset
Equations
• List.instTransSubsetSublist = { trans := }
instance List.instTransMemSublist {α : Type u_1} :
Trans Membership.mem List.Sublist Membership.mem
Equations
• List.instTransMemSublist = { trans := }
theorem List.Sublist.length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₁.length l₂.length
@[simp]
theorem List.sublist_nil {α : Type u_1} {l : List α} :
l.Sublist [] l = []
theorem List.Sublist.eq_of_length :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₁.length = l₂.lengthl₁ = l₂
theorem List.Sublist.eq_of_length_le :
∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂l₂.length l₁.lengthl₁ = l₂
@[simp]
theorem List.singleton_sublist {α : Type u_1} {a : α} {l : List α} :
[a].Sublist l a l
@[simp]
theorem List.replicate_sublist_replicate {α : Type u_1} {m : Nat} {n : Nat} (a : α) :
().Sublist () m n
theorem List.isSublist_iff_sublist {α : Type u_1} [BEq α] [] {l₁ : List α} {l₂ : List α} :
l₁.isSublist l₂ = true l₁.Sublist l₂
instance List.instDecidableSublistOfDecidableEq {α : Type u_1} [] (l₁ : List α) (l₂ : List α) :
Decidable (l₁.Sublist l₂)
Equations

### tail #

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

### next? #

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

### get? #

theorem List.getElem_eq_iff {α : Type u_1} {x : α} {l : List α} {n : Nat} {h : n < l.length} :
l[n] = x l[n]? = some x
@[deprecated List.getElem_eq_iff]
theorem List.get_eq_iff :
∀ {α : Type u_1} {l : List α} {n : Fin l.length} {x : α}, l.get n = x l.get? n = some x
theorem List.getElem?_inj {i : Nat} :
∀ {α : Type u_1} {xs : List α} {j : Nat}, i < xs.lengthxs.Nodupxs[i]? = xs[j]?i = j
@[deprecated List.getElem?_inj]
theorem List.get?_inj {i : Nat} :
∀ {α : Type u_1} {xs : List α} {j : Nat}, i < xs.lengthxs.Nodupxs.get? i = xs.get? ji = j

### drop #

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

### modifyNth #

@[simp]
theorem List.modifyNth_nil {α : Type u_1} (f : αα) (n : Nat) :
List.modifyNth f n [] = []
@[simp]
theorem List.modifyNth_zero_cons {α : Type u_1} (f : αα) (a : α) (l : List α) :
List.modifyNth f 0 (a :: l) = f a :: l
@[simp]
theorem List.modifyNth_succ_cons {α : Type u_1} (f : αα) (a : α) (l : List α) (n : Nat) :
List.modifyNth f (n + 1) (a :: l) = a ::
theorem List.modifyNthTail_id {α : Type u_1} (n : Nat) (l : List α) :
= l
theorem List.eraseIdx_eq_modifyNthTail {α : Type u_1} (n : Nat) (l : List α) :
l.eraseIdx n = List.modifyNthTail List.tail n l
@[deprecated List.eraseIdx_eq_modifyNthTail]
theorem List.removeNth_eq_nth_tail {α : Type u_1} (n : Nat) (l : List α) :
l.eraseIdx n = List.modifyNthTail List.tail n l

Alias of List.eraseIdx_eq_modifyNthTail.

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

### set #

theorem List.set_eq_modifyNth {α : Type u_1} (a : α) (n : Nat) (l : List α) :
l.set n a = List.modifyNth (fun (x : α) => a) n l
theorem List.set_eq_take_cons_drop {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) :
l.set n a = ++ a :: List.drop (n + 1) l
theorem List.modifyNth_eq_set_get? {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
= ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l theorem List.modifyNth_eq_set_get {α : Type u_1} (f : αα) {n : Nat} {l : List α} (h : n < l.length) : = l.set n (f (l.get n, h)) theorem List.exists_of_set {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < l.length) : ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ l₁.length = n l.set n a' = l₁ ++ a' :: l₂ theorem List.exists_of_set' {α : Type u_1} {n : Nat} {a' : α} {l : List α} (h : n < l.length) : ∃ (l₁ : List α), ∃ (l₂ : List α), l = l₁ ++ l[n] :: l₂ l₁.length = n l.set n a' = l₁ ++ a' :: l₂ @[simp] theorem List.getElem?_set_eq' {α : Type u_1} (a : α) (n : Nat) (l : List α) : (l.set n a)[n]? = (fun (x : α) => a) <$> l[n]?
@[deprecated List.getElem?_set_eq']
theorem List.get?_set_eq {α : Type u_1} (a : α) (n : Nat) (l : List α) :
(l.set n a).get? n = (fun (x : α) => a) <$> l.get? n theorem List.getElem?_set_eq_of_lt {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) : (l.set n a)[n]? = some a @[deprecated List.getElem?_set_eq_of_lt] theorem List.get?_set_eq_of_lt {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) : (l.set n a).get? n = some a @[deprecated List.getElem?_set_ne] theorem List.get?_set_ne {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : m n) : (l.set m a).get? n = l.get? n theorem List.getElem?_set' {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) : (l.set m a)[n]? = if m = n then (fun (x : α) => a) <$> l[n]? else l[n]?
@[deprecated List.getElem?_set]
theorem List.get?_set {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) :
(l.set m a).get? n = if m = n then (fun (x : α) => a) <$> l.get? n else l.get? n theorem List.get?_set_of_lt {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : n < l.length) : (l.set m a).get? n = if m = n then some a else l.get? n theorem List.get?_set_of_lt' {α : Type u_1} (a : α) {m : Nat} {n : Nat} (l : List α) (h : m < l.length) : (l.set m a).get? n = if m = n then some a else l.get? n theorem List.drop_set_of_lt {α : Type u_1} (a : α) {n : Nat} {m : Nat} (l : List α) (h : n < m) : List.drop m (l.set n a) = theorem List.take_set_of_lt {α : Type u_1} (a : α) {n : Nat} {m : Nat} (l : List α) (h : m < n) : List.take m (l.set n a) = ### removeNth # theorem List.length_eraseIdx {α : Type u_1} {l : List α} {i : Nat} : i < l.length(l.eraseIdx i).length = l.length - 1 @[deprecated List.length_eraseIdx] theorem List.length_removeNth {α : Type u_1} {l : List α} {i : Nat} : i < l.length(l.eraseIdx i).length = l.length - 1 Alias of List.length_eraseIdx. ### tail # @[simp] theorem List.length_tail {α : Type u_1} (l : List α) : l.tail.length = l.length - 1 ### eraseP # @[simp] theorem List.eraseP_nil : ∀ {α : Type u_1} {p : αBool}, List.eraseP p [] = [] theorem List.eraseP_cons {α : Type u_1} {p : αBool} (a : α) (l : List α) : List.eraseP p (a :: l) = bif p a then l else a :: @[simp] theorem List.eraseP_cons_of_pos {α : Type u_1} {a : α} {l : List α} (p : αBool) (h : p a = true) : List.eraseP p (a :: l) = l @[simp] theorem List.eraseP_cons_of_neg {α : Type u_1} {a : α} {l : List α} (p : αBool) (h : ¬p a = true) : List.eraseP p (a :: l) = a :: theorem List.eraseP_of_forall_not {α : Type u_1} {p : αBool} {l : List α} (h : ∀ (a : α), a l¬p a = true) : = l theorem List.exists_of_eraseP {α : Type u_1} {p : αBool} {l : List α} {a : α} (al : a l) (pa : p a = true) : ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁¬p b = true) p a = true l = l₁ ++ a :: l₂ = l₁ ++ l₂ theorem List.exists_or_eq_self_of_eraseP {α : Type u_1} (p : αBool) (l : List α) : = l ∃ (a : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁¬p b = true) p a = true l = l₁ ++ a :: l₂ = l₁ ++ l₂ @[simp] theorem List.length_eraseP_of_mem : ∀ {α : Type u_1} {a : α} {l : List α} {p : αBool}, a lp a = true().length = l.length.pred theorem List.eraseP_append_left {α : Type u_1} {p : αBool} {a : α} (pa : p a = true) {l₁ : List α} (l₂ : List α) : a l₁List.eraseP p (l₁ ++ l₂) = List.eraseP p l₁ ++ l₂ theorem List.eraseP_append_right {α : Type u_1} {p : αBool} {l₁ : List α} (l₂ : List α) : (∀ (b : α), b l₁¬p b = true)List.eraseP p (l₁ ++ l₂) = l₁ ++ List.eraseP p l₂ theorem List.eraseP_sublist {α : Type u_1} {p : αBool} (l : List α) : ().Sublist l theorem List.eraseP_subset {α : Type u_1} {p : αBool} (l : List α) : l theorem List.Sublist.eraseP : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : αBool}, l₁.Sublist l₂(List.eraseP p l₁).Sublist (List.eraseP p l₂) theorem List.mem_of_mem_eraseP {α : Type u_1} {a : α} {p : αBool} {l : List α} : a a l @[simp] theorem List.mem_eraseP_of_neg {α : Type u_1} {p : αBool} {a : α} {l : List α} (pa : ¬p a = true) : a a l theorem List.eraseP_map {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) : @[simp] theorem List.extractP_eq_find?_eraseP {α : Type u_1} {p : αBool} (l : List α) : = (, ) theorem List.extractP_eq_find?_eraseP.go {α : Type u_1} {p : αBool} (l : List α) (acc : ) (xs : List α) : l = acc.data ++ xsList.extractP.go p l xs acc = (List.find? p xs, acc.data ++ List.eraseP p xs) ### erase # theorem List.erase_eq_eraseP' {α : Type u_1} [BEq α] (a : α) (l : List α) : l.erase a = List.eraseP (fun (x : α) => x == a) l theorem List.erase_eq_eraseP {α : Type u_1} [BEq α] [] (a : α) (l : List α) : l.erase a = List.eraseP (fun (x : α) => a == x) l theorem List.exists_erase_eq {α : Type u_1} [BEq α] [] {a : α} {l : List α} (h : a l) : ∃ (l₁ : List α), ∃ (l₂ : List α), ¬a l₁ l = l₁ ++ a :: l₂ l.erase a = l₁ ++ l₂ @[simp] theorem List.length_erase_of_mem {α : Type u_1} [BEq α] [] {a : α} {l : List α} (h : a l) : (l.erase a).length = l.length.pred theorem List.erase_append_left {α : Type u_1} [BEq α] {a : α} [] {l₁ : List α} (l₂ : List α) (h : a l₁) : (l₁ ++ l₂).erase a = l₁.erase a ++ l₂ theorem List.erase_append_right {α : Type u_1} [BEq α] [] {a : α} {l₁ : List α} (l₂ : List α) (h : ¬a l₁) : (l₁ ++ l₂).erase a = l₁ ++ l₂.erase a theorem List.erase_sublist {α : Type u_1} [BEq α] (a : α) (l : List α) : (l.erase a).Sublist l theorem List.erase_subset {α : Type u_1} [BEq α] (a : α) (l : List α) : l.erase a l theorem List.Sublist.erase {α : Type u_1} [BEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) : (l₁.erase a).Sublist (l₂.erase a) @[deprecated List.Sublist.erase] theorem List.sublist.erase {α : Type u_1} [BEq α] (a : α) {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) : (l₁.erase a).Sublist (l₂.erase a) Alias of List.Sublist.erase. theorem List.mem_of_mem_erase {α : Type u_1} [BEq α] {a : α} {b : α} {l : List α} (h : a l.erase b) : a l @[simp] theorem List.mem_erase_of_ne {α : Type u_1} [BEq α] [] {a : α} {b : α} {l : List α} (ab : a b) : a l.erase b a l theorem List.erase_comm {α : Type u_1} [BEq α] [] (a : α) (b : α) (l : List α) : (l.erase a).erase b = (l.erase b).erase a ### filter and partition # @[simp] theorem List.filter_sublist {α : Type u_1} {p : αBool} (l : List α) : ().Sublist l ### filterMap # theorem List.Sublist.filterMap {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} (f : α) (s : l₁.Sublist l₂) : ().Sublist () theorem List.Sublist.filter {α : Type u_1} (p : αBool) {l₁ : List α} {l₂ : List α} (s : l₁.Sublist l₂) : (List.filter p l₁).Sublist (List.filter p l₂) ### findIdx # @[simp] theorem List.findIdx_nil {α : Type u_1} (p : αBool) : theorem List.findIdx_cons {α : Type u_1} (p : αBool) (b : α) (l : List α) : List.findIdx p (b :: l) = bif p b then 0 else + 1 theorem List.findIdx_cons.findIdx_go_succ {α : Type u_1} (p : αBool) (l : List α) (n : Nat) : List.findIdx.go p l (n + 1) = + 1 theorem List.findIdx_of_get?_eq_some {α : Type u_1} {p : αBool} {y : α} {xs : List α} (w : xs.get? (List.findIdx p xs) = some y) : p y = true theorem List.findIdx_get {α : Type u_1} {p : αBool} {xs : List α} {w : List.findIdx p xs < xs.length} : p (xs.get List.findIdx p xs, w) = true theorem List.findIdx_lt_length_of_exists {α : Type u_1} {p : αBool} {xs : List α} (h : ∃ (x : α), x xs p x = true) : List.findIdx p xs < xs.length theorem List.findIdx_get?_eq_get_of_exists {α : Type u_1} {p : αBool} {xs : List α} (h : ∃ (x : α), x xs p x = true) : xs.get? (List.findIdx p xs) = some (xs.get List.findIdx p xs, ) ### findIdx? # @[simp] theorem List.findIdx?_nil {α : Type u_1} {p : αBool} {i : Nat} : List.findIdx? p [] i = none @[simp] theorem List.findIdx?_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {p : αBool} {i : Nat}, List.findIdx? p (x :: xs) i = if p x = true then some i else List.findIdx? p xs (i + 1) @[simp] theorem List.findIdx?_succ {α : Type u_1} {xs : List α} {p : αBool} {i : Nat} : List.findIdx? p xs (i + 1) = Option.map (fun (i : Nat) => i + 1) (List.findIdx? p xs i) theorem List.findIdx?_eq_some_iff {α : Type u_1} {i : Nat} (xs : List α) (p : αBool) : = some i List.map p (List.take (i + 1) xs) = theorem List.findIdx?_of_eq_some {α : Type u_1} {i : Nat} {xs : List α} {p : αBool} (w : = some i) : match xs.get? i with | some a => p a = true | none => theorem List.findIdx?_of_eq_none {α : Type u_1} {xs : List α} {p : αBool} (w : = none) (i : Nat) : match xs.get? i with | some a => ¬p a = true | none => @[simp] theorem List.findIdx?_append {α : Type u_1} {xs : List α} {ys : List α} {p : αBool} : List.findIdx? p (xs ++ ys) = HOrElse.hOrElse () fun (x : Unit) => Option.map (fun (i : Nat) => i + xs.length) () @[simp] theorem List.findIdx?_replicate {n : Nat} : ∀ {α : Type u_1} {a : α} {p : αBool}, List.findIdx? p () = if 0 < n p a = true then some 0 else none ### pairwise # theorem List.Pairwise.sublist : ∀ {α : Type u_1} {l₁ l₂ : List α} {R : ααProp}, l₁.Sublist l₂ theorem List.pairwise_map {α : Type u_1} : ∀ {α_1 : Type u_2} {f : αα_1} {R : α_1α_1Prop} {l : List α}, List.Pairwise R (List.map f l) List.Pairwise (fun (a b : α) => R (f a) (f b)) l theorem List.pairwise_append {α : Type u_1} {R : ααProp} {l₁ : List α} {l₂ : List α} : List.Pairwise R (l₁ ++ l₂) ∀ (a : α), a l₁∀ (b : α), b l₂R a b theorem List.pairwise_reverse {α : Type u_1} {R : ααProp} {l : List α} : List.Pairwise R l.reverse List.Pairwise (fun (a b : α) => R b a) l theorem List.Pairwise.imp {α : Type u_1} {R : ααProp} {S : ααProp} (H : ∀ {a b : α}, R a bS a b) {l : List α} : ### replaceF # theorem List.replaceF_nil : ∀ {α : Type u_1} {p : α}, = [] theorem List.replaceF_cons {α : Type u_1} {p : α} (a : α) (l : List α) : List.replaceF p (a :: l) = match p a with | none => a :: | some a' => a' :: l theorem List.replaceF_cons_of_some {α : Type u_1} {a' : α} {a : α} {l : List α} (p : α) (h : p a = some a') : List.replaceF p (a :: l) = a' :: l theorem List.replaceF_cons_of_none {α : Type u_1} {a : α} {l : List α} (p : α) (h : p a = none) : List.replaceF p (a :: l) = a :: theorem List.replaceF_of_forall_none {α : Type u_1} {p : α} {l : List α} (h : ∀ (a : α), a lp a = none) : = l theorem List.exists_of_replaceF {α : Type u_1} {p : α} {l : List α} {a : α} {a' : α} (al : a l) (pa : p a = some a') : ∃ (a : α), ∃ (a' : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁p b = none) p a = some a' l = l₁ ++ a :: l₂ = l₁ ++ a' :: l₂ theorem List.exists_or_eq_self_of_replaceF {α : Type u_1} (p : α) (l : List α) : = l ∃ (a : α), ∃ (a' : α), ∃ (l₁ : List α), ∃ (l₂ : List α), (∀ (b : α), b l₁p b = none) p a = some a' l = l₁ ++ a :: l₂ = l₁ ++ a' :: l₂ @[simp] theorem List.length_replaceF : ∀ {α : Type u_1} {f : α} {l : List α}, ().length = l.length ### disjoint # theorem List.disjoint_symm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂l₂.Disjoint l₁ theorem List.disjoint_comm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ l₂.Disjoint l₁ theorem List.disjoint_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ∀ ⦃a : α⦄, a l₁¬a l₂ theorem List.disjoint_right : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ∀ ⦃a : α⦄, a l₂¬a l₁ theorem List.disjoint_iff_ne : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ∀ (a : α), a l₁∀ (b : α), b l₂a b theorem List.disjoint_of_subset_left : ∀ {α : Type u_1} {l₁ l l₂ : List α}, l₁ ll.Disjoint l₂l₁.Disjoint l₂ theorem List.disjoint_of_subset_right : ∀ {α : Type u_1} {l₂ l l₁ : List α}, l₂ ll₁.Disjoint ll₁.Disjoint l₂ theorem List.disjoint_of_disjoint_cons_left : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂l₁.Disjoint l₂ theorem List.disjoint_of_disjoint_cons_right : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₁.Disjoint (a :: l₂)l₁.Disjoint l₂ @[simp] theorem List.disjoint_nil_left {α : Type u_1} (l : List α) : [].Disjoint l @[simp] theorem List.disjoint_nil_right {α : Type u_1} (l : List α) : l.Disjoint [] @[simp] theorem List.singleton_disjoint : ∀ {α : Type u_1} {a : α} {l : List α}, [a].Disjoint l ¬a l @[simp] theorem List.disjoint_singleton : ∀ {α : Type u_1} {l : List α} {a : α}, l.Disjoint [a] ¬a l @[simp] theorem List.disjoint_append_left : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l l₁.Disjoint l l₂.Disjoint l @[simp] theorem List.disjoint_append_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) l.Disjoint l₁ l.Disjoint l₂ @[simp] theorem List.disjoint_cons_left : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, (a :: l₁).Disjoint l₂ ¬a l₂ l₁.Disjoint l₂ @[simp] theorem List.disjoint_cons_right : ∀ {α : Type u_1} {l₁ : List α} {a : α} {l₂ : List α}, l₁.Disjoint (a :: l₂) ¬a l₁ l₁.Disjoint l₂ theorem List.disjoint_of_disjoint_append_left_left : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint ll₁.Disjoint l theorem List.disjoint_of_disjoint_append_left_right : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint ll₂.Disjoint l theorem List.disjoint_of_disjoint_append_right_left : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂)l.Disjoint l₁ theorem List.disjoint_of_disjoint_append_right_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂)l.Disjoint l₂ ### foldl / foldr # theorem List.foldl_hom {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁α₂) (g₁ : α₁βα₁) (g₂ : α₂βα₂) (l : List β) (init : α₁) (H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) : List.foldl g₂ (f init) l = f (List.foldl g₁ init l) theorem List.foldr_hom {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁β₂) (g₁ : αβ₁β₁) (g₂ : αβ₂β₂) (l : List α) (init : β₁) (H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) : List.foldr g₂ (f init) l = f (List.foldr g₁ init l) ### union # theorem List.union_def {α : Type u_1} [BEq α] (l₁ : List α) (l₂ : List α) : l₁ l₂ = List.foldr List.insert l₂ l₁ @[simp] theorem List.nil_union {α : Type u_1} [BEq α] (l : List α) : [] l = l @[simp] theorem List.cons_union {α : Type u_1} [BEq α] (a : α) (l₁ : List α) (l₂ : List α) : a :: l₁ l₂ = List.insert a (l₁ l₂) @[simp] theorem List.mem_union_iff {α : Type u_1} [BEq α] [] {x : α} {l₁ : List α} {l₂ : List α} : x l₁ l₂ x l₁ x l₂ ### inter # theorem List.inter_def {α : Type u_1} [BEq α] (l₁ : List α) (l₂ : List α) : l₁ l₂ = List.filter (fun (x : α) => List.elem x l₂) l₁ @[simp] theorem List.mem_inter_iff {α : Type u_1} [BEq α] [] {x : α} {l₁ : List α} {l₂ : List α} : x l₁ l₂ x l₁ x l₂ ### product # @[simp] theorem List.pair_mem_product {α : Type u_1} {β : Type u_2} {xs : List α} {ys : List β} {x : α} {y : β} : (x, y) xs.product ys x xs y ys List.prod satisfies a specification of cartesian product on lists. ### leftpad # @[simp] theorem List.leftpad_length {α : Type u_1} (n : Nat) (a : α) (l : List α) : (List.leftpad n a l).length = max n l.length The length of the List returned by List.leftpad n a l is equal to the larger of n and l.length theorem List.leftpad_prefix {α : Type u_1} (n : Nat) (a : α) (l : List α) : List.replicate (n - l.length) a <+: List.leftpad n a l theorem List.leftpad_suffix {α : Type u_1} (n : Nat) (a : α) (l : List α) : ### monadic operations # @[simp] theorem List.forIn_eq_forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] : List.forIn = forIn theorem List.forIn_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] [] (f : αβm ()) (l : List α) (init : β) : forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
@[simp]
theorem List.forM_append {m : Type u_1 → Type u_2} {α : Type u_3} [] [] (l₁ : List α) (l₂ : List α) (f : α) :
(l₁ ++ l₂).forM f = do l₁.forM f l₂.forM f

### diff #

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

### prefix, suffix, infix #

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

### drop #

theorem List.mem_of_mem_drop {α : Type u_1} {a : α} {n : Nat} {l : List α} (h : a ) :
a l
theorem List.disjoint_take_drop {α : Type u_1} {m : Nat} {n : Nat} {l : List α} :
l.Nodupm n().Disjoint ()

### Chain #

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

### range', range #

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

### enum, enumFrom #

@[simp]
theorem List.enumFrom_map_fst {α : Type u_1} (n : Nat) (l : List α) :
List.map Prod.fst () = List.range' n l.length
@[simp]
theorem List.enum_map_fst {α : Type u_1} (l : List α) :
List.map Prod.fst l.enum = List.range l.length

### indexOf and indexesOf #

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