Lemmas about List.findSome?, List.find?, List.findIdx, List.findIdx?, List.idxOf, and List.lookup.

findSome?

@[simp]

theorem List.findSome?_cons_of_isSome {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} (l : List α✝) (h : (f a).isSome = true) : findSome? f (a :: l) = f a

@[simp]

theorem List.findSome?_cons_of_isNone {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} (l : List α✝) (h : (f a).isNone = true) : findSome? f (a :: l) = findSome? f l

theorem List.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → Option β} (w : findSome? f l = some b) : ∃ (a : α), a ∈ l ∧ f a = some b

@[simp]

theorem List.findSome?_eq_none_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {p : α✝ → Option α✝¹} {l : List α✝} : findSome? p l = none ↔ ∀ (x : α✝), x ∈ l → p x = none

@[reducible, inline, deprecated List.findSome?_eq_none_iff (since := "2024-09-05")]

abbrev List.findSome?_eq_none {α✝ : Type u_1} {α✝¹ : Type u_2} {p : α✝ → Option α✝¹} {l : List α✝} : findSome? p l = none ↔ ∀ (x : α✝), x ∈ l → p x = none

Equations

• @List.findSome?_eq_none = @List.findSome?_eq_none_iff

@[simp]

theorem List.findSome?_isSome_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : 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 : β} : 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 α) : findSome? (Option.guard fun (x : α) => p x = true) l = find? p l

theorem List.find?_eq_findSome?_guard {α : Type u_1} {p : α → Bool} (l : List α) : find? p l = findSome? (Option.guard fun (x : α) => p x = true) l

@[simp]

theorem List.head?_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : (filterMap f l).head? = findSome? f l

@[simp]

theorem List.head_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) (h : filterMap f l ≠ []) : (filterMap f l).head h = (findSome? f l).get ⋯

@[simp]

theorem List.getLast?_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : (filterMap f l).getLast? = findSome? f l.reverse

@[simp]

theorem List.getLast_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) (h : filterMap f l ≠ []) : (filterMap f l).getLast h = (findSome? f l.reverse).get ⋯

@[simp]

theorem List.map_findSome? {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → γ) (l : List α) : Option.map g (findSome? f l) = findSome? (Option.map g ∘ f) l

theorem List.findSome?_map {β : Type u_1} {γ : Type u_2} {α✝ : Type u_3} {p : γ → Option α✝} (f : β → γ) (l : List β) : findSome? p (map f l) = findSome? (p ∘ f) l

theorem List.findSome?_append {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {l₁ l₂ : List α} : findSome? f (l₁ ++ l₂) = (findSome? f l₁).or (findSome? f l₂)

theorem List.head_flatten {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l ∈ L ∧ l ≠ []) : L.flatten.head ⋯ = (findSome? (fun (l : List α) => l.head?) L).get ⋯

theorem List.getLast_flatten {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l ∈ L ∧ l ≠ []) : L.flatten.getLast ⋯ = (findSome? (fun (l : List α) => l.getLast?) L.reverse).get ⋯

theorem List.findSome?_replicate {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} : findSome? f (replicate n a) = if n = 0 then none else f a

@[simp]

theorem List.findSome?_replicate_of_pos {n : Nat} {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} (h : 0 < n) : findSome? f (replicate n a) = f a

@[simp]

theorem List.findSome?_replicate_of_isSome {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} : (f a).isSome = true → findSome? f (replicate n a) = if n = 0 then none else f a

@[simp]

theorem List.findSome?_replicate_of_isNone {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} (h : (f a).isNone = true) : findSome? f (replicate n a) = none

theorem List.Sublist.findSome?_isSome {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : (findSome? f l₁).isSome = true → (findSome? f l₂).isSome = true

theorem List.Sublist.findSome?_eq_none {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : findSome? f l₂ = none → findSome? f l₁ = none

theorem List.IsPrefix.findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) : findSome? f l₁ = some b → findSome? f l₂ = some b

theorem List.IsPrefix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) : findSome? f l₂ = none → findSome? f l₁ = none

theorem List.IsSuffix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+ l₂) : findSome? f l₂ = none → findSome? f l₁ = none

theorem List.IsInfix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+: l₂) : findSome? f l₂ = none → findSome? f l₁ = none

find?

@[simp]

theorem List.find?_singleton {α : Type u_1} (a : α) (p : α → Bool) : 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 α✝) (h : p a = true) : find? p (a :: l) = some a

@[simp]

theorem List.find?_cons_of_neg {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (l : List α✝) (h : ¬p a = true) : find? p (a :: l) = find? p l

@[simp]

theorem List.find?_eq_none {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} : find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true

theorem List.find?_eq_some_iff_append {α✝ : Type u_1} {b : α✝} {p : α✝ → Bool} {xs : List α✝} : find? p xs = some b ↔ p b = true ∧ ∃ (as : List α✝), ∃ (bs : List α✝), xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

@[reducible, inline, deprecated List.find?_eq_some_iff_append (since := "2024-11-06")]

abbrev List.find?_eq_some {α✝ : Type u_1} {b : α✝} {p : α✝ → Bool} {xs : List α✝} : find? p xs = some b ↔ p b = true ∧ ∃ (as : List α✝), ∃ (bs : List α✝), xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

Equations

• @List.find?_eq_some = @List.find?_eq_some_iff_append

@[simp]

theorem List.find?_cons_eq_some {α✝ : Type u_1} {a : α✝} {xs : List α✝} {p : α✝ → Bool} {b : α✝} : find? p (a :: xs) = some b ↔ p a = true ∧ a = b ∨ (!p a) = true ∧ find? p xs = some b

@[simp]

theorem List.find?_isSome {α : Type u_1} {xs : List α} {p : α → Bool} : (find? p xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ p x = true

theorem List.find?_some {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {l : List α✝} : find? p l = some a → p a = true

theorem List.mem_of_find?_eq_some {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {l : List α✝} : find? p l = some a → a ∈ l

theorem List.get_find?_mem {α : Type u_1} (xs : List α) (p : α → Bool) (h : (find? p xs).isSome = true) : (find? p xs).get h ∈ xs

@[simp]

theorem List.find?_filter {α : Type u_1} (xs : List α) (p q : α → Bool) : find? q (filter p xs) = find? (fun (a : α) => decide (p a = true ∧ q a = true)) xs

@[simp]

theorem List.head?_filter {α : Type u_1} (p : α → Bool) (l : List α) : (filter p l).head? = find? p l

@[simp]

theorem List.head_filter {α : Type u_1} (p : α → Bool) (l : List α) (h : filter p l ≠ []) : (filter p l).head h = (find? p l).get ⋯

@[simp]

theorem List.getLast?_filter {α : Type u_1} (p : α → Bool) (l : List α) : (filter p l).getLast? = find? p l.reverse

@[simp]

theorem List.getLast_filter {α : Type u_1} (p : α → Bool) (l : List α) (h : filter p l ≠ []) : (filter p l).getLast h = (find? p l.reverse).get ⋯

@[simp]

theorem List.find?_filterMap {α : Type u_1} {β : Type u_2} (xs : List α) (f : α → Option β) (p : β → Bool) : find? p (filterMap f xs) = (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 β) : find? p (map f l) = Option.map f (find? (p ∘ f) l)

@[simp]

theorem List.find?_append {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} : find? p (l₁ ++ l₂) = (find? p l₁).or (find? p l₂)

@[simp]

theorem List.find?_flatten {α : Type u_1} (xs : List (List α)) (p : α → Bool) : find? p xs.flatten = findSome? (fun (x : List α) => find? p x) xs

theorem List.find?_flatten_eq_none_iff {α : Type u_1} {xs : List (List α)} {p : α → Bool} : find? p xs.flatten = none ↔ ∀ (ys : List α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

@[reducible, inline, deprecated List.find?_flatten_eq_none_iff (since := "2025-02-03")]

abbrev List.find?_flatten_eq_none {α : Type u_1} {xs : List (List α)} {p : α → Bool} : find? p xs.flatten = none ↔ ∀ (ys : List α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

Equations

• @List.find?_flatten_eq_none = @List.find?_flatten_eq_none_iff

theorem List.find?_flatten_eq_some_iff {α : Type u_1} {xs : List (List α)} {p : α → Bool} {a : α} : find? p xs.flatten = 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.flatten, 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.

@[reducible, inline, deprecated List.find?_flatten_eq_some_iff (since := "2025-02-03")]

abbrev List.find?_flatten_eq_some {α : Type u_1} {xs : List (List α)} {p : α → Bool} {a : α} : find? p xs.flatten = 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

Equations

• @List.find?_flatten_eq_some = @List.find?_flatten_eq_some_iff

@[simp]

theorem List.find?_flatMap {α : Type u_1} {β : Type u_2} (xs : List α) (f : α → List β) (p : β → Bool) : find? p (flatMap f xs) = findSome? (fun (x : α) => find? p (f x)) xs

@[reducible, inline, deprecated List.find?_flatMap (since := "2024-10-16")]

abbrev List.find?_bind {α : Type u_1} {β : Type u_2} (xs : List α) (f : α → List β) (p : β → Bool) : find? p (flatMap f xs) = findSome? (fun (x : α) => find? p (f x)) xs

Equations

• @List.find?_bind = @List.find?_flatMap

theorem List.find?_flatMap_eq_none_iff {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {p : β → Bool} : find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

@[reducible, inline, deprecated List.find?_flatMap_eq_none_iff (since := "2024-10-16")]

abbrev List.find?_flatMap_eq_none {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {p : β → Bool} : find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

Equations

• @List.find?_flatMap_eq_none = @List.find?_flatMap_eq_none_iff

@[reducible, inline, deprecated List.find?_flatMap_eq_none (since := "2024-10-16")]

abbrev List.find?_bind_eq_none {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {p : β → Bool} : find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

Equations

• @List.find?_bind_eq_none = @List.find?_flatMap_eq_none_iff

theorem List.find?_replicate {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} : find? p (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 : α✝} (h : 0 < n) : find? p (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 : α✝} (h : p a = true) : find? p (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 : α✝} (h : ¬p a = true) : find? p (replicate n a) = none

theorem List.find?_replicate_eq_none_iff {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} : find? p (replicate n a) = none ↔ n = 0 ∨ (!p a) = true

@[reducible, inline, deprecated List.find?_replicate_eq_none_iff (since := "2025-02-03")]

abbrev List.find?_replicate_eq_none {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} : find? p (replicate n a) = none ↔ n = 0 ∨ (!p a) = true

Equations

• @List.find?_replicate_eq_none = @List.find?_replicate_eq_none_iff

@[simp]

theorem List.find?_replicate_eq_some_iff {α : Type u_1} {n : Nat} {a b : α} {p : α → Bool} : find? p (replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

@[reducible, inline, deprecated List.find?_replicate_eq_some_iff (since := "2025-02-03")]

abbrev List.find?_replicate_eq_some {α : Type u_1} {n : Nat} {a b : α} {p : α → Bool} : find? p (replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

Equations

• @List.find?_replicate_eq_some = @List.find?_replicate_eq_some_iff

@[simp]

theorem List.get_find?_replicate {α : Type u_1} (n : Nat) (a : α) (p : α → Bool) (h : (find? p (replicate n a)).isSome = true) : (find? p (replicate n a)).get h = a

theorem List.Sublist.find?_isSome {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : (find? p l₁).isSome = true → (find? p l₂).isSome = true

theorem List.Sublist.find?_eq_none {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : find? p l₂ = none → find? p l₁ = none

theorem List.IsPrefix.find?_eq_some {α : Type u_1} {b : α} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : find? p l₁ = some b → find? p l₂ = some b

theorem List.IsPrefix.find?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : find? p l₂ = none → find? p l₁ = none

theorem List.IsSuffix.find?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) : find? p l₂ = none → find? p l₁ = none

theorem List.IsInfix.find?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) : find? p l₂ = none → 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 ∈ xs → P a) (p : β → Bool) : find? p (pmap f xs H) = Option.map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => f a ⋯) (find? (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => p (f a ⋯)) xs.attach)

findIdx? (preliminary lemmas)

@[simp]

theorem List.findIdx?_nil {α : Type u_1} {p : α → Bool} : findIdx? p [] = none

@[simp]

theorem List.findIdx?_cons {α✝ : Type u_1} {x : α✝} {xs : List α✝} {p : α✝ → Bool} : findIdx? p (x :: xs) = if p x = true then some 0 else Option.map (fun (i : Nat) => i + 1) (findIdx? p xs)

findFinIdx?

@[simp]

theorem List.findFinIdx?_nil {α : Type u_1} {p : α → Bool} : findFinIdx? p [] = none

@[irreducible]

theorem List.findIdx?_go_eq_map_findFinIdx?_go_val {α : Type u_1} {l xs : List α} {p : α → Bool} {i : Nat} {h : xs.length + i = l.length} : findIdx?.go p xs i = Option.map (fun (x : Fin l.length) => ↑x) (findFinIdx?.go p l xs i h)

theorem List.findIdx?_eq_map_findFinIdx?_val {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = Option.map (fun (x : Fin xs.length) => ↑x) (findFinIdx? p xs)

@[simp]

theorem List.findFinIdx?_cons {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : findFinIdx? p (x :: xs) = if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs)

@[simp]

theorem List.findFinIdx?_subtype {α : Type u_1} {p : α → Prop} {l : List { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findFinIdx? f l = Option.map (fun (i : Fin l.unattach.length) => Fin.cast ⋯ i) (findFinIdx? g l.unattach)

findIdx

theorem List.findIdx_cons {α : Type u_1} (p : α → Bool) (b : α) (l : List α) : findIdx p (b :: l) = bif p b then 0 else findIdx p l + 1

theorem List.findIdx_cons.findIdx_go_succ {α : Type u_1} (p : α → Bool) (l : List α) (n : Nat) : findIdx.go p l (n + 1) = findIdx.go p l n + 1

theorem List.findIdx_of_getElem?_eq_some {α : Type u_1} {p : α → Bool} {y : α} {xs : List α} (w : xs[findIdx p xs]? = some y) : p y = true

theorem List.findIdx_getElem {α : Type u_1} {p : α → Bool} {xs : List α} {w : findIdx p xs < xs.length} : p xs[findIdx p xs] = true

@[deprecated List.findIdx_of_getElem?_eq_some (since := "2024-08-12")]

theorem List.findIdx_of_get?_eq_some {α : Type u_1} {p : α → Bool} {y : α} {xs : List α} (w : xs.get? (findIdx p xs) = some y) : p y = true

@[deprecated List.findIdx_getElem (since := "2024-08-12")]

theorem List.findIdx_get {α : Type u_1} {p : α → Bool} {xs : List α} {w : findIdx p xs < xs.length} : p (xs.get ⟨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) : 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[findIdx p xs]? = some xs[findIdx p xs]

@[deprecated List.findIdx_getElem?_eq_getElem_of_exists (since := "2024-08-12")]

theorem List.findIdx_get?_eq_get_of_exists {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∃ (x : α), x ∈ xs ∧ p x = true) : xs.get? (findIdx p xs) = some (xs.get ⟨findIdx p xs, ⋯⟩)

@[simp]

theorem List.findIdx_eq_length {α : Type u_1} {p : α → Bool} {xs : List α} : findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false

theorem List.findIdx_eq_length_of_false {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∀ (x : α), x ∈ xs → p x = false) : findIdx p xs = xs.length

theorem List.findIdx_le_length {α : Type u_1} (p : α → Bool) {xs : List α} : findIdx p xs ≤ xs.length

@[simp]

theorem List.findIdx_lt_length {α : Type u_1} {p : α → Bool} {xs : 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 < 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) : i ≤ findIdx p xs

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[j] = true) : i < findIdx p xs

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) : 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₁ l₂ : List α) : findIdx p (l₁ ++ l₂) = if findIdx p l₁ < l₁.length then findIdx p l₁ else findIdx p l₂ + l₁.length

theorem List.IsPrefix.findIdx_le {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : findIdx p l₁ ≤ findIdx p l₂

theorem List.IsPrefix.findIdx_eq_of_findIdx_lt_length {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) (lt : findIdx p l₁ < l₁.length) : findIdx p l₂ = findIdx p l₁

theorem List.findIdx_le_findIdx {α : Type u_1} {l : List α} {p q : α → Bool} (h : ∀ (x : α), x ∈ l → p x = true → q x = true) : findIdx q l ≤ findIdx p l

@[simp]

theorem List.findIdx_subtype {α : Type u_1} {p : α → Prop} {l : List { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findIdx f l = findIdx g l.unattach

findIdx?

@[simp]

theorem List.findIdx?_eq_none_iff {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false

theorem List.findIdx?_isSome {α : Type u_1} {xs : List α} {p : α → Bool} : (findIdx? p xs).isSome = xs.any p

theorem List.findIdx?_isNone {α : Type u_1} {xs : List α} {p : α → Bool} : (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} : findIdx? p xs = some i ↔ i < xs.length ∧ 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) : findIdx? p xs = some (findIdx p xs)

theorem List.findIdx?_eq_none_iff_findIdx_eq {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = none ↔ findIdx p xs = xs.length

theorem List.findIdx?_eq_guard_findIdx_lt {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = Option.guard (fun (i : Nat) => i < xs.length) (findIdx p xs)

theorem List.findIdx?_eq_some_iff_getElem {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} : findIdx? p xs = some i ↔ ∃ (h : i < xs.length), p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true

theorem List.of_findIdx?_eq_some {α : Type u_1} {i : Nat} {xs : List α} {p : α → Bool} (w : findIdx? p xs = some i) : match xs[i]? with | some a => p a = true | none => false = true

@[reducible, inline, deprecated List.of_findIdx?_eq_some (since := "2025-02-02")]

abbrev List.findIdx?_of_eq_some {α : Type u_1} {i : Nat} {xs : List α} {p : α → Bool} (w : findIdx? p xs = some i) : match xs[i]? with | some a => p a = true | none => false = true

Equations

• @List.findIdx?_of_eq_some = @List.of_findIdx?_eq_some

theorem List.of_findIdx?_eq_none {α : Type u_1} {xs : List α} {p : α → Bool} (w : findIdx? p xs = none) (i : Nat) : match xs[i]? with | some a => ¬p a = true | none => true = true

@[reducible, inline, deprecated List.of_findIdx?_eq_none (since := "2025-02-02")]

abbrev List.findIdx?_of_eq_none {α : Type u_1} {xs : List α} {p : α → Bool} (w : findIdx? p xs = none) (i : Nat) : match xs[i]? with | some a => ¬p a = true | none => true = true

Equations

• @List.findIdx?_of_eq_none = @List.of_findIdx?_eq_none

@[simp]

theorem List.findIdx?_map {β : Type u_1} {α : Type u_2} {p : α → Bool} (f : β → α) (l : List β) : findIdx? p (map f l) = findIdx? (p ∘ f) l

@[simp]

theorem List.findIdx?_append {α : Type u_1} {xs ys : List α} {p : α → Bool} : findIdx? p (xs ++ ys) = (findIdx? p xs).or (Option.map (fun (i : Nat) => i + xs.length) (findIdx? p ys))

theorem List.findIdx?_flatten {α : Type u_1} {l : List (List α)} {p : α → Bool} : findIdx? p l.flatten = Option.map (fun (i : Nat) => (map length (take i l)).sum + (Option.map (fun (xs : List α) => findIdx p xs) l[i]?).getD 0) (findIdx? (fun (x : List α) => x.any p) l)

@[simp]

theorem List.findIdx?_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {p : α✝ → Bool} : findIdx? p (replicate n a) = if 0 < n ∧ p a = true then some 0 else none

theorem List.findIdx?_eq_findSome?_zipIdx {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = findSome? (fun (x : α × Nat) => match x with | (a, i) => if p a = true then some i else none) xs.zipIdx

theorem List.findIdx?_eq_fst_find?_zipIdx {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = Option.map (fun (x : α × Nat) => x.snd) (find? (fun (x : α × Nat) => match x with | (x, snd) => p x) xs.zipIdx)

theorem List.findIdx?_eq_none_of_findIdx?_eq_none {α : Type u_1} {xs : List α} {p q : α → Bool} (w : ∀ (x : α), x ∈ xs → p x = true → q x = true) : findIdx? q xs = none → findIdx? p xs = none

theorem List.Sublist.findIdx?_isSome {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : (findIdx? p l₁).isSome = true → (findIdx? p l₂).isSome = true

theorem List.Sublist.findIdx?_eq_none {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.IsPrefix.findIdx?_eq_some {α : Type u_1} {i : Nat} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : findIdx? p l₁ = some i → findIdx? p l₂ = some i

theorem List.IsPrefix.findIdx?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.IsSuffix.findIdx?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.IsInfix.findIdx?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.findIdx_eq_getD_findIdx? {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx p xs = (findIdx? p xs).getD xs.length

@[simp]

theorem List.findIdx?_subtype {α : Type u_1} {p : α → Prop} {l : List { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findIdx? f l = findIdx? g l.unattach

idxOf

The verification API for idxOf is still incomplete. The lemmas below should be made consistent with those for findIdx (and proved using them).

theorem List.idxOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] : idxOf y (x :: xs) = bif x == y then 0 else idxOf y xs + 1

@[reducible, inline, deprecated List.idxOf_cons (since := "2025-01-29")]

abbrev List.indexOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] : idxOf y (x :: xs) = bif x == y then 0 else idxOf y xs + 1

Equations

• @List.indexOf_cons = @List.idxOf_cons

@[simp]

theorem List.idxOf_cons_self {α : Type u_1} {a : α} [BEq α] [ReflBEq α] {l : List α} : idxOf a (a :: l) = 0

@[reducible, inline, deprecated List.idxOf_cons_self (since := "2025-01-29")]

abbrev List.indexOf_cons_self {α : Type u_1} {a : α} [BEq α] [ReflBEq α] {l : List α} : idxOf a (a :: l) = 0

Equations

• @List.indexOf_cons_self = @List.idxOf_cons_self

theorem List.idxOf_append {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} : idxOf a (l₁ ++ l₂) = if a ∈ l₁ then idxOf a l₁ else idxOf a l₂ + l₁.length

@[reducible, inline, deprecated List.idxOf_append (since := "2025-01-29")]

abbrev List.indexOf_append {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} : idxOf a (l₁ ++ l₂) = if a ∈ l₁ then idxOf a l₁ else idxOf a l₂ + l₁.length

Equations

• @List.indexOf_append = @List.idxOf_append

theorem List.idxOf_eq_length {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} (h : ¬a ∈ l) : idxOf a l = l.length

@[reducible, inline, deprecated List.idxOf_eq_length (since := "2025-01-29")]

abbrev List.indexOf_eq_length {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} (h : ¬a ∈ l) : idxOf a l = l.length

Equations

• @List.indexOf_eq_length = @List.idxOf_eq_length

theorem List.idxOf_lt_length {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} (h : a ∈ l) : idxOf a l < l.length

@[reducible, inline, deprecated List.idxOf_lt_length (since := "2025-01-29")]

abbrev List.indexOf_lt_length {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} (h : a ∈ l) : idxOf a l < l.length

Equations

• @List.indexOf_lt_length = @List.idxOf_lt_length

idxOf?

The verification API for idxOf? is still incomplete. The lemmas below should be made consistent with those for findIdx? (and proved using them).

@[simp]

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

theorem List.idxOf?_cons {α : Type u_1} [BEq α] (a : α) (xs : List α) (b : α) : idxOf? b (a :: xs) = if (a == b) = true then some 0 else Option.map (fun (x : Nat) => x + 1) (idxOf? b xs)

@[simp]

theorem List.idxOf?_eq_none_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : idxOf? a l = none ↔ ¬a ∈ l

@[reducible, inline, deprecated List.idxOf?_eq_none_iff (since := "2025-01-29")]

abbrev List.indexOf?_eq_none_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : idxOf? a l = none ↔ ¬a ∈ l

Equations

• @List.indexOf?_eq_none_iff = @List.idxOf?_eq_none_iff

finIdxOf?

theorem List.idxOf?_eq_map_finIdxOf?_val {α : Type u_1} [BEq α] {xs : List α} {a : α} : idxOf? a xs = Option.map (fun (x : Fin xs.length) => ↑x) (finIdxOf? a xs)

lookup

@[simp]

theorem List.lookup_cons_self {α : Type u_2} [BEq α] [LawfulBEq α] {β✝ : Type u_1} {b : β✝} {es : List (α × β✝)} {k : α} : lookup k ((k, b) :: es) = some b

theorem List.lookup_eq_findSome? {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} (l : List (α × β)) (k : α) : lookup k l = 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 : α} : 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 : α} : (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 : β} : 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₁ l₂ : List (α × β)} {k : α} : lookup k (l₁ ++ l₂) = (lookup k l₁).or (lookup k l₂)

theorem List.lookup_replicate {α : Type u_2} [BEq α] [LawfulBEq α] {n : Nat} {a : α} {α✝ : Type u_1} {b : α✝} {k : α} : lookup k (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 : α} {α✝ : Type u_1} {b : α✝} {k : α} (h : 0 < n) : lookup k (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} {α✝ : Type u_1} {b : α✝} {a : α} : lookup a (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} {α✝ : Type u_1} {b : α✝} {a : α} (h : 0 < n) : lookup a (replicate n (a, b)) = some b

@[simp]

theorem List.lookup_replicate_ne {α : Type u_2} [BEq α] [LawfulBEq α] {a : α} {n : Nat} {α✝ : Type u_1} {b : α✝} {k : α} (h : (!k == a) = true) : lookup k (replicate n (a, b)) = none

theorem List.Sublist.lookup_isSome {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁.Sublist l₂) : (lookup k l₁).isSome = true → (lookup k l₂).isSome = true

theorem List.Sublist.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁.Sublist l₂) : lookup k l₂ = none → lookup k l₁ = none

theorem List.IsPrefix.lookup_eq_some {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {b : β} {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) : lookup k l₁ = some b → lookup k l₂ = some b

theorem List.IsPrefix.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) : lookup k l₂ = none → lookup k l₁ = none

theorem List.IsSuffix.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁ <:+ l₂) : lookup k l₂ = none → lookup k l₁ = none

theorem List.IsInfix.lookup_eq_none {α : Type u_2} [BEq α] [LawfulBEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂) : lookup k l₂ = none → lookup k l₁ = none

Deprecations

@[reducible, inline, deprecated List.head_flatten (since := "2024-10-14")]

abbrev List.head_join {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l ∈ L ∧ l ≠ []) : L.flatten.head ⋯ = (findSome? (fun (l : List α) => l.head?) L).get ⋯

Equations

• @List.head_join = @List.head_flatten

@[reducible, inline, deprecated List.getLast_flatten (since := "2024-10-14")]

abbrev List.getLast_join {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l ∈ L ∧ l ≠ []) : L.flatten.getLast ⋯ = (findSome? (fun (l : List α) => l.getLast?) L.reverse).get ⋯

Equations

• @List.getLast_join = @List.getLast_flatten

@[reducible, inline, deprecated List.find?_flatten (since := "2024-10-14")]

abbrev List.find?_join {α : Type u_1} (xs : List (List α)) (p : α → Bool) : find? p xs.flatten = findSome? (fun (x : List α) => find? p x) xs

Equations

• @List.find?_join = @List.find?_flatten

@[reducible, inline, deprecated List.find?_flatten_eq_none (since := "2024-10-14")]

abbrev List.find?_join_eq_none {α : Type u_1} {xs : List (List α)} {p : α → Bool} : find? p xs.flatten = none ↔ ∀ (ys : List α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

Equations

• @List.find?_join_eq_none = @List.find?_flatten_eq_none_iff

@[reducible, inline, deprecated List.find?_flatten_eq_some (since := "2024-10-14")]

abbrev List.find?_join_eq_some {α : Type u_1} {xs : List (List α)} {p : α → Bool} {a : α} : find? p xs.flatten = 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

Equations

• @List.find?_join_eq_some = @List.find?_flatten_eq_some_iff

@[reducible, inline, deprecated List.findIdx?_flatten (since := "2024-10-14")]

abbrev List.findIdx?_join {α : Type u_1} {l : List (List α)} {p : α → Bool} : findIdx? p l.flatten = Option.map (fun (i : Nat) => (map length (take i l)).sum + (Option.map (fun (xs : List α) => findIdx p xs) l[i]?).getD 0) (findIdx? (fun (x : List α) => x.any p) l)

Equations

• @List.findIdx?_join = @List.findIdx?_flatten