Documentation

Init.Data.List.Find

Lemmas about List.findSome?, List.find?, List.findIdx, List.findIdx?, and List.indexOf. #

findSome? #

@[simp]
theorem List.findSome?_cons_of_isSome :
∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {a : α} (l : List α), (f a).isSome = trueList.findSome? f (a :: l) = f a
@[simp]
theorem List.findSome?_cons_of_isNone :
∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {a : α} (l : List α), (f a).isNone = trueList.findSome? f (a :: l) = List.findSome? f l
theorem List.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : αOption β} (w : List.findSome? f l = some b) :
∃ (a : α), a l f a = some b
@[simp]
theorem List.findSome?_eq_none_iff :
∀ {α : Type u_1} {α_1 : Type u_2} {p : αOption α_1} {l : List α}, List.findSome? p l = none ∀ (x : α), x lp x = none
@[reducible, inline, deprecated List.findSome?_eq_none_iff]
abbrev List.findSome?_eq_none :
∀ {α : Type u_1} {α_1 : Type u_2} {p : αOption α_1} {l : List α}, List.findSome? p l = none ∀ (x : α), x lp x = none
Equations
Instances For
    @[simp]
    theorem List.findSome?_isSome_iff {α : Type u_1} {β : Type u_2} {f : αOption β} {l : List α} :
    (List.findSome? f l).isSome = true ∃ (x : α), x l (f x).isSome = true
    theorem List.findSome?_eq_some_iff {α : Type u_1} {β : Type u_2} {f : αOption β} {l : List α} {b : β} :
    List.findSome? f l = some b ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ f a = some b ∀ (x : α), x l₁f x = none
    @[simp]
    theorem List.findSome?_guard {α : Type u_1} {p : αBool} (l : List α) :
    List.findSome? (Option.guard fun (x : α) => p x = true) l = List.find? p l
    @[simp]
    theorem List.filterMap_head? {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
    @[simp]
    theorem List.filterMap_head {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) (h : List.filterMap f l []) :
    (List.filterMap f l).head h = (List.findSome? f l).get
    @[simp]
    theorem List.filterMap_getLast? {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
    (List.filterMap f l).getLast? = List.findSome? f l.reverse
    @[simp]
    theorem List.filterMap_getLast {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) (h : List.filterMap f l []) :
    (List.filterMap f l).getLast h = (List.findSome? f l.reverse).get
    @[simp]
    theorem List.map_findSome? {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption β) (g : βγ) (l : List α) :
    theorem List.findSome?_map {β : Type u_1} {γ : Type u_2} :
    ∀ {α : Type u_3} {p : γOption α} (f : βγ) (l : List β), List.findSome? p (List.map f l) = List.findSome? (p f) l
    theorem List.findSome?_append {α : Type u_1} :
    ∀ {α_1 : Type u_2} {f : αOption α_1} {l₁ l₂ : List α}, List.findSome? f (l₁ ++ l₂) = (List.findSome? f l₁).or (List.findSome? f l₂)
    theorem List.head_join {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l L l []) :
    L.join.head = (List.findSome? (fun (l : List α) => l.head?) L).get
    theorem List.getLast_join {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l L l []) :
    L.join.getLast = (List.findSome? (fun (l : List α) => l.getLast?) L.reverse).get
    theorem List.findSome?_replicate :
    ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {n : Nat} {a : α}, List.findSome? f (List.replicate n a) = if n = 0 then none else f a
    @[simp]
    theorem List.findSome?_replicate_of_pos {n : Nat} :
    ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {a : α}, 0 < nList.findSome? f (List.replicate n a) = f a
    @[simp]
    theorem List.findSome?_replicate_of_isSome :
    ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {n : Nat} {a : α}, (f a).isSome = trueList.findSome? f (List.replicate n a) = if n = 0 then none else f a
    @[simp]
    theorem List.findSome?_replicate_of_isNone :
    ∀ {α : Type u_1} {α_1 : Type u_2} {f : αOption α_1} {n : Nat} {a : α}, (f a).isNone = trueList.findSome? f (List.replicate n a) = none
    theorem List.Sublist.findSome?_isSome {α : Type u_1} :
    ∀ {α_1 : Type u_2} {f : αOption α_1} {l₁ l₂ : List α}, l₁.Sublist l₂(List.findSome? f l₁).isSome = true(List.findSome? f l₂).isSome = true
    theorem List.Sublist.findSome?_eq_none {α : Type u_1} :
    ∀ {α_1 : Type u_2} {f : αOption α_1} {l₁ l₂ : List α}, l₁.Sublist l₂List.findSome? f l₂ = noneList.findSome? f l₁ = none
    theorem List.IsPrefix.findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l₁ : List α} {l₂ : List α} {f : αOption β} (h : l₁ <+: l₂) :
    List.findSome? f l₁ = some bList.findSome? f l₂ = some b
    theorem List.IsPrefix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} {f : αOption β} (h : l₁ <+: l₂) :
    List.findSome? f l₂ = noneList.findSome? f l₁ = none
    theorem List.IsSuffix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} {f : αOption β} (h : l₁ <:+ l₂) :
    List.findSome? f l₂ = noneList.findSome? f l₁ = none
    theorem List.IsInfix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List α} {f : αOption β} (h : l₁ <:+: l₂) :
    List.findSome? f l₂ = noneList.findSome? f l₁ = none

    find? #

    @[simp]
    theorem List.find?_singleton {α : Type u_1} (a : α) (p : αBool) :
    List.find? p [a] = if p a = true then some a else none
    @[simp]
    theorem List.find?_cons_of_pos :
    ∀ {α : Type u_1} {p : αBool} {a : α} (l : List α), p a = trueList.find? p (a :: l) = some a
    @[simp]
    theorem List.find?_cons_of_neg :
    ∀ {α : Type u_1} {p : αBool} {a : α} (l : List α), ¬p a = trueList.find? p (a :: l) = List.find? p l
    @[simp]
    theorem List.find?_eq_none :
    ∀ {α : Type u_1} {p : αBool} {l : List α}, List.find? p l = none ∀ (x : α), x l¬p x = true
    theorem List.find?_eq_some :
    ∀ {α : Type u_1} {b : α} {p : αBool} {xs : List α}, List.find? p xs = some b p b = true ∃ (as : List α), ∃ (bs : List α), xs = as ++ b :: bs ∀ (a : α), a as(!p a) = true
    @[simp]
    theorem List.find?_cons_eq_some :
    ∀ {α : Type u_1} {a : α} {xs : List α} {p : αBool} {b : α}, List.find? p (a :: xs) = some b p a = true a = b (!p a) = true List.find? p xs = some b
    @[simp]
    theorem List.find?_isSome {α : Type u_1} {xs : List α} {p : αBool} :
    (List.find? p xs).isSome = true ∃ (x : α), x xs p x = true
    theorem List.find?_some :
    ∀ {α : Type u_1} {p : αBool} {a : α} {l : List α}, List.find? p l = some ap a = true
    theorem List.mem_of_find?_eq_some :
    ∀ {α : Type u_1} {p : αBool} {a : α} {l : List α}, List.find? p l = some aa l
    theorem List.get_find?_mem {α : Type u_1} (xs : List α) (p : αBool) (h : (List.find? p xs).isSome = true) :
    (List.find? p xs).get h xs
    @[simp]
    theorem List.find?_filter {α : Type u_1} (xs : List α) (p : αBool) (q : αBool) :
    List.find? q (List.filter p xs) = List.find? (fun (a : α) => decide (p a = true q a = true)) xs
    @[simp]
    theorem List.filter_head? {α : Type u_1} (p : αBool) (l : List α) :
    (List.filter p l).head? = List.find? p l
    @[simp]
    theorem List.filter_head {α : Type u_1} (p : αBool) (l : List α) (h : List.filter p l []) :
    (List.filter p l).head h = (List.find? p l).get
    @[simp]
    theorem List.filter_getLast? {α : Type u_1} (p : αBool) (l : List α) :
    (List.filter p l).getLast? = List.find? p l.reverse
    @[simp]
    theorem List.filter_getLast {α : Type u_1} (p : αBool) (l : List α) (h : List.filter p l []) :
    (List.filter p l).getLast h = (List.find? p l.reverse).get
    @[simp]
    theorem List.find?_filterMap {α : Type u_1} {β : Type u_2} (xs : List α) (f : αOption β) (p : βBool) :
    List.find? p (List.filterMap f xs) = (List.find? (fun (a : α) => Option.any p (f a)) xs).bind f
    @[simp]
    theorem List.find?_map {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) :
    @[simp]
    theorem List.find?_append {α : Type u_1} {p : αBool} {l₁ : List α} {l₂ : List α} :
    List.find? p (l₁ ++ l₂) = (List.find? p l₁).or (List.find? p l₂)
    @[simp]
    theorem List.find?_join {α : Type u_1} (xs : List (List α)) (p : αBool) :
    List.find? p xs.join = List.findSome? (fun (x : List α) => List.find? p x) xs
    theorem List.find?_join_eq_none {α : Type u_1} {xs : List (List α)} {p : αBool} :
    List.find? p xs.join = none ∀ (ys : List α), ys xs∀ (x : α), x ys(!p x) = true
    theorem List.find?_join_eq_some {α : Type u_1} {xs : List (List α)} {p : αBool} {a : α} :
    List.find? p xs.join = some a p a = true ∃ (as : List (List α)), ∃ (ys : List α), ∃ (zs : List α), ∃ (bs : List (List α)), xs = as ++ (ys ++ a :: zs) :: bs (∀ (a : List α), a as∀ (x : α), x a(!p x) = true) ∀ (x : α), x ys(!p x) = true

    If find? p returns some a from xs.join, then p a holds, and some list in xs contains a, and no earlier element of that list satisfies p. Moreover, no earlier list in xs has an element satisfying p.

    @[simp]
    theorem List.find?_bind {α : Type u_1} {β : Type u_2} (xs : List α) (f : αList β) (p : βBool) :
    List.find? p (xs.bind f) = List.findSome? (fun (x : α) => List.find? p (f x)) xs
    theorem List.find?_bind_eq_none {α : Type u_1} {β : Type u_2} {xs : List α} {f : αList β} {p : βBool} :
    List.find? p (xs.bind f) = none ∀ (x : α), x xs∀ (y : β), y f x(!p y) = true
    theorem List.find?_replicate :
    ∀ {α : Type u_1} {p : αBool} {n : Nat} {a : α}, List.find? p (List.replicate n a) = if n = 0 then none else if p a = true then some a else none
    @[simp]
    theorem List.find?_replicate_of_length_pos {n : Nat} :
    ∀ {α : Type u_1} {p : αBool} {a : α}, 0 < nList.find? p (List.replicate n a) = if p a = true then some a else none
    @[simp]
    theorem List.find?_replicate_of_pos :
    ∀ {α : Type u_1} {p : αBool} {n : Nat} {a : α}, p a = trueList.find? p (List.replicate n a) = if n = 0 then none else some a
    @[simp]
    theorem List.find?_replicate_of_neg :
    ∀ {α : Type u_1} {p : αBool} {n : Nat} {a : α}, ¬p a = trueList.find? p (List.replicate n a) = none
    theorem List.find?_replicate_eq_none {α : Type u_1} {n : Nat} {a : α} {p : αBool} :
    List.find? p (List.replicate n a) = none n = 0 (!p a) = true
    @[simp]
    theorem List.find?_replicate_eq_some {α : Type u_1} {n : Nat} {a : α} {b : α} {p : αBool} :
    List.find? p (List.replicate n a) = some b n 0 p a = true a = b
    @[simp]
    theorem List.get_find?_replicate {α : Type u_1} (n : Nat) (a : α) (p : αBool) (h : (List.find? p (List.replicate n a)).isSome = true) :
    (List.find? p (List.replicate n a)).get h = a
    theorem List.Sublist.find?_isSome {α : Type u_1} {p : αBool} {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) :
    (List.find? p l₁).isSome = true(List.find? p l₂).isSome = true
    theorem List.Sublist.find?_eq_none {α : Type u_1} {p : αBool} {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) :
    List.find? p l₂ = noneList.find? p l₁ = none
    theorem List.IsPrefix.find?_eq_some {α : Type u_1} {b : α} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <+: l₂) :
    List.find? p l₁ = some bList.find? p l₂ = some b
    theorem List.IsPrefix.find?_eq_none {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <+: l₂) :
    List.find? p l₂ = noneList.find? p l₁ = none
    theorem List.IsSuffix.find?_eq_none {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <:+ l₂) :
    List.find? p l₂ = noneList.find? p l₁ = none
    theorem List.IsInfix.find?_eq_none {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <:+: l₂) :
    List.find? p l₂ = noneList.find? p l₁ = none
    theorem List.find?_pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (xs : List α) (H : ∀ (a : α), a xsP a) (p : βBool) :
    List.find? p (List.pmap f xs H) = Option.map (fun (x : { x : α // x xs }) => match x with | a, m => f a ) (List.find? (fun (x : { x : α // x xs }) => match x with | a, m => p (f a )) xs.attach)

    findIdx #

    theorem List.findIdx_cons {α : Type u_1} (p : αBool) (b : α) (l : List α) :
    List.findIdx p (b :: l) = bif p b then 0 else List.findIdx p l + 1
    theorem List.findIdx_cons.findIdx_go_succ {α : Type u_1} (p : αBool) (l : List α) (n : Nat) :
    List.findIdx.go p l (n + 1) = List.findIdx.go p l n + 1
    theorem List.findIdx_of_getElem?_eq_some {α : Type u_1} {p : αBool} {y : α} {xs : List α} (w : xs[List.findIdx p xs]? = some y) :
    p y = true
    theorem List.findIdx_getElem {α : Type u_1} {p : αBool} {xs : List α} {w : List.findIdx p xs < xs.length} :
    p xs[List.findIdx p xs] = true
    @[deprecated List.findIdx_of_getElem?_eq_some]
    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
    @[deprecated List.findIdx_getElem]
    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_getElem?_eq_getElem_of_exists {α : Type u_1} {p : αBool} {xs : List α} (h : ∃ (x : α), x xs p x = true) :
    xs[List.findIdx p xs]? = some xs[List.findIdx p xs]
    @[deprecated List.findIdx_getElem?_eq_getElem_of_exists]
    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, )
    @[simp]
    theorem List.findIdx_eq_length {α : Type u_1} {p : αBool} {xs : List α} :
    List.findIdx p xs = xs.length ∀ (x : α), x xsp x = false
    theorem List.findIdx_eq_length_of_false {α : Type u_1} {p : αBool} {xs : List α} (h : ∀ (x : α), x xsp x = false) :
    List.findIdx p xs = xs.length
    theorem List.findIdx_le_length {α : Type u_1} (p : αBool) {xs : List α} :
    List.findIdx p xs xs.length
    @[simp]
    theorem List.findIdx_lt_length {α : Type u_1} {p : αBool} {xs : List α} :
    List.findIdx p xs < xs.length ∃ (x : α), x xs p x = true
    theorem List.not_of_lt_findIdx {α : Type u_1} {p : αBool} {xs : List α} {i : Nat} (h : i < List.findIdx p xs) :
    p xs[i] = false

    p does not hold for elements with indices less than xs.findIdx p.

    theorem List.le_findIdx_of_not {α : Type u_1} {p : αBool} {xs : List α} {i : Nat} (h : i < xs.length) (h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false) :

    If ¬ p xs[j] for all j < i, then i ≤ xs.findIdx p.

    theorem List.lt_findIdx_of_not {α : Type u_1} {p : αBool} {xs : List α} {i : Nat} (h : i < xs.length) (h2 : ∀ (j : Nat) (hji : j i), ¬p (xs.get j, ) = true) :

    If ¬ p xs[j] for all j ≤ i, then i < xs.findIdx p.

    theorem List.findIdx_eq {α : Type u_1} {p : αBool} {xs : List α} {i : Nat} (h : i < xs.length) :
    List.findIdx p xs = i p xs[i] = true ∀ (j : Nat) (hji : j < i), p xs[j] = false

    xs.findIdx p = i iff p xs[i] and ¬ p xs [j] for all j < i.

    theorem List.findIdx_append {α : Type u_1} (p : αBool) (l₁ : List α) (l₂ : List α) :
    List.findIdx p (l₁ ++ l₂) = if ∃ (x : α), x l₁ p x = true then List.findIdx p l₁ else List.findIdx p l₂ + l₁.length
    theorem List.IsPrefix.findIdx_le {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <+: l₂) :
    theorem List.IsPrefix.findIdx_eq_of_findIdx_lt_length {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <+: l₂) (lt : List.findIdx p l₁ < l₁.length) :
    theorem List.findIdx_le_findIdx {α : Type u_1} {l : List α} {p : αBool} {q : αBool} (h : ∀ (x : α), x lp x = trueq x = true) :

    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)
    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)
    @[simp]
    theorem List.findIdx?_start_succ {α : Type u_1} {xs : List α} {p : αBool} {i : Nat} :
    List.findIdx? p xs (i + 1) = Option.map (fun (k : Nat) => k + (i + 1)) (List.findIdx? p xs)
    @[simp]
    theorem List.findIdx?_eq_none_iff {α : Type u_1} {xs : List α} {p : αBool} :
    List.findIdx? p xs = none ∀ (x : α), x xsp x = false
    theorem List.findIdx?_isSome {α : Type u_1} {xs : List α} {p : αBool} :
    (List.findIdx? p xs).isSome = xs.any p
    theorem List.findIdx?_isNone {α : Type u_1} {xs : List α} {p : αBool} :
    (List.findIdx? p xs).isNone = xs.all fun (x : α) => decide ¬p x = true
    theorem List.findIdx?_eq_some_iff_findIdx_eq {α : Type u_1} {xs : List α} {p : αBool} {i : Nat} :
    List.findIdx? p xs = some i i < xs.length List.findIdx p xs = i
    theorem List.findIdx?_eq_some_of_exists {α : Type u_1} {xs : List α} {p : αBool} (h : ∃ (x : α), x xs p x = true) :
    theorem List.findIdx?_eq_none_iff_findIdx_eq {α : Type u_1} {xs : List α} {p : αBool} :
    List.findIdx? p xs = none List.findIdx p xs = xs.length
    theorem List.findIdx?_eq_guard_findIdx_lt {α : Type u_1} {xs : List α} {p : αBool} :
    List.findIdx? p xs = Option.guard (fun (i : Nat) => i < xs.length) (List.findIdx p xs)
    theorem List.findIdx?_eq_some_iff_getElem {α : Type u_1} {xs : List α} {p : αBool} {i : Nat} :
    List.findIdx? p xs = some i ∃ (h : i < xs.length), p xs[i] = true ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
    theorem List.findIdx?_of_eq_some {α : Type u_1} {i : Nat} {xs : List α} {p : αBool} (w : List.findIdx? p xs = some i) :
    match xs[i]? with | some a => p a = true | none => false = true
    theorem List.findIdx?_of_eq_none {α : Type u_1} {xs : List α} {p : αBool} (w : List.findIdx? p xs = none) (i : Nat) :
    match xs[i]? with | some a => ¬p a = true | none => true = true
    @[simp]
    theorem List.findIdx?_map {β : Type u_1} {α : Type u_2} {p : αBool} (f : βα) (l : List β) :
    @[simp]
    theorem List.findIdx?_append {α : Type u_1} {xs : List α} {ys : List α} {p : αBool} :
    List.findIdx? p (xs ++ ys) = (List.findIdx? p xs).or (Option.map (fun (i : Nat) => i + xs.length) (List.findIdx? p ys))
    theorem List.findIdx?_join {α : Type u_1} {l : List (List α)} {p : αBool} :
    List.findIdx? p l.join = Option.map (fun (i : Nat) => Nat.sum (List.map List.length (List.take i l)) + (Option.map (fun (xs : List α) => List.findIdx p xs) l[i]?).getD 0) (List.findIdx? (fun (x : List α) => x.any p) l)
    @[simp]
    theorem List.findIdx?_replicate {n : Nat} :
    ∀ {α : Type u_1} {a : α} {p : αBool}, List.findIdx? p (List.replicate n a) = if 0 < n p a = true then some 0 else none
    theorem List.findIdx?_eq_findSome?_enum {α : Type u_1} {xs : List α} {p : αBool} :
    List.findIdx? p xs = List.findSome? (fun (x : Nat × α) => match x with | (i, a) => if p a = true then some i else none) xs.enum
    theorem List.findIdx?_eq_fst_find?_enum {α : Type u_1} {xs : List α} {p : αBool} :
    List.findIdx? p xs = Option.map (fun (x : Nat × α) => x.fst) (List.find? (fun (x : Nat × α) => match x with | (fst, x) => p x) xs.enum)
    theorem List.findIdx?_eq_none_of_findIdx?_eq_none {α : Type u_1} {xs : List α} {p : αBool} {q : αBool} (w : ∀ (x : α), x xsp x = trueq x = true) :
    List.findIdx? q xs = noneList.findIdx? p xs = none
    theorem List.Sublist.findIdx?_isSome {α : Type u_1} {p : αBool} {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) :
    (List.findIdx? p l₁).isSome = true(List.findIdx? p l₂).isSome = true
    theorem List.Sublist.findIdx?_eq_none {α : Type u_1} {p : αBool} {l₁ : List α} {l₂ : List α} (h : l₁.Sublist l₂) :
    List.findIdx? p l₂ = noneList.findIdx? p l₁ = none
    theorem List.IsPrefix.findIdx?_eq_some {α : Type u_1} {i : Nat} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <+: l₂) :
    List.findIdx? p l₁ = some iList.findIdx? p l₂ = some i
    theorem List.IsPrefix.findIdx?_eq_none {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <+: l₂) :
    List.findIdx? p l₂ = noneList.findIdx? p l₁ = none
    theorem List.IsSuffix.findIdx?_eq_none {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <:+ l₂) :
    List.findIdx? p l₂ = noneList.findIdx? p l₁ = none
    theorem List.IsInfix.findIdx?_eq_none {α : Type u_1} {l₁ : List α} {l₂ : List α} {p : αBool} (h : l₁ <:+: l₂) :
    List.findIdx? p l₂ = noneList.findIdx? p l₁ = none

    indexOf #

    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

    lookup #

    @[simp]
    theorem List.lookup_cons_self {α : Type u_2} [BEq α] [LawfulBEq α] :
    ∀ {β : Type u_1} {b : β} {es : List (α × β)} {k : α}, List.lookup k ((k, b) :: es) = some b
    theorem List.lookup_eq_findSome? {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} (l : List (α × β)) (k : α) :
    List.lookup k l = List.findSome? (fun (p : α × β) => if (k == p.fst) = true then some p.snd else none) l
    @[simp]
    theorem List.lookup_eq_none_iff {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {l : List (α × β)} {k : α} :
    List.lookup k l = none ∀ (p : α × β), p l(k != p.fst) = true
    @[simp]
    theorem List.lookup_isSome_iff {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {l : List (α × β)} {k : α} :
    (List.lookup k l).isSome = true ∃ (p : α × β), p l (k == p.fst) = true
    theorem List.lookup_eq_some_iff {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {l : List (α × β)} {k : α} {b : β} :
    List.lookup k l = some b ∃ (l₁ : List (α × β)), ∃ (l₂ : List (α × β)), l = l₁ ++ (k, b) :: l₂ ∀ (p : α × β), p l₁(k != p.fst) = true
    theorem List.lookup_append {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {l₁ : List (α × β)} {l₂ : List (α × β)} {k : α} :
    List.lookup k (l₁ ++ l₂) = (List.lookup k l₁).or (List.lookup k l₂)
    theorem List.lookup_replicate {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} {a : α} :
    ∀ {α_1 : Type u_1} {b : α_1} {k : α}, List.lookup k (List.replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
    theorem List.lookup_replicate_of_pos {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} {a : α} :
    ∀ {α_1 : Type u_1} {b : α_1} {k : α}, 0 < nList.lookup k (List.replicate n (a, b)) = if (k == a) = true then some b else none
    theorem List.lookup_replicate_self {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} :
    ∀ {α_1 : Type u_1} {b : α_1} {a : α}, List.lookup a (List.replicate n (a, b)) = if n = 0 then none else some b
    @[simp]
    theorem List.lookup_replicate_self_of_pos {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} :
    ∀ {α_1 : Type u_1} {b : α_1} {a : α}, 0 < nList.lookup a (List.replicate n (a, b)) = some b
    @[simp]
    theorem List.lookup_replicate_ne {α : Type u_2} [BEq α] [LawfulBEq α] {a : α} {n : Nat} :
    ∀ {α_1 : Type u_1} {b : α_1} {k : α}, (!k == a) = trueList.lookup k (List.replicate n (a, b)) = none
    theorem List.Sublist.lookup_isSome {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ : List (α × β)} {l₂ : List (α × β)} (h : l₁.Sublist l₂) :
    (List.lookup k l₁).isSome = true(List.lookup k l₂).isSome = true
    theorem List.Sublist.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ : List (α × β)} {l₂ : List (α × β)} (h : l₁.Sublist l₂) :
    List.lookup k l₂ = noneList.lookup k l₁ = none
    theorem List.IsPrefix.lookup_eq_some {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {b : β} {l₁ : List (α × β)} {l₂ : List (α × β)} (h : l₁ <+: l₂) :
    List.lookup k l₁ = some bList.lookup k l₂ = some b
    theorem List.IsPrefix.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ : List (α × β)} {l₂ : List (α × β)} (h : l₁ <+: l₂) :
    List.lookup k l₂ = noneList.lookup k l₁ = none
    theorem List.IsSuffix.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ : List (α × β)} {l₂ : List (α × β)} (h : l₁ <:+ l₂) :
    List.lookup k l₂ = noneList.lookup k l₁ = none
    theorem List.IsInfix.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ : List (α × β)} {l₂ : List (α × β)} (h : l₁ <:+: l₂) :
    List.lookup k l₂ = noneList.lookup k l₁ = none