Lemmas about Vector.findSome?, Vector.find?, Vector.findFinIdx?.

We are still missing results about idxOf?, findIdx, and findIdx?.

findSome?

@[simp]

theorem Vector.findSome?_empty {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} : findSome? f { toArray := #[], size_toArray := ⋯ } = none

@[simp]

theorem Vector.findSome?_push {α : Type u_1} {n : Nat} {a : α} {α✝ : Type u_2} {f : α → Option α✝} {xs : Vector α n} : findSome? f (xs.push a) = (findSome? f xs).or (f a)

theorem Vector.findSome?_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : α → Option β} : findSome? f { toArray := #[a], size_toArray := ⋯ } = f a

@[simp]

theorem Vector.findSomeRev?_push_of_isSome {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : α → Option α✝} {a : α} {xs : Vector α n} {h : (f a).isSome = true} : findSomeRev? f (xs.push a) = f a

@[simp]

theorem Vector.findSomeRev?_push_of_isNone {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : α → Option α✝} {a : α} {xs : Vector α n} {h : (f a).isNone = true} : findSomeRev? f (xs.push a) = findSomeRev? f xs

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

@[simp]

theorem Vector.findSome?_eq_none_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} : findSome? f xs = none ↔ ∀ (x : α), x ∈ xs → f x = none

@[simp]

theorem Vector.findSome?_isSome_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} : (findSome? f xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ (f x).isSome = true

theorem Vector.findSome?_eq_some_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} {b : β} : findSome? f xs = some b ↔ ∃ (k₁ : Nat), ∃ (k₂ : Nat), ∃ (w : n = k₁ + 1 + k₂), ∃ (ys : Vector α k₁), ∃ (a : α), ∃ (zs : Vector α k₂), xs = Vector.cast ⋯ (ys.push a ++ zs) ∧ f a = some b ∧ ∀ (x : α), x ∈ ys → f x = none

@[simp]

theorem Vector.findSome?_guard {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} : findSome? (Option.guard fun (x : α) => p x) xs = find? p xs

theorem Vector.find?_eq_findSome?_guard {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} : find? p xs = findSome? (Option.guard fun (x : α) => p x) xs

@[simp]

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

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

theorem Vector.findSome?_append {α : Type u_1} {n₁ n₂ : Nat} {α✝ : Type u_2} {f : α → Option α✝} {xs : Vector α n₁} {ys : Vector α n₂} : findSome? f (xs ++ ys) = (findSome? f xs).or (findSome? f ys)

theorem Vector.getElem?_zero_flatten {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} : xss.flatten[0]? = findSome? (fun (xs : Vector α m) => xs[0]?) xss

theorem Vector.getElem_zero_flatten.proof {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} (h : 0 < n * m) : (findSome? (fun (xs : Vector α m) => xs[0]?) xss).isSome = true

theorem Vector.getElem_zero_flatten {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} (h : 0 < n * m) : xss.flatten[0] = (findSome? (fun (xs : Vector α m) => xs[0]?) xss).get ⋯

theorem Vector.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

@[reducible, inline, deprecated Vector.findSome?_replicate (since := "2025-03-18")]

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

Equations

• @Vector.findSome?_mkVector = @Vector.findSome?_replicate

@[simp]

theorem Vector.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

@[reducible, inline, deprecated Vector.findSome?_replicate_of_pos (since := "2025-03-18")]

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

Equations

• @Vector.findSome?_mkVector_of_pos = @Vector.findSome?_replicate_of_pos

@[simp]

theorem Vector.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

@[reducible, inline, deprecated Vector.findSome?_replicate_of_isSome (since := "2025-03-18")]

abbrev Vector.findSome?_mkVector_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

Equations

• @Vector.findSome?_mkVector_of_isSome = @Vector.findSome?_replicate_of_isSome

@[simp]

theorem Vector.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

@[reducible, inline, deprecated Vector.findSome?_replicate_of_isNone (since := "2025-03-18")]

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

Equations

• @Vector.findSome?_mkVector_of_isNone = @Vector.findSome?_replicate_of_isNone

find?

@[simp]

theorem Vector.find?_empty {α✝ : Type} {p : α✝ → Bool} : find? p { toArray := #[], size_toArray := ⋯ } = none

theorem Vector.find?_singleton {α : Type} {a : α} {p : α → Bool} : find? p { toArray := #[a], size_toArray := ⋯ } = if p a = true then some a else none

@[simp]

theorem Vector.findRev?_push_of_pos {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} (h : p a = true) : findRev? p (xs.push a) = some a

@[simp]

theorem Vector.findRev?_cons_of_neg {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} (h : ¬p a = true) : findRev? p (xs.push a) = findRev? p xs

@[simp]

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

theorem Vector.find?_eq_some_iff_append {α : Type} {n : Nat} {p : α → Bool} {b : α} {xs : Vector α n} : find? p xs = some b ↔ p b = true ∧ ∃ (k₁ : Nat), ∃ (k₂ : Nat), ∃ (w : n = k₁ + 1 + k₂), ∃ (as : Vector α k₁), ∃ (bs : Vector α k₂), xs = Vector.cast ⋯ (as.push b ++ bs) ∧ ∀ (a : α), a ∈ as → (!p a) = true

theorem Vector.find?_push {α : Type} {n : Nat} {a : α} {p : α → Bool} {xs : Vector α n} : find? p (xs.push a) = (find? p xs).or (if p a = true then some a else none)

@[simp]

theorem Vector.find?_push_eq_some {α : Type} {n : Nat} {a : α} {p : α → Bool} {b : α} {xs : Vector α n} : find? p (xs.push a) = some b ↔ find? p xs = some b ∨ find? p xs = none ∧ p a = true ∧ a = b

@[simp]

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

theorem Vector.find?_some {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} (h : find? p xs = some a) : p a = true

theorem Vector.mem_of_find?_eq_some {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} (h : find? p xs = some a) : a ∈ xs

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

@[simp]

theorem Vector.find?_map {β α : Type} {n : Nat} {p : α → Bool} {f : β → α} {xs : Vector β n} : find? p (map f xs) = Option.map f (find? (p ∘ f) xs)

@[simp]

theorem Vector.find?_append {α : Type} {n₁ n₂ : Nat} {p : α → Bool} {xs : Vector α n₁} {ys : Vector α n₂} : find? p (xs ++ ys) = (find? p xs).or (find? p ys)

@[simp]

theorem Vector.find?_flatten {α : Type} {m n : Nat} {xs : Vector (Vector α m) n} {p : α → Bool} : find? p xs.flatten = findSome? (fun (x : Vector α m) => find? p x) xs

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

@[simp]

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

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

theorem Vector.find?_replicate {α✝ : Type} {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

@[reducible, inline, deprecated Vector.find?_replicate (since := "2025-03-18")]

abbrev Vector.find?_mkVector {α✝ : Type} {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

Equations

• @Vector.find?_mkVector = @Vector.find?_replicate

@[simp]

theorem Vector.find?_replicate_of_size_pos {n : Nat} {α✝ : Type} {p : α✝ → Bool} {a : α✝} (h : 0 < n) : find? p (replicate n a) = if p a = true then some a else none

@[reducible, inline, deprecated Vector.find?_replicate_of_size_pos (since := "2025-03-18")]

abbrev Vector.find?_mkVector_of_length_pos {n : Nat} {α✝ : Type} {p : α✝ → Bool} {a : α✝} (h : 0 < n) : find? p (replicate n a) = if p a = true then some a else none

Equations

• @Vector.find?_mkVector_of_length_pos = @Vector.find?_replicate_of_size_pos

@[simp]

theorem Vector.find?_replicate_of_pos {α✝ : Type} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : p a = true) : find? p (replicate n a) = if n = 0 then none else some a

@[reducible, inline, deprecated Vector.find?_replicate_of_pos (since := "2025-03-18")]

abbrev Vector.find?_mkVector_of_pos {α✝ : Type} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : p a = true) : find? p (replicate n a) = if n = 0 then none else some a

Equations

• @Vector.find?_mkVector_of_pos = @Vector.find?_replicate_of_pos

@[simp]

theorem Vector.find?_replicate_of_neg {α✝ : Type} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) : find? p (replicate n a) = none

@[reducible, inline, deprecated Vector.find?_replicate_of_neg (since := "2025-03-18")]

abbrev Vector.find?_mkVector_of_neg {α✝ : Type} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) : find? p (replicate n a) = none

Equations

• @Vector.find?_mkVector_of_neg = @Vector.find?_replicate_of_neg

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

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

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

Equations

• @Vector.find?_mkVector_eq_none_iff = @Vector.find?_replicate_eq_none_iff

@[simp]

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

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

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

Equations

• @Vector.find?_mkVector_eq_some_iff = @Vector.find?_replicate_eq_some_iff

@[simp]

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

@[reducible, inline, deprecated Vector.get_find?_replicate (since := "2025-03-18")]

abbrev Vector.get_find?_mkVector {α : Type} {n : Nat} {a : α} {p : α → Bool} (h : (find? p (replicate n a)).isSome = true) : (find? p (replicate n a)).get h = a

Equations

• @Vector.get_find?_mkVector = @Vector.get_find?_replicate

theorem Vector.find?_pmap {α β : Type} {n : Nat} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (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)

theorem Vector.find?_eq_some_iff_getElem {α : Type} {n : Nat} {xs : Vector α n} {p : α → Bool} {b : α} : find? p xs = some b ↔ p b = true ∧ ∃ (i : Nat), ∃ (h : i < n), xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

findFinIdx?

theorem Vector.findFinIdx?_empty {α : Type u_1} {p : α → Bool} : findFinIdx? p { toArray := #[], size_toArray := ⋯ } = none

theorem Vector.findFinIdx?_singleton {α : Type u_1} {a : α} {p : α → Bool} : Array.findFinIdx? p #[a] = if p a = true then some ⟨0, ⋯⟩ else none

theorem Vector.findFinIdx?_congr {α : Type u_1} {n : Nat} {p : α → Bool} {xs ys : Vector α n} (w : xs = ys) : findFinIdx? p xs = findFinIdx? p ys

theorem Vector.findFinIdx?_push {α : Type u_1} {n : Nat} {xs : Vector α n} {a : α} {p : α → Bool} : findFinIdx? p (xs.push a) = (Option.map Fin.castSucc (findFinIdx? p xs)).or (if p a = true then some ⟨n, ⋯⟩ else none)

theorem Vector.findFinIdx?_append {α : Type u_1} {n₁ n₂ : Nat} {xs : Vector α n₁} {ys : Vector α n₂} {p : α → Bool} : findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (findFinIdx? p xs)).or (Option.map (Fin.natAdd n₁) (findFinIdx? p ys))

@[simp]

theorem Vector.isSome_findFinIdx? {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : (findFinIdx? p xs).isSome = xs.any p

@[simp]

theorem Vector.isNone_findFinIdx? {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} : (findFinIdx? p xs).isNone = xs.all fun (x : α) => decide ¬p x = true

@[simp]

theorem Vector.findFinIdx?_subtype {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findFinIdx? f xs = findFinIdx? g xs.unattach