### toArray #

source
@[deprecated List.getElem_toArray (since := "2025-09-11")]
theorem List.getElem_mk {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.length) :
{ toList := xs }[i] = xs[i]

### next? #

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

### dropLast #

source
theorem List.dropLast_eq_eraseIdx {α : Type u_1} {xs : List α} {i : Nat} (last_idx : i + 1 = xs.length) :
xs.dropLast = xs.eraseIdx i

### set #

source
theorem List.set_eq_modify {α : Type u_1} (a : α) (n : Nat) (l : List α) :
l.set n a = l.modify n fun (x : α) => a
source
theorem List.set_eq_take_cons_drop {α : Type u_1} (a : α) {n : Nat} {l : List α} (h : n < l.length) :
l.set n a = take n l ++ a :: drop (n + 1) l
source
theorem List.modify_eq_set_getElem? {α : Type u_1} (f : α → α) (n : Nat) (l : List α) :
l.modify n f = ((fun (a : α) => l.set n (f a)) <$> l[n]?).getD l
source
@[deprecated List.modify_eq_set_getElem? (since := "2025-02-15")]
theorem List.modify_eq_set_get? {α : Type u_1} (f : α → α) (n : Nat) (l : List α) :
l.modify n f = ((fun (a : α) => l.set n (f a)) <$> l[n]?).getD l

Alias of `List.modify_eq_set_getElem?`.

source
theorem List.modify_eq_set_get {α : Type u_1} (f : α → α) {n : Nat} {l : List α} (h : n < l.length) :
l.modify n f = l.set n (f (l.get ⟨n, h⟩))
source
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
source
theorem List.getElem?_set_of_lt {α : Type u_1} (a : α) {m n : Nat} (l : List α) (h : n < l.length) :
(l.set m a)[n]? = if m = n then some a else l[n]?
source
@[deprecated List.getElem?_set_of_lt (since := "2025-02-15")]
theorem List.get?_set_of_lt {α : Type u_1} (a : α) {m n : Nat} (l : List α) (h : n < l.length) :
(l.set m a)[n]? = if m = n then some a else l[n]?

Alias of `List.getElem?_set_of_lt`.

source
theorem List.getElem?_set_of_lt' {α : Type u_1} (a : α) {m n : Nat} (l : List α) (h : m < l.length) :
(l.set m a)[n]? = if m = n then some a else l[n]?
source
@[deprecated List.getElem?_set_of_lt' (since := "2025-02-15")]
theorem List.get?_set_of_lt' {α : Type u_1} (a : α) {m n : Nat} (l : List α) (h : m < l.length) :
(l.set m a)[n]? = if m = n then some a else l[n]?

Alias of `List.getElem?_set_of_lt'`.

### tail #

source
theorem List.length_tail_add_one {α : Type u_1} (l : List α) (h : 0 < l.length) :
l.tail.length + 1 = l.length

### eraseP #

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

### erase #

source
theorem List.erase_eq_self_iff_forall_bne {α : Type u_1} [BEq α] (a : α) (xs : List α) :
xs.erase a = xs ↔ ∀ (x : α), x ∈ xs → ¬(x == a) = true

### findIdx? #

source
theorem List.findIdx_eq_findIdx? {α : Type u_1} (p : α → Bool) (l : List α) :
findIdx p l = match findIdx? p l with | some i => i | none => l.length

### replaceF #

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

### disjoint #

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

### union #

source
theorem List.union_def {α : Type u_1} [BEq α] (l₁ l₂ : List α) :
l₁ ∪ l₂ = foldr List.insert l₂ l₁
source
@[simp]
theorem List.nil_union {α : Type u_1} [BEq α] (l : List α) :
[] ∪ l = l
source
@[simp]
theorem List.cons_union {α : Type u_1} [BEq α] (a : α) (l₁ l₂ : List α) :
a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂)
source
@[simp]
theorem List.mem_union_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α} :
x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂

### inter #

source
theorem List.inter_def {α : Type u_1} [BEq α] (l₁ l₂ : List α) :
l₁ ∩ l₂ = filter (fun (x : α) => elem x l₂) l₁
source
@[simp]
theorem List.mem_inter_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α} :
x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂

### product #

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

### monadic operations #

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

### diff #

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

### drop #

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

### Pairwise #

source
theorem List.Pairwise.isChain {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} (p : Pairwise R l) :
IsChain R l
source
theorem List.pairwise_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} :
Pairwise R (a :: b :: l) ↔ R a b ∧ Pairwise R (a :: l) ∧ Pairwise R (b :: l)

### IsChain #

source
@[deprecated List.isChain_cons_cons (since := "2025-09-19")]
theorem List.chain_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} :
IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)

Alias of `List.isChain_cons_cons`.

source
theorem List.rel_of_isChain_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} (p : IsChain R (a :: b :: l)) :
R a b
source
@[deprecated List.rel_of_isChain_cons_cons (since := "2025-09-19")]
theorem List.rel_of_chain_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} (p : IsChain R (a :: b :: l)) :
R a b

Alias of `List.rel_of_isChain_cons_cons`.

source
theorem List.isChain_cons_of_isChain_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} (p : IsChain R (a :: b :: l)) :
IsChain R (b :: l)
source
@[deprecated List.isChain_cons_of_isChain_cons_cons (since := "2025-09-19")]
theorem List.chain_of_chain_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} (p : IsChain R (a :: b :: l)) :
IsChain R (b :: l)

Alias of `List.isChain_cons_of_isChain_cons_cons`.

source
theorem List.isChain_of_isChain_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {b : α✝} {l : List α✝} (p : IsChain R (b :: l)) :
IsChain R l
source
theorem List.isChain_of_isChain_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} (p : IsChain R (a :: b :: l)) :
IsChain R l
source
theorem List.IsChain.imp {α : Type u_1} {R S : α → α → Prop} {l : List α} (H : ∀ ⦃a b : α⦄, R a b → S a b) (p : IsChain R l) :
IsChain S l
source
@[deprecated List.IsChain.imp (since := "2025-09-19")]
theorem List.Chain.imp {α : Type u_1} {R S : α → α → Prop} {l : List α} (H : ∀ ⦃a b : α⦄, R a b → S a b) (p : IsChain R l) :
IsChain S l

Alias of `List.IsChain.imp`.

source
theorem List.IsChain.cons_of_imp_of_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a : α✝} {l : List α✝} {b : α✝} (h : ∀ (c : α✝), R a c → R b c) :
IsChain R (a :: l) → IsChain R (b :: l)
source
@[deprecated "Use IsChain.imp and IsChain.change_head" (since := "2025-09-19")]
theorem List.Chain.imp' {α : Type u_1} {R S : α → α → Prop} {a : α} {l : List α} {b : α} (HRS : ∀ ⦃a b : α⦄, R a b → S a b) (Hab : ∀ ⦃c : α⦄, R a c → S b c) :
IsChain R (a :: l) → IsChain S (b :: l)
source
@[deprecated List.Pairwise.isChain (since := "2025-09-19")]
theorem List.Pairwise.chain {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} (p : Pairwise R l) :
IsChain R l

Alias of `List.Pairwise.isChain`.

source
theorem List.IsChain.pairwise {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} [Trans R R R] (c : IsChain R l) :
Pairwise R l
source
theorem List.isChain_iff_pairwise {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} [Trans R R R] :
IsChain R l ↔ Pairwise R l
source
theorem List.isChain_iff_getElem {α : Type u_1} {R : α → α → Prop} {l : List α} :
IsChain R l ↔ ∀ (i : Nat) (_hi : i + 1 < l.length), R l[i] l[i + 1]
source
theorem List.IsChain.getElem {α : Type u_1} {R : α → α → Prop} {l : List α} (c : IsChain R l) (i : Nat) (hi : i + 1 < l.length) :
R l[i] l[i + 1]

### range', range #

source
theorem List.isChain_range' (s n step : Nat) :
IsChain (fun (a b : Nat) => b = a + step) (range' s n step)
source
@[deprecated List.isChain_range' (since := "2025-09-19")]
theorem List.chain_succ_range' (s n step : Nat) :
IsChain (fun (a b : Nat) => b = a + step) (s :: range' (s + step) n step)
source
theorem List.isChain_lt_range' {step : Nat} (s n : Nat) (h : 0 < step) :
IsChain (fun (x1 x2 : Nat) => x1 < x2) (range' s n step)
source
@[deprecated List.isChain_lt_range' (since := "2025-09-19")]
theorem List.chain_lt_range' {step : Nat} (s n : Nat) (h : 0 < step) :
IsChain (fun (x1 x2 : Nat) => x1 < x2) (s :: range' (s + step) n step)

### idxOf and idxsOf #

source
theorem List.foldrIdx_start {α : Type u_1} {xs : List α} {α✝ : Sort u_2} {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat} :
foldrIdx f i xs s = foldrIdx (fun (i : Nat) => f (i + s)) i xs
source
@[simp]
theorem List.foldrIdx_cons {α : Type u_1} {x : α} {xs : List α} {α✝ : Sort u_2} {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat} :
foldrIdx f i (x :: xs) s = f s x (foldrIdx f i xs (s + 1))
source
theorem List.findIdxs_cons_aux {α : Type u_1} {xs : List α} {s : Nat} (p : α → Bool) :
foldrIdx (fun (i : Nat) (a : α) (is : List Nat) => if p a = true then (i + 1) :: is else is) [] xs s = map (fun (x : Nat) => x + 1) (foldrIdx (fun (i : Nat) (a : α) (is : List Nat) => if p a = true then i :: is else is) [] xs s)
source
theorem List.findIdxs_cons {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} :
findIdxs p (x :: xs) = bif p x then 0 :: map (fun (x : Nat) => x + 1) (findIdxs p xs) else map (fun (x : Nat) => x + 1) (findIdxs p xs)
source
@[simp]
theorem List.idxsOf_nil {α : Type u_1} {x : α} [BEq α] :
idxsOf x [] = []
source
theorem List.idxsOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] :
idxsOf y (x :: xs) = bif x == y then 0 :: map (fun (x : Nat) => x + 1) (idxsOf y xs) else map (fun (x : Nat) => x + 1) (idxsOf y xs)
source
@[simp]
theorem List.eraseIdx_idxOf_eq_erase {α : Type u_1} [BEq α] (a : α) (l : List α) :
l.eraseIdx (idxOf a l) = l.erase a
source
theorem List.idxOf_mem_idxsOf {α : Type u_1} {x : α} [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) :
idxOf x xs ∈ idxsOf x xs
source
theorem List.idxOf_eq_idxOf? {α : Type u_1} [BEq α] (a : α) (l : List α) :
idxOf a l = match idxOf? a l with | some i => i | none => l.length

### insertP #

source
theorem List.insertP_loop {α : Type u_1} {p : α → Bool} (a : α) (l r : List α) :
insertP.loop p a l r = r.reverseAux (insertP p a l)
source
@[simp]
theorem List.insertP_nil {α : Type u_1} (p : α → Bool) (a : α) :
insertP p a [] = [a]
source
@[simp]
theorem List.insertP_cons_pos {α : Type u_1} (p : α → Bool) (a b : α) (l : List α) (h : p b = true) :
insertP p a (b :: l) = a :: b :: l
source
@[simp]
theorem List.insertP_cons_neg {α : Type u_1} (p : α → Bool) (a b : α) (l : List α) (h : ¬p b = true) :
insertP p a (b :: l) = b :: insertP p a l
source
@[simp]
theorem List.length_insertP {α : Type u_1} (p : α → Bool) (a : α) (l : List α) :
(insertP p a l).length = l.length + 1
source
@[simp]
theorem List.mem_insertP {α : Type u_1} (p : α → Bool) (a : α) (l : List α) :
a ∈ insertP p a l

### dropPrefix?, dropSuffix?, dropInfix? #

source
@[simp]
theorem List.dropPrefix?_nil {α : Type u_1} [BEq α] {p : List α} :
p.dropPrefix? [] = some p
source
@[irreducible]
theorem List.dropPrefix?_eq_some_iff {α : Type u_1} [BEq α] {l p s : List α} :
l.dropPrefix? p = some s ↔ ∃ (p' : List α), l = p' ++ s ∧ (p' == p) = true
source
theorem List.dropPrefix?_append_of_beq {α : Type u_1} [BEq α] {l₁ l₂ : List α} (p : List α) (h : (l₁ == l₂) = true) :
(l₁ ++ p).dropPrefix? l₂ = some p
source
theorem List.dropSuffix?_eq_some_iff {α : Type u_1} [BEq α] {l p s : List α} :
l.dropSuffix? s = some p ↔ ∃ (s' : List α), l = p ++ s' ∧ (s' == s) = true
source
@[simp]
theorem List.dropSuffix?_nil {α : Type u_1} [BEq α] {s : List α} :
s.dropSuffix? [] = some s
source
@[irreducible]
theorem List.dropInfix?_go_eq_some_iff {α : Type u_1} [BEq α] {i l acc p s : List α} :
dropInfix?.go i l acc = some (p, s) ↔ ∃ (p' : List α), p = acc.reverse ++ p' ∧ (∃ (i' : List α), l = p' ++ i' ++ s ∧ (i' == i) = true) ∧ ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length
source
theorem List.dropInfix?_eq_some_iff {α : Type u_1} [BEq α] {l i p s : List α} :
l.dropInfix? i = some (p, s) ↔ (∃ (i' : List α), l = p ++ i' ++ s ∧ (i' == i) = true) ∧ ∀ (p' i' s' : List α), l = p' ++ i' ++ s' → (i' == i) = true → p'.length ≥ p.length
source
@[simp]
theorem List.dropInfix?_nil {α : Type u_1} [BEq α] {s : List α} :
s.dropInfix? [] = some ([], s)

### IsPrefixOf?, IsSuffixOf? #

source
@[simp]
theorem List.isSome_isPrefixOf?_eq_isPrefixOf {α : Type u_1} [BEq α] (xs ys : List α) :
(xs.isPrefixOf? ys).isSome = xs.isPrefixOf ys
source
@[simp]
theorem List.isPrefixOf?_eq_some_iff_append_eq {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys zs : List α} :
xs.isPrefixOf? ys = some zs ↔ xs ++ zs = ys
source
theorem List.append_eq_of_isPrefixOf?_eq_some {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys zs : List α} (h : xs.isPrefixOf? ys = some zs) :
xs ++ zs = ys
source
@[simp]
theorem List.isSome_isSuffixOf?_eq_isSuffixOf {α : Type u_1} [BEq α] (xs ys : List α) :
(xs.isSuffixOf? ys).isSome = xs.isSuffixOf ys
source
@[simp]
theorem List.isSuffixOf?_eq_some_iff_append_eq {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys zs : List α} :
xs.isSuffixOf? ys = some zs ↔ zs ++ xs = ys
source
theorem List.append_eq_of_isSuffixOf?_eq_some {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys zs : List α} (h : xs.isSuffixOf? ys = some zs) :
zs ++ xs = ys

### sum/prod #

source
theorem List.foldr_eq_foldl {α : Type u_1} (f : α → α → α) (init : α) [Std.Associative f] [Std.LawfulIdentity f init] {l : List α} :
foldr f init l = foldl f init l
source
@[simp]
theorem List.prod_nil {α : Type u_1} [Mul α] [One α] :
[].prod = 1
source
@[simp]
theorem List.prod_cons {α : Type u_1} [Mul α] [One α] {a : α} {l : List α} :
(a :: l).prod = a * l.prod
source
theorem List.prod_one_cons {α : Type u_1} [Mul α] [One α] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} :
(1 :: l).prod = l.prod
source
theorem List.prod_singleton {α : Type u_1} [Mul α] [One α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 * x2) 1] {a : α} :
[a].prod = a
source
theorem List.prod_pair {α : Type u_1} [Mul α] [One α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 * x2) 1] {a b : α} :
[a, b].prod = a * b
source
@[simp]
theorem List.prod_append {α : Type u_1} [Mul α] [One α] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 * x2) 1] [Std.Associative fun (x1 x2 : α) => x1 * x2] {l₁ l₂ : List α} :
(l₁ ++ l₂).prod = l₁.prod * l₂.prod
source
theorem List.prod_concat {α : Type u_1} [Mul α] [One α] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] [Std.Associative fun (x1 x2 : α) => x1 * x2] {l : List α} {a : α} :
(l.concat a).prod = l.prod * a
source
@[simp]
theorem List.prod_flatten {α : Type u_1} [Mul α] [One α] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] [Std.Associative fun (x1 x2 : α) => x1 * x2] {l : List (List α)} :
l.flatten.prod = (map prod l).prod
source
theorem List.prod_eq_foldr {α : Type u_1} [Mul α] [One α] {l : List α} :
l.prod = foldr (fun (x1 x2 : α) => x1 * x2) 1 l
source
theorem List.prod_eq_foldl {α : Type u_1} [Mul α] [One α] [Std.Associative fun (x1 x2 : α) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 * x2) 1] {l : List α} :
l.prod = foldl (fun (x1 x2 : α) => x1 * x2) 1 l
source
theorem List.sum_zero_cons {α : Type u_1} [Add α] [Zero α] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} :
(0 :: l).sum = l.sum
source
theorem List.sum_singleton {α : Type u_1} [Add α] [Zero α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 + x2) 0] {a : α} :
[a].sum = a
source
theorem List.sum_pair {α : Type u_1} [Add α] [Zero α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 + x2) 0] {a b : α} :
[a, b].sum = a + b
source
@[simp]
theorem List.sum_append {α : Type u_1} [Add α] [Zero α] [Std.LawfulLeftIdentity (fun (x1 x2 : α) => x1 + x2) 0] [Std.Associative fun (x1 x2 : α) => x1 + x2] {l₁ l₂ : List α} :
(l₁ ++ l₂).sum = l₁.sum + l₂.sum
source
theorem List.sum_concat {α : Type u_1} [Add α] [Zero α] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] [Std.Associative fun (x1 x2 : α) => x1 + x2] {l : List α} {a : α} :
(l.concat a).sum = l.sum + a
source
@[simp]
theorem List.sum_flatten {α : Type u_1} [Add α] [Zero α] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] [Std.Associative fun (x1 x2 : α) => x1 + x2] {l : List (List α)} :
l.flatten.sum = (map sum l).sum
source
theorem List.sum_eq_foldr {α : Type u_1} [Add α] [Zero α] {l : List α} :
l.sum = foldr (fun (x1 x2 : α) => x1 + x2) 0 l
source
theorem List.sum_eq_foldl {α : Type u_1} [Add α] [Zero α] [Std.Associative fun (x1 x2 : α) => x1 + x2] [Std.LawfulIdentity (fun (x1 x2 : α) => x1 + x2) 0] {l : List α} :
l.sum = foldl (fun (x1 x2 : α) => x1 + x2) 0 l