instance List.instNeZeroNatLengthCons {α : Type u_1} {a : α} {l : List α} : NeZero (a :: l).length

count

theorem List.count_getElem_take_succ {α : Type u_1} [BEq α] [EquivBEq α] {xs : List α} {i : Nat} {hi : i < xs.length} : count xs[i] (take (i + 1) xs) = count xs[i] (take i xs) + 1

theorem List.count_getElem_take_lt_count {α : Type u_1} [BEq α] [EquivBEq α] {xs : List α} {i : Nat} {hi : i < xs.length} : count xs[i] (take i xs) < count xs[i] xs

zip

zipIdx

toArray

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

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

dropLast

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

set

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

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

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

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

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

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

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]?

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

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]?

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

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

eraseP

@[simp]

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

erase

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?

@[deprecated List.findIdx_eq_getD_findIdx? (since := "2025-11-06")]

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

theorem List.replaceF_nil {α✝ : Type u_1} {p : α✝ → Option α✝} : replaceF p [] = []

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

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

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

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

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₂

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₂

@[simp]

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

disjoint

theorem List.disjoint_symm {α✝ : Type u_1} {l₁ l₂ : List α✝} (d : 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 α✝} (ss : l₁ ⊆ l) (d : l.Disjoint l₂) : l₁.Disjoint l₂

theorem List.disjoint_of_subset_right {α✝ : Type u_1} {l₂ l l₁ : List α✝} (ss : l₂ ⊆ l) (d : l₁.Disjoint l) : l₁.Disjoint l₂

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.disjoint_of_disjoint_append_left_left {α✝ : Type u_1} {l₁ l₂ l : List α✝} (d : (l₁ ++ l₂).Disjoint l) : l₁.Disjoint l

theorem List.disjoint_of_disjoint_append_left_right {α✝ : Type u_1} {l₁ l₂ l : List α✝} (d : (l₁ ++ l₂).Disjoint l) : l₂.Disjoint l

theorem List.disjoint_of_disjoint_append_right_left {α✝ : Type u_1} {l l₁ l₂ : List α✝} (d : l.Disjoint (l₁ ++ l₂)) : l.Disjoint l₁

theorem List.disjoint_of_disjoint_append_right_right {α✝ : Type u_1} {l l₁ l₂ : List α✝} (d : l.Disjoint (l₁ ++ l₂)) : l.Disjoint l₂

union

theorem List.union_def {α : Type u_1} [BEq α] (l₁ l₂ : List α) : l₁ ∪ l₂ = 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₁ l₂ : List α) : a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂)

@[simp]

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

inter

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

@[simp]

theorem List.mem_inter_iff {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {l₁ 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.

monadic operations

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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

drop

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

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)

theorem List.Pairwise.isChain {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} (p : Pairwise R l) : IsChain R l

IsChain

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

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

theorem List.IsChain.rel {α✝ : 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.

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

theorem List.isChain_of_isChain_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {b : α✝} {l : List α✝} (p : IsChain R (b :: l)) : IsChain R l

theorem List.IsChain.of_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {b : α✝} {l : List α✝} (p : IsChain R (b :: l)) : IsChain R l

Alias of List.isChain_of_isChain_cons.

@[deprecated List.IsChain.of_cons (since := "2026-02-10")]

theorem List.isChain_cons_of_isChain_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} : IsChain R (a :: b :: l) → IsChain R (b :: l)

@[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 α✝} : IsChain R (a :: b :: l) → IsChain R (b :: l)

Alias of List.isChain_cons_of_isChain_cons_cons.

@[deprecated List.IsChain.of_cons (since := "2026-02-10")]

theorem List.isChain_of_isChain_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} : IsChain R (a :: b :: l) → IsChain R l

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

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

theorem List.IsChain.cons_of_imp {α✝ : 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)

@[deprecated List.IsChain.cons_of_imp (since := "2026-02-10")]

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)

Alias of List.IsChain.cons_of_imp.

theorem List.IsChain.cons_of_imp_of_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) (h : IsChain R (a :: l)) : IsChain S (b :: l)

@[deprecated List.IsChain.cons_of_imp_of_imp (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) (h : IsChain R (a :: l)) : IsChain S (b :: l)

Alias of List.IsChain.cons_of_imp_of_imp.

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

theorem List.isChain_iff_pairwise {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} [Trans R R R] : IsChain R l ↔ Pairwise R l

theorem List.IsChain.pairwise {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} [Trans R R R] (c : IsChain R l) : Pairwise R l

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]

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

theorem List.isChain_range' (s n step : Nat) : IsChain (fun (a b : Nat) => b = a + step) (range' s n step)

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

theorem List.isChain_lt_range' {step : Nat} (s n : Nat) (h : 0 < step) : IsChain (fun (x1 x2 : Nat) => x1 < x2) (range' s n step)

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

foldrIdx

@[simp]

theorem List.foldrIdx_nil {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat} : foldrIdx f i [] s = i

@[simp]

theorem List.foldrIdx_cons {α : Type u_1} {x : α} {xs : List α} {α✝ : Type u_2} {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat} : foldrIdx f i (x :: xs) s = f s x (foldrIdx f i xs (s + 1))

theorem List.foldrIdx_start {α : Type u_1} {xs : List α} {α✝ : Type u_2} {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat} : foldrIdx f i xs s = foldrIdx (fun (x : Nat) => f (x + s)) i xs

theorem List.foldrIdx_const {α : Type u_1} {xs : List α} {α✝ : Type u_2} {f : α → α✝ → α✝} {i : α✝} {s : Nat} : foldrIdx (Function.const Nat f) i xs s = foldr f i xs

theorem List.foldrIdx_eq_foldr_zipIdx {α : Type u_1} {xs : List α} {α✝ : Type u_2} {f : Nat → α → α✝ → α✝} {i : α✝} {s : Nat} : foldrIdx f i xs s = foldr (fun (ab : α × Nat) => f ab.snd ab.fst) i (xs.zipIdx s)

foldlIdx

@[simp]

theorem List.foldlIdx_nil {α : Type u_1} {α✝ : Sort u_2} {f : Nat → α✝ → α → α✝} {i : α✝} {s : Nat} : foldlIdx f i [] s = i

@[simp]

theorem List.foldlIdx_cons {α : Type u_1} {x : α} {xs : List α} {α✝ : Sort u_2} {f : Nat → α✝ → α → α✝} {i : α✝} {s : Nat} : foldlIdx f i (x :: xs) s = foldlIdx f (f s i x) xs (s + 1)

theorem List.foldlIdx_start {α : Type u_1} {xs : List α} {α✝ : Sort u_2} {f : Nat → α✝ → α → α✝} {i : α✝} {s : Nat} : foldlIdx f i xs s = foldlIdx (fun (x : Nat) => f (x + s)) i xs

theorem List.foldlIdx_const {α : Type u_1} {xs : List α} {α✝ : Type u_2} {f : α✝ → α → α✝} {i : α✝} {s : Nat} : foldlIdx (Function.const Nat f) i xs s = foldl f i xs

theorem List.foldlIdx_eq_foldl_zipIdx {α : Type u_1} {xs : List α} {α✝ : Type u_2} {f : Nat → α✝ → α → α✝} {i : α✝} {s : Nat} : foldlIdx f i xs s = foldl (fun (b : α✝) (ab : α × Nat) => f ab.snd b ab.fst) i (xs.zipIdx s)

findIdxs

@[simp]

theorem List.findIdxs_nil {α : Type u_1} {p : α → Bool} {s : Nat} : findIdxs p [] s = []

@[simp]

theorem List.findIdxs_cons {α : Type u_1} {x : α} {xs : List α} {p : α → Bool} {s : Nat} : findIdxs p (x :: xs) s = if p x = true then s :: findIdxs p xs (s + 1) else findIdxs p xs (s + 1)

theorem List.findIdxs_singleton {α✝ : Type u_1} {x : α✝} {p : α✝ → Bool} {s : Nat} : findIdxs p [x] s = if p x = true then [s] else []

theorem List.findIdxs_start {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : findIdxs p xs s = map (fun (x : Nat) => x + s) (findIdxs p xs)

theorem List.findIdxs_eq_filterMap_zipIdx {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : findIdxs p xs s = filterMap (fun (ab : α × Nat) => bif p ab.fst then some ab.snd else none) (xs.zipIdx s)

@[simp]

theorem List.mem_findIdxs_iff_getElem_sub_pos {α : Type u_1} {xs : List α} {p : α → Bool} {s i : Nat} : i ∈ findIdxs p xs s ↔ s ≤ i ∧ ∃ (hix : i - s < xs.length), p xs[i - s] = true

theorem List.mem_findIdxs_iff_exists_getElem_pos {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} : i ∈ findIdxs p xs ↔ ∃ (hix : i < xs.length), p xs[i] = true

theorem List.mem_findIdxs_iff_pos_getElem {i : Nat} {α : Type u_1} {xs : List α} {p : α → Bool} (hi : i < xs.length) : i ∈ findIdxs p xs ↔ p xs[i] = true

theorem List.ge_of_mem_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} (y : Nat) : y ∈ findIdxs p xs s → s ≤ y

theorem List.lt_add_of_mem_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} (y : Nat) : y ∈ findIdxs p xs s → y < xs.length + s

theorem List.findIdxs_eq_nil_iff {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : findIdxs p xs s = [] ↔ ∀ (x : α), x ∈ xs → p x = false

@[simp]

theorem List.length_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : (findIdxs p xs s).length = countP p xs

@[simp]

theorem List.pairwise_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : Pairwise (fun (x1 x2 : Nat) => x1 < x2) (findIdxs p xs s)

@[simp]

theorem List.isChain_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : IsChain (fun (x1 x2 : Nat) => x1 < x2) (findIdxs p xs s)

@[simp]

theorem List.nodup_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : (findIdxs p xs s).Nodup

@[simp]

theorem List.findIdxs_map {α : Type u_1} {xs : List α} {α✝ : Type u_2} {f : α → α✝} {p : α✝ → Bool} {s : Nat} : findIdxs p (map f xs) s = findIdxs (p ∘ f) xs s

@[simp]

theorem List.findIdxs_append {α : Type u_1} {xs ys : List α} {p : α → Bool} {s : Nat} : findIdxs p (xs ++ ys) s = findIdxs p xs s ++ findIdxs p ys (s + xs.length)

@[simp]

theorem List.findIdxs_take {α : Type u_1} {xs : List α} {n : Nat} {p : α → Bool} {s : Nat} : findIdxs p (take n xs) s = take (countP p (take n xs)) (findIdxs p xs s)

@[simp]

theorem List.le_getElem_findIdxs {i : Nat} {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} (h : i < (findIdxs p xs s).length) : s ≤ (findIdxs p xs s)[i]

@[simp]

theorem List.getElem_findIdxs_lt {i : Nat} {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} (h : i < (findIdxs p xs s).length) : (findIdxs p xs s)[i] < xs.length + s

theorem List.getElem_filter_eq_getElem_getElem_findIdxs_sub {i : Nat} {α : Type u_1} {xs : List α} {p : α → Bool} (s : Nat) (h : i < (filter p xs).length) : (filter p xs)[i] = xs[(findIdxs p xs s)[i] - s]

theorem List.getElem_filter_eq_getElem_getElem_findIdxs {i : Nat} {α : Type u_1} {xs : List α} {p : α → Bool} (h : i < (filter p xs).length) : (filter p xs)[i] = xs[(findIdxs p xs)[i]]

theorem List.getElem_getElem_findIdxs_sub {i : Nat} {α : Type u_1} {xs : List α} {p : α → Bool} (s : Nat) (h : i < (findIdxs p xs s).length) : p xs[(findIdxs p xs s)[i] - s] = true

theorem List.getElem_getElem_findIdxs {i : Nat} {α : Type u_1} {xs : List α} {p : α → Bool} (h : i < (findIdxs p xs).length) : p xs[(findIdxs p xs)[i]] = true

theorem List.getElem_zero_findIdxs_eq_findIdx_add {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} (h : 0 < (findIdxs p xs s).length) : (findIdxs p xs s)[0] = findIdx p xs + s

@[simp]

theorem List.getElem_zero_findIdxs_eq_findIdx {α : Type u_1} {xs : List α} {p : α → Bool} (h : 0 < (findIdxs p xs).length) : (findIdxs p xs)[0] = findIdx p xs

theorem List.findIdx_add_mem_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} (s : Nat) (h : findIdx p xs < xs.length) : findIdx p xs + s ∈ findIdxs p xs s

theorem List.findIdx_mem_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} (h : findIdx p xs < xs.length) : findIdx p xs ∈ findIdxs p xs

findIdxsValues

theorem List.findIdxsValues_eq_zip_filter_findIdxs {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : findIdxsValues p xs s = (findIdxs p xs s).zip (filter p xs)

@[simp]

theorem List.unzip_findIdxsValues {α : Type u_1} {xs : List α} {p : α → Bool} {s : Nat} : (findIdxsValues p xs s).unzip = (findIdxs p xs s, filter p xs)

findIdxNth

@[simp]

theorem List.findIdxNth_nil {α : Type u_1} {p : α → Bool} {n : Nat} : findIdxNth p [] n = 0

theorem List.findIdxNth_cons {α : Type u_1} {xs : List α} {p : α → Bool} {n : Nat} {a : α} : findIdxNth p (a :: xs) n = if n = 0 then if p a = true then 0 else findIdxNth p xs 0 + 1 else if p a = true then findIdxNth p xs (n - 1) + 1 else findIdxNth p xs n + 1

@[simp]

theorem List.findIdxNth_cons_zero {α : Type u_1} {xs : List α} {p : α → Bool} {a : α} : findIdxNth p (a :: xs) 0 = if p a = true then 0 else findIdxNth p xs 0 + 1

@[simp]

theorem List.findIdxNth_cons_succ {α : Type u_1} {xs : List α} {p : α → Bool} {n : Nat} {a : α} : findIdxNth p (a :: xs) (n + 1) = if p a = true then findIdxNth p xs n + 1 else findIdxNth p xs (n + 1) + 1

theorem List.findIdxNth_cons_of_neg {α : Type u_1} {p : α → Bool} {xs : List α} {n : Nat} {a : α} (h : p a = false) : findIdxNth p (a :: xs) n = findIdxNth p xs n + 1

theorem List.findIdxNth_cons_of_pos {α : Type u_1} {p : α → Bool} {xs : List α} {n : Nat} {a : α} (h : p a = true) : findIdxNth p (a :: xs) n = if n = 0 then 0 else findIdxNth p xs (n - 1) + 1

theorem List.findIdxNth_cons_zero_of_pos {α : Type u_1} {p : α → Bool} {xs : List α} {a : α} (h : p a = true) : findIdxNth p (a :: xs) 0 = 0

theorem List.findIdxNth_cons_succ_of_pos {α : Type u_1} {p : α → Bool} {xs : List α} {n : Nat} {a : α} (h : p a = true) : findIdxNth p (a :: xs) (n + 1) = findIdxNth p xs n + 1

theorem List.getElem_findIdxs_eq_findIdxNth_add {α : Type u_1} {n : Nat} {p : α → Bool} {s : Nat} {xs : List α} {h : n < (findIdxs p xs s).length} : (findIdxs p xs s)[n] = findIdxNth p xs n + s

theorem List.getElem_findIdxs_eq_findIdxNth {α : Type u_1} {n : Nat} {p : α → Bool} {xs : List α} {h : n < (findIdxs p xs).length} : (findIdxs p xs)[n] = findIdxNth p xs n

theorem List.pos_findIdxNth_getElem {α : Type u_1} {p : α → Bool} {n : Nat} {xs : List α} {h : findIdxNth p xs n < xs.length} : p xs[findIdxNth p xs n] = true

theorem List.findIdxNth_zero {α : Type u_1} {xs : List α} {p : α → Bool} : findIdxNth p xs 0 = findIdx p xs

theorem List.findIdxNth_lt_length_iff {α : Type u_1} {p : α → Bool} {n : Nat} {xs : List α} : findIdxNth p xs n < xs.length ↔ n < countP p xs

theorem List.findIdxNth_eq_length_iff {α : Type u_1} {p : α → Bool} {n : Nat} {xs : List α} : findIdxNth p xs n = xs.length ↔ countP p xs ≤ n

@[simp]

theorem List.findIdxNth_le_length {α : Type u_1} {p : α → Bool} {n : Nat} {xs : List α} : findIdxNth p xs n ≤ xs.length

theorem List.findIdxNth_lt_length_of_lt_countP {α : Type u_1} {n : Nat} {p : α → Bool} {xs : List α} (h : n < countP p xs) : findIdxNth p xs n < xs.length

theorem List.findIdxNth_eq_length_of_ge_countP {α : Type u_1} {p : α → Bool} {n : Nat} {xs : List α} : countP p xs ≤ n → findIdxNth p xs n = xs.length

theorem List.findIdxNth_le_findIdxNth_iff {α : Type u_1} {p : α → Bool} {n m : Nat} {xs : List α} : findIdxNth p xs n ≤ findIdxNth p xs m ↔ countP p xs ≤ m ∨ n ≤ m

theorem List.findIdxNth_lt_findIdxNth_iff {α : Type u_1} {p : α → Bool} {n m : Nat} {xs : List α} : findIdxNth p xs n < findIdxNth p xs m ↔ n < countP p xs ∧ n < m

theorem List.findIdxNth_eq_findIdxNth_iff {α : Type u_1} {p : α → Bool} {n m : Nat} {xs : List α} : findIdxNth p xs n = findIdxNth p xs m ↔ (countP p xs ≤ m ∨ n ≤ m) ∧ (countP p xs ≤ n ∨ m ≤ n)

theorem List.findIdxNth_lt_findIdxNth_iff_of_lt_countP {α : Type u_1} {n : Nat} {p : α → Bool} {m : Nat} {xs : List α} (hn : n < countP p xs) : findIdxNth p xs n < findIdxNth p xs m ↔ n < m

theorem List.findIdxNth_mono {α : Type u_1} {n m : Nat} {p : α → Bool} {xs : List α} (hnm : n ≤ m) : findIdxNth p xs n ≤ findIdxNth p xs m

theorem List.findIdxNth_eq_findIdxNth_iff_of_left_lt_countP {α : Type u_1} {n : Nat} {p : α → Bool} {m : Nat} {xs : List α} (hn : n < countP p xs) : findIdxNth p xs n = findIdxNth p xs m ↔ n = m

theorem List.findIdxNth_eq_findIdxNth_iff_of_right_lt_countP {α : Type u_1} {m : Nat} {p : α → Bool} {n : Nat} {xs : List α} (hm : m < countP p xs) : findIdxNth p xs n = findIdxNth p xs m ↔ n = m

theorem List.findIdxNth_eq_findIdxNth_of_ge_countP_ge_countP {α : Type u_1} {p : α → Bool} {n m : Nat} {xs : List α} (hn : countP p xs ≤ n) (hm : countP p xs ≤ m) : findIdxNth p xs n = findIdxNth p xs m

idxOf

@[simp]

theorem List.eraseIdx_idxOf_eq_erase {α : Type u_1} [BEq α] (a : α) (l : List α) : l.eraseIdx (idxOf a l) = l.erase a

theorem List.idxOf_eq_getD_idxOf? {α : Type u_1} [BEq α] (a : α) (l : List α) : idxOf a l = (idxOf? a l).getD l.length

@[deprecated List.idxOf_eq_getD_idxOf? (since := "2025-11-06")]

theorem List.idxOf_eq_idxOf? {α : Type u_1} [BEq α] (a : α) (l : List α) : idxOf a l = (idxOf? a l).getD l.length

Alias of List.idxOf_eq_getD_idxOf?.

@[simp]

theorem List.getElem_idxOf {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {xs : List α} (h : idxOf x xs < xs.length) : xs[idxOf x xs] = x

@[simp]

theorem List.Nodup.idxOf_getElem {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} (H : xs.Nodup) (i : Nat) (h : i < xs.length) : idxOf xs[i] xs = i

idxsOf

@[simp]

theorem List.idxsOf_nil {α : Type u_1} {x : α} {s : Nat} [BEq α] : idxsOf x [] s = []

@[simp]

theorem List.idxsOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} {s : Nat} [BEq α] : idxsOf y (x :: xs) s = if (x == y) = true then s :: idxsOf y xs (s + 1) else idxsOf y xs (s + 1)

theorem List.idxsOf_start {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] : idxsOf x xs s = map (fun (x : Nat) => x + s) (idxsOf x xs)

theorem List.idxsOf_eq_filterMap_zipIdx {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] : idxsOf x xs s = filterMap (fun (ab : α × Nat) => bif ab.fst == x then some ab.snd else none) (xs.zipIdx s)

@[simp]

theorem List.mem_idxsOf_iff_getElem_sub_pos {α : Type u_1} {xs : List α} {x : α} {s i : Nat} [BEq α] : i ∈ idxsOf x xs s ↔ s ≤ i ∧ ∃ (hix : i - s < xs.length), (xs[i - s] == x) = true

theorem List.mem_idxsOf_iff_exists_getElem_pos {α : Type u_1} {xs : List α} {x : α} {i : Nat} [BEq α] : i ∈ idxsOf x xs ↔ ∃ (hix : i < xs.length), (xs[i] == x) = true

theorem List.mem_idxsOf_iff_getElem_pos {α : Type u_1} {i : Nat} {xs : List α} {x : α} [BEq α] (hi : i < xs.length) : i ∈ idxsOf x xs ↔ (xs[i] == x) = true

theorem List.ge_of_mem_idxsOf {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] (y : Nat) : y ∈ idxsOf x xs s → s ≤ y

theorem List.lt_add_of_mem_idxsOf {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] (y : Nat) : y ∈ idxsOf x xs s → y < xs.length + s

theorem List.idxsOf_eq_nil_iff {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] : idxsOf x xs s = [] ↔ ∀ (y : α), y ∈ xs → (y == x) = false

@[simp]

theorem List.length_idxsOf {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] : (idxsOf x xs s).length = count x xs

@[simp]

theorem List.pairwise_idxsOf {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] : Pairwise (fun (x1 x2 : Nat) => x1 < x2) (idxsOf x xs s)

@[simp]

theorem List.isChain_idxsOf {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] : IsChain (fun (x1 x2 : Nat) => x1 < x2) (idxsOf x xs s)

@[simp]

theorem List.nodup_idxsOf {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] : (idxsOf x xs s).Nodup

@[simp]

theorem List.idxsOf_map {α : Type u_1} {β : Type u_2} {xs : List β} {x : α} {s : Nat} [BEq α] {f : β → α} : idxsOf x (map f xs) s = findIdxs (fun (x_1 : β) => f x_1 == x) xs s

@[simp]

theorem List.idxsOf_append {α : Type u_1} {xs ys : List α} {x : α} {s : Nat} [BEq α] : idxsOf x (xs ++ ys) s = idxsOf x xs s ++ idxsOf x ys (s + xs.length)

@[simp]

theorem List.idxsOf_take {α : Type u_1} {xs : List α} {n : Nat} {x : α} {s : Nat} [BEq α] : idxsOf x (take n xs) s = take (count x (take n xs)) (idxsOf x xs s)

@[simp]

theorem List.le_getElem_idxsOf {α : Type u_1} {i : Nat} {xs : List α} {x : α} {s : Nat} [BEq α] (h : i < (idxsOf x xs s).length) : s ≤ (idxsOf x xs s)[i]

@[simp]

theorem List.getElem_idxsOf_lt {α : Type u_1} {i : Nat} {xs : List α} {x : α} {s : Nat} [BEq α] (h : i < (idxsOf x xs s).length) : (idxsOf x xs s)[i] < xs.length + s

theorem List.getElem_getElem_idxsOf_sub {α : Type u_1} {i : Nat} {xs : List α} {x : α} [BEq α] (s : Nat) (h : i < (idxsOf x xs s).length) : (xs[(idxsOf x xs s)[i] - s] == x) = true

@[simp]

theorem List.getElem_getElem_idxsOf_sub_of_lawful {α : Type u_1} {i : Nat} {xs : List α} {x : α} [BEq α] [LawfulBEq α] (s : Nat) (h : i < (idxsOf x xs s).length) : xs[(idxsOf x xs s)[i] - s] = x

theorem List.getElem_getElem_idxsOf {α : Type u_1} {i : Nat} {xs : List α} {x : α} [BEq α] (h : i < (idxsOf x xs).length) : (xs[(idxsOf x xs)[i]] == x) = true

@[simp]

theorem List.getElem_getElem_idxsOf_of_lawful {α : Type u_1} {i : Nat} {xs : List α} {x : α} [BEq α] [LawfulBEq α] (h : i < (idxsOf x xs).length) : xs[(idxsOf x xs)[i]] = x

theorem List.mem_idxsOf_getElem {α : Type u_1} {i : Nat} {xs : List α} [BEq α] [EquivBEq α] (h : i < xs.length) : i ∈ idxsOf xs[i] xs

theorem List.getElem_zero_idxsOf_eq_idxOf_add {α : Type u_1} {xs : List α} {x : α} {s : Nat} [BEq α] (h : 0 < (idxsOf x xs s).length) : (idxsOf x xs s)[0] = idxOf x xs + s

@[simp]

theorem List.getElem_zero_idxsOf_eq_idxOf {α : Type u_1} {xs : List α} {x : α} [BEq α] (h : 0 < (idxsOf x xs).length) : (idxsOf x xs)[0] = idxOf x xs

theorem List.idxOf_add_mem_idxsOf {α : Type u_1} {xs : List α} {x : α} [BEq α] (s : Nat) (h : idxOf x xs < xs.length) : idxOf x xs + s ∈ idxsOf x xs s

theorem List.idxOf_mem_idxsOf {α : Type u_1} {xs : List α} {x : α} [BEq α] (h : idxOf x xs < xs.length) : idxOf x xs ∈ idxsOf x xs

idxOfNth

@[simp]

theorem List.idxOfNth_nil {α : Type u_1} {x : α} {n : Nat} [BEq α] : idxOfNth x [] n = 0

theorem List.idxOfNth_cons {α : Type u_1} {xs : List α} {x : α} {n : Nat} [BEq α] {a : α} : idxOfNth x (a :: xs) n = if n = 0 then if (a == x) = true then 0 else idxOfNth x xs 0 + 1 else if (a == x) = true then idxOfNth x xs (n - 1) + 1 else idxOfNth x xs n + 1

@[simp]

theorem List.idxOfNth_cons_zero {α : Type u_1} {xs : List α} {x : α} [BEq α] {a : α} : idxOfNth x (a :: xs) 0 = if (a == x) = true then 0 else idxOfNth x xs 0 + 1

@[simp]

theorem List.idxOfNth_cons_succ {α : Type u_1} {xs : List α} {x : α} {n : Nat} [BEq α] {a : α} : idxOfNth x (a :: xs) (n + 1) = if (a == x) = true then idxOfNth x xs n + 1 else idxOfNth x xs (n + 1) + 1

theorem List.idxOfNth_cons_of_not_beq {α : Type u_1} {x : α} {xs : List α} {n : Nat} {a : α} [BEq α] (h : (a == x) = false) : idxOfNth x (a :: xs) n = idxOfNth x xs n + 1

theorem List.idxOfNth_cons_of_beq {α : Type u_1} {x : α} {xs : List α} {n : Nat} {a : α} [BEq α] (h : (a == x) = true) : idxOfNth x (a :: xs) n = if n = 0 then 0 else idxOfNth x xs (n - 1) + 1

theorem List.idxOfNth_cons_zero_of_beq {α : Type u_1} {x : α} {xs : List α} {a : α} [BEq α] (h : (a == x) = true) : idxOfNth x (a :: xs) 0 = 0

theorem List.idxOfNth_cons_succ_of_beq {α : Type u_1} {x : α} {xs : List α} {n : Nat} {a : α} [BEq α] (h : (a == x) = true) : idxOfNth x (a :: xs) (n + 1) = idxOfNth x xs n + 1

theorem List.getElem_idxOf_eq_idxOfNth_add {α : Type u_1} {n : Nat} {x : α} {s : Nat} {xs : List α} [BEq α] {h : n < (idxsOf x xs s).length} : (idxsOf x xs s)[n] = idxOfNth x xs n + s

theorem List.getElem_idxOf_eq_idxOfNth {α : Type u_1} {n : Nat} {x : α} {xs : List α} [BEq α] {h : n < (idxsOf x xs).length} : (idxsOf x xs)[n] = idxOfNth x xs n

theorem List.getElem_idxOfNth_beq {α : Type u_1} {x : α} {n : Nat} {xs : List α} [BEq α] {h : idxOfNth x xs n < xs.length} : (xs[idxOfNth x xs n] == x) = true

@[simp]

theorem List.getElem_idxOfNth_eq {α : Type u_1} {x : α} {n : Nat} {xs : List α} [BEq α] [LawfulBEq α] {h : idxOfNth x xs n < xs.length} : xs[idxOfNth x xs n] = x

theorem List.idxOfNth_zero {α : Type u_1} {xs : List α} {x : α} [BEq α] : idxOfNth x xs 0 = idxOf x xs

theorem List.idxOfNth_lt_length_iff {α : Type u_1} {x : α} {n : Nat} [BEq α] {xs : List α} : idxOfNth x xs n < xs.length ↔ n < count x xs

theorem List.idxOfNth_eq_length_iff {α : Type u_1} {x : α} {n : Nat} [BEq α] {xs : List α} : idxOfNth x xs n = xs.length ↔ count x xs ≤ n

theorem List.idxOfNth_le_length {α : Type u_1} {x : α} {n : Nat} [BEq α] {xs : List α} : idxOfNth x xs n ≤ xs.length

theorem List.idxOfNth_lt_length_of_lt_count {α : Type u_1} {n : Nat} {x : α} {xs : List α} [BEq α] : n < count x xs → idxOfNth x xs n < xs.length

theorem List.idxOfNth_eq_length_of_ge_count {α : Type u_1} {x : α} {n : Nat} {xs : List α} [BEq α] : count x xs ≤ n → idxOfNth x xs n = xs.length

theorem List.idxOfNth_lt_idxOfNth_iff {α : Type u_1} {x : α} {n m : Nat} [BEq α] {xs : List α} : idxOfNth x xs n < idxOfNth x xs m ↔ n < count x xs ∧ n < m

theorem List.idxOfNth_eq_idxOfNth_iff {α : Type u_1} {x : α} {n m : Nat} [BEq α] {xs : List α} : idxOfNth x xs n = idxOfNth x xs m ↔ (count x xs ≤ m ∨ n ≤ m) ∧ (count x xs ≤ n ∨ m ≤ n)

theorem List.idxOfNth_lt_idxOfNth_iff_of_lt_count {α : Type u_1} {n : Nat} {x : α} {m : Nat} [BEq α] {xs : List α} (hn : n < count x xs) : idxOfNth x xs n < idxOfNth x xs m ↔ n < m

theorem List.idxOfNth_mono {α : Type u_1} {n m : Nat} {x : α} [BEq α] {xs : List α} (hnm : n ≤ m) : idxOfNth x xs n ≤ idxOfNth x xs m

theorem List.idxOfNth_eq_idxOfNth_iff_of_left_lt_count {α : Type u_1} {n : Nat} {x : α} {m : Nat} [BEq α] {xs : List α} (hn : n < count x xs) : idxOfNth x xs n = idxOfNth x xs m ↔ n = m

theorem List.idxOfNth_eq_idxOfNth_iff_of_right_lt_count {α : Type u_1} {m : Nat} {x : α} {n : Nat} [BEq α] {xs : List α} (hm : m < count x xs) : idxOfNth x xs n = idxOfNth x xs m ↔ n = m

theorem List.idxOfNth_eq_idxOfNth_of_ge_countP_ge_countP {α : Type u_1} {x : α} {n m : Nat} [BEq α] {xs : List α} (hn : count x xs ≤ n) (hm : count x xs ≤ m) : idxOfNth x xs n = idxOfNth x xs m

countPBefore

@[simp]

theorem List.countPBefore_nil {α : Type u_1} {p : α → Bool} {n : Nat} : countPBefore p [] n = 0

theorem List.countPBefore_cons {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} {a : α} : countPBefore p (a :: xs) i = if i = 0 then 0 else if p a = true then countPBefore p xs (i - 1) + 1 else countPBefore p xs (i - 1)

theorem List.countPBefore_cons_zero {α : Type u_1} {xs : List α} {p : α → Bool} {a : α} : countPBefore p (a :: xs) 0 = 0

@[simp]

theorem List.countPBefore_cons_succ {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} {a : α} : countPBefore p (a :: xs) (i + 1) = if p a = true then countPBefore p xs i + 1 else countPBefore p xs i

@[simp]

theorem List.countPBefore_zero {α : Type u_1} {xs : List α} {p : α → Bool} : countPBefore p xs 0 = 0

theorem List.countPBefore_succ {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} : countPBefore p xs (i + 1) = if h : xs = [] then 0 else if p (xs.head h) = true then countPBefore p xs.tail i + 1 else countPBefore p xs.tail i

theorem List.countPBefore_cons_succ_of_neg {α : Type u_1} {p : α → Bool} {xs : List α} {i : Nat} {a : α} (h : p a = false) : countPBefore p (a :: xs) (i + 1) = countPBefore p xs i

theorem List.countPBefore_cons_succ_of_pos {α : Type u_1} {p : α → Bool} {xs : List α} {i : Nat} {a : α} (h : p a = true) : countPBefore p (a :: xs) (i + 1) = countPBefore p xs i + 1

theorem List.countPBefore_eq_countP_take {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} : countPBefore p xs i = countP p (take i xs)

theorem List.countPBefore_of_ge_length {α : Type u_1} {i : Nat} {p : α → Bool} {xs : List α} (hi : xs.length ≤ i) : countPBefore p xs i = countP p xs

theorem List.countPBefore_length {α : Type u_1} {p : α → Bool} {xs : List α} : countPBefore p xs xs.length = countP p xs

@[simp]

theorem List.findIdxNth_countPBefore_of_lt_length_of_pos {α : Type u_1} {i : Nat} {p : α → Bool} {xs : List α} {h : i < xs.length} (hip : p xs[i] = true) : findIdxNth p xs (countPBefore p xs i) = i

@[simp]

theorem List.countPBefore_findIdxNth_of_lt_countP {α : Type u_1} {n : Nat} {p : α → Bool} {xs : List α} : n < countP p xs → countPBefore p xs (findIdxNth p xs n) = n

theorem List.pos_iff_exists_findIdxNth {α : Type u_1} {i : Nat} {p : α → Bool} {xs : List α} {h : i < xs.length} : p xs[i] = true ↔ ∃ (n : Nat), findIdxNth p xs n = i

theorem List.countPBefore_le_countP {α : Type u_1} {i : Nat} {xs : List α} (p : α → Bool) : countPBefore p xs i ≤ countP p xs

theorem List.countPBefore_mono {α : Type u_1} {i j : Nat} {p : α → Bool} {xs : List α} (hij : i ≤ j) : countPBefore p xs i ≤ countPBefore p xs j

theorem List.countPBefore_lt_countP_of_lt_length_of_pos {α : Type u_1} {i : Nat} {p : α → Bool} {xs : List α} {h : i < xs.length} (hip : p xs[i] = true) : countPBefore p xs i < countP p xs

countBefore

@[simp]

theorem List.countBefore_nil {α : Type u_1} {x : α} {i : Nat} [BEq α] : countBefore x [] i = 0

theorem List.countBefore_cons {α : Type u_1} {xs : List α} {x : α} {i : Nat} [BEq α] {a : α} : countBefore x (a :: xs) i = if i = 0 then 0 else if (a == x) = true then countBefore x xs (i - 1) + 1 else countBefore x xs (i - 1)

@[simp]

theorem List.countBefore_zero {α : Type u_1} {xs : List α} {p : α} [BEq α] : countBefore p xs 0 = 0

@[simp]

theorem List.countBefore_cons_succ {α : Type u_1} {xs : List α} {x : α} {i : Nat} {a : α} [BEq α] : countBefore x (a :: xs) (i + 1) = countBefore x xs i + if (a == x) = true then 1 else 0

theorem List.countBefore_cons_succ_of_not_beq {α : Type u_1} {x : α} {xs : List α} {i : Nat} [BEq α] {a : α} (h : (a == x) = false) : countBefore x (a :: xs) (i + 1) = countBefore x xs i

theorem List.countBefore_cons_succ_of_beq {α : Type u_1} {x : α} {xs : List α} {i : Nat} {a : α} [BEq α] (h : (a == x) = true) : countBefore x (a :: xs) (i + 1) = countBefore x xs i + 1

theorem List.countBefore_eq_count_take {α : Type u_1} {xs : List α} {x : α} {i : Nat} [BEq α] : countBefore x xs i = count x (take i xs)

theorem List.countBefore_idxOfNth_of_lt_count {α : Type u_1} {n : Nat} {x : α} [BEq α] {xs : List α} (hn : n < count x xs) : countBefore x xs (idxOfNth x xs n) = n

theorem List.idxOfNth_countBefore_of_lt_length_of_beq {α : Type u_1} {i : Nat} {x : α} [BEq α] {xs : List α} {h : i < xs.length} (hip : (xs[i] == x) = true) : idxOfNth x xs (countBefore x xs i) = i

@[simp]

theorem List.idxOfNth_countBefore_getElem {α : Type u_1} {i : Nat} [BEq α] [ReflBEq α] {xs : List α} {h : i < xs.length} : idxOfNth xs[i] xs (countBefore xs[i] xs i) = i

theorem List.beq_iff_exists_findIdxNth {α : Type u_1} {i : Nat} {x : α} [BEq α] {xs : List α} {h : i < xs.length} : (xs[i] == x) = true ↔ ∃ (n : Nat), idxOfNth x xs n = i

theorem List.countBefore_le_count {α : Type u_1} {x : α} {i : Nat} [BEq α] {xs : List α} : countBefore x xs i ≤ count x xs

theorem List.countBefore_lt_count_of_lt_length_of_beq {α : Type u_1} {i : Nat} {x : α} [BEq α] {xs : List α} {h : i < xs.length} (hip : (xs[i] == x) = true) : countBefore x xs i < count x xs

@[simp]

theorem List.countBefore_lt_count_getElem {α : Type u_1} {i : Nat} [BEq α] [ReflBEq α] {xs : List α} {h : i < xs.length} : countBefore xs[i] xs i < count xs[i] xs

theorem List.countBefore_of_ge_length {α : Type u_1} {i : Nat} {x : α} [BEq α] {xs : List α} (hi : xs.length ≤ i) : countBefore x xs i = count x xs

insertP

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)

@[simp]

theorem List.insertP_nil {α : Type u_1} (p : α → Bool) (a : α) : insertP p a [] = [a]

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

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

@[simp]

theorem List.length_insertP {α : Type u_1} (p : α → Bool) (a : α) (l : List α) : (insertP p a l).length = l.length + 1

@[simp]

theorem List.mem_insertP {α : Type u_1} (p : α → Bool) (a : α) (l : List α) : a ∈ insertP p a l

dropPrefix?, dropSuffix?, dropInfix?

@[simp]

theorem List.dropPrefix?_nil {α : Type u_1} [BEq α] {p : List α} : p.dropPrefix? [] = some p

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

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

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

@[simp]

theorem List.dropSuffix?_nil {α : Type u_1} [BEq α] {s : List α} : s.dropSuffix? [] = some s

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

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

@[simp]

theorem List.dropInfix?_nil {α : Type u_1} [BEq α] {s : List α} : s.dropInfix? [] = some ([], s)

IsPrefixOf?, IsSuffixOf?

@[simp]

theorem List.isSome_isPrefixOf?_eq_isPrefixOf {α : Type u_1} [BEq α] (xs ys : List α) : (xs.isPrefixOf? ys).isSome = xs.isPrefixOf ys

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

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

@[simp]

theorem List.isSome_isSuffixOf?_eq_isSuffixOf {α : Type u_1} [BEq α] (xs ys : List α) : (xs.isSuffixOf? ys).isSome = xs.isSuffixOf ys

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

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

finRange

theorem List.get_finRange {n : Nat} (i : Fin (finRange n).length) : (finRange n).get i = Fin.cast ⋯ i

@[simp]

theorem List.finRange_eq_nil_iff {n : Nat} : finRange n = [] ↔ n = 0

theorem List.finRange_eq_pmap_range {n : Nat} : finRange n = pmap Fin.mk (range n) ⋯

theorem List.nodup_finRange (n : Nat) : (finRange n).Nodup

theorem List.pairwise_lt_finRange (n : Nat) : Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (finRange n)

theorem List.pairwise_le_finRange (n : Nat) : Pairwise (fun (x1 x2 : Fin n) => x1 ≤ x2) (finRange n)

@[simp]

theorem List.map_get_finRange {α : Type u_1} (l : List α) : map l.get (finRange l.length) = l

@[simp]

theorem List.map_getElem_finRange {α : Type u_1} (l : List α) : map (fun (x : Fin l.length) => l[↑x]) (finRange l.length) = l

@[simp]

theorem List.map_coe_finRange_eq_range {n : Nat} : map (fun (x : Fin n) => ↑x) (finRange n) = range n

sum/prod

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

@[simp]

theorem List.prod_nil {α : Type u_1} [Mul α] [One α] : [].prod = 1

@[simp]

theorem List.prod_cons {α : Type u_1} [Mul α] [One α] {a : α} {l : List α} : (a :: l).prod = a * l.prod

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

theorem List.prod_singleton {α : Type u_1} [Mul α] [One α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 * x2) 1] {a : α} : [a].prod = a

theorem List.prod_pair {α : Type u_1} [Mul α] [One α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 * x2) 1] {a b : α} : [a, b].prod = a * b

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

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

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

theorem List.prod_eq_foldr {α : Type u_1} [Mul α] [One α] {l : List α} : l.prod = foldr (fun (x1 x2 : α) => x1 * x2) 1 l

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

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

theorem List.sum_singleton {α : Type u_1} [Add α] [Zero α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 + x2) 0] {a : α} : [a].sum = a

theorem List.sum_pair {α : Type u_1} [Add α] [Zero α] [Std.LawfulRightIdentity (fun (x1 x2 : α) => x1 + x2) 0] {a b : α} : [a, b].sum = a + b

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

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

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

theorem List.take_succ_drop {α : Type u_1} {l : List α} {n stop : Nat} (h : n < l.length - stop) : take (n + 1) (drop stop l) = take n (drop stop l) ++ [l[stop + n]]