toArray

@[simp]

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

get?

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

@[deprecated List.getElem?_inj]

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

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 :: List.modifyNth f n l

theorem List.modifyNthTail_id {α : Type u_1} (n : Nat) (l : List α) : List.modifyNthTail id n l = 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) : (List.modifyNth f n l)[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) : (List.modifyNth f n l).get? m = (fun (a : α) => if n = m then f a else a) <$> l.get? m

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

@[deprecated List.length_modifyNthTail]

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

Alias of List.length_modifyNthTail.

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₁ ++ List.modifyNthTail f n 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 ∧ List.modifyNthTail f n l = l₁ ++ f l₂

@[simp]

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

@[deprecated List.length_modifyNth]

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

Alias of List.length_modifyNth.

@[simp]

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

@[deprecated List.getElem?_modifyNth_eq]

theorem List.get?_modifyNth_eq {α : Type u_1} (f : α → α) (n : Nat) (l : List α) : (List.modifyNth f n l).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) : (List.modifyNth f m l)[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) : (List.modifyNth f m l).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 ∧ List.modifyNth f n l = l₁ ++ f a :: l₂

theorem List.modifyNthTail_eq_take_drop {α : Type u_1} (f : List α → List α) (H : f [] = []) (n : Nat) (l : List α) : List.modifyNthTail f n l = List.take n l ++ f (List.drop n l)

theorem List.modifyNth_eq_take_drop {α : Type u_1} (f : α → α) (n : Nat) (l : List α) : List.modifyNth f n l = List.take n l ++ List.modifyHead f (List.drop n l)

theorem List.modifyNth_eq_take_cons_drop {α : Type u_1} (f : α → α) {n : Nat} {l : List α} (h : n < l.length) : List.modifyNth f n l = List.take n l ++ 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 = List.take n l ++ a :: List.drop (n + 1) l

theorem List.modifyNth_eq_set_get? {α : Type u_1} (f : α → α) (n : Nat) (l : List α) : List.modifyNth f n l = ((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) : List.modifyNth f n l = l.set n (f (l.get ⟨n, h⟩))

@[deprecated List.exists_of_set]

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₂

@[deprecated List.getElem?_set_self']

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

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

@[deprecated List.length_eraseIdx]

theorem List.length_removeNth {α : Type u_1} (l : List α) (i : Nat) : (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length

Alias of List.length_eraseIdx.

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 α) : List.extractP p l = (List.find? p l, List.eraseP p l)

theorem List.extractP_eq_find?_eraseP.go {α : Type u_1} {p : α → Bool} (l : List α) (acc : Array α) (xs : List α) : l = acc.toList ++ xs → List.extractP.go p l xs acc = (List.find? p xs, acc.toList ++ List.eraseP p xs)

erase

@[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.erase_eq_self_iff_forall_bne {α : Type u_1} [BEq α] (a : α) (xs : List α) : xs.erase a = xs ↔ ∀ (x : α), x ∈ xs → ¬(x == a) = true

findIdx?

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

replaceF

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

theorem List.replaceF_cons {α : Type u_1} {p : α → Option α} (a : α) (l : List α) : List.replaceF p (a :: l) = match p a with | none => a :: List.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') : List.replaceF p (a :: l) = a' :: l

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

theorem List.replaceF_of_forall_none {α : Type u_1} {p : α → Option α} {l : List α} (h : ∀ (a : α), a ∈ l → p a = none) : List.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₂ ∧ List.replaceF p l = l₁ ++ a' :: l₂

theorem List.exists_or_eq_self_of_replaceF {α : Type u_1} (p : α → Option α) (l : List α) : 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₂ ∧ List.replaceF p l = l₁ ++ a' :: l₂

@[simp]

theorem List.length_replaceF : ∀ {α : Type u_1} {f : α → Option α} {l : List α}, (List.replaceF f l).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₁ ⊆ l → l.Disjoint l₂ → l₁.Disjoint l₂

theorem List.disjoint_of_subset_right : ∀ {α : Type u_1} {l₂ l l₁ : List α}, l₂ ⊆ l → 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 α}, (l₁ ++ l₂).Disjoint l → l₁.Disjoint l

theorem List.disjoint_of_disjoint_append_left_right : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l → l₂.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₂

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 α] [LawfulBEq α] {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 α] [LawfulBEq α] {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.

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₁ : List α) (l₂ : List α) (a : α) : l₁.diff (a :: l₂) = (l₁.erase a).diff l₂

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

theorem List.diff_erase {α : Type u_1} [BEq α] [LawfulBEq α] (l₁ : List α) (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₁ : 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 α] [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₁ : List α) (l₂ : List α) : l₁.diff l₂ = List.foldl List.erase l₁ l₂

@[simp]

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

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

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

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

theorem List.Sublist.diff_right {α : Type u_1} [BEq α] [LawfulBEq α] {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 α] [LawfulBEq α] {a : α} {l₁ : List α} {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 : Nat} {n : Nat} {l : List α} : l.Nodup → m ≤ n → (List.take m l).Disjoint (List.drop n l)

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)) : List.Chain R b l

theorem List.Chain.imp' {α : Type u_1} {R : α → α → Prop} {S : α → α → Prop} (HRS : ∀ ⦃a b : α⦄, R a b → S a b) {a : α} {b : α} (Hab : ∀ ⦃c : α⦄, R a c → S b c) {l : List α} (p : List.Chain R a l) : List.Chain S b l

theorem List.Chain.imp {α : Type u_1} {R : α → α → Prop} {S : α → α → Prop} (H : ∀ (a b : α), R a b → S a b) {a : α} {l : List α} (p : List.Chain R a l) : List.Chain S 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.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 (x1 x2 : Nat) => x1 < x2) s (List.range' (s + step) n step)

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

@[deprecated List.getElem?_range]

theorem List.get?_range {m : Nat} {n : Nat} (h : m < n) : (List.range n).get? m = some m

@[deprecated List.getElem_range]

theorem List.get_range {n : Nat} (i : Nat) (H : i < (List.range n).length) : (List.range n).get ⟨i, H⟩ = i

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 : List Nat) => 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 : List Nat) => 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) (List.findIdxs p xs) else List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs)

@[simp]

theorem List.indexesOf_nil {α : Type u_1} {x : α} [BEq α] : List.indexesOf x [] = []

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) (List.indexesOf y xs) else List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs)

@[simp]

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

theorem List.indexOf_mem_indexesOf {α : Type u_1} {x : α} [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) : List.indexOf x xs ∈ List.indexesOf x xs

@[simp]

theorem List.indexOf?_nil {α : Type u_1} {x : α} [BEq α] : List.indexOf? x [] = none

theorem List.indexOf?_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] : List.indexOf? y (x :: xs) = if (x == y) = true then some 0 else Option.map Nat.succ (List.indexOf? y xs)

theorem List.indexOf?_eq_none_iff {α : Type u_1} [BEq α] {a : α} {l : List α} : List.indexOf? a l = none ↔ ∀ (x : α), x ∈ l → ¬(x == a) = true

theorem List.indexOf_eq_indexOf? {α : Type u_1} [BEq α] (a : α) (l : List α) : List.indexOf a l = match List.indexOf? a l with | some i => i | none => l.length

insertP

theorem List.insertP_loop {α : Type u_1} {p : α → Bool} (a : α) (l : List α) (r : List α) : List.insertP.loop p a l r = r.reverseAux (List.insertP p a l)

@[simp]

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

@[simp]

theorem List.insertP_cons_pos {α : Type u_1} (p : α → Bool) (a : α) (b : α) (l : List α) (h : p b = true) : List.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) : List.insertP p a (b :: l) = b :: List.insertP p a l

@[simp]

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

@[simp]

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

foldlM and foldrM

theorem List.foldlM_map {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : List β₁) (init : α) : List.foldlM g init (List.map f l) = List.foldlM (fun (x : α) (y : β₁) => g x (f y)) init l

theorem List.foldrM_map {m : Type u_1 → Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {α : Type u_1} [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : List β₁) (init : α) : List.foldrM g init (List.map f l) = List.foldrM (fun (x : β₁) (y : α) => g (f x) y) init l