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

find?

@[simp]

theorem List.find?_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), p a = true → List.find? p (a :: l) = some a

@[simp]

theorem List.find?_cons_of_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), ¬p a = true → List.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?_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → p a = true

@[simp]

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

@[simp]

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

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 < n → List.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 = true → List.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 = true → List.find? p (List.replicate n a) = none

theorem List.find?_isSome_of_sublist {α : 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

findSome?

@[simp]

theorem List.findSome?_cons_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} (l : List α), (f a).isSome = true → List.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 = true → List.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?_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?_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 < n → List.findSome? f (List.replicate n a) = f a

@[simp]

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

@[simp]

theorem List.find?_replicate_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α}, (f a).isNone = true → List.findSome? f (List.replicate n a) = none

theorem List.findSome?_isSome_of_sublist {α : 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

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_get?_eq_some {α : Type u_1} {p : α → Bool} {y : α} {xs : List α} (w : xs.get? (List.findIdx p xs) = some y) : p y = true

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_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, ⋯⟩)

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)

@[simp]

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)

theorem List.findIdx?_eq_some_iff {α : Type u_1} {i : Nat} (xs : List α) (p : α → Bool) : List.findIdx? p xs = some i ↔ List.map p (List.take (i + 1) xs) = List.replicate i false ++ [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.get? 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.get? i with | some a => ¬p a = true | none => true = true

@[simp]

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

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

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