diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index 297637c8cf..1ad501b248 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -642,14 +642,28 @@ and simplifies these to the function directly taking the value.
   rw [List.filterMap_subtype]
   simp [hf]
 
+@[simp] theorem findSome?_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findSome? f = l.unattach.findSome? g := by
+  cases l
+  simp
+  rw [List.findSome?_subtype hf]
+
+@[simp] theorem find?_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    (l.find? f).map Subtype.val = l.unattach.find? g := by
+  cases l
+  simp
+  rw [List.find?_subtype hf]
+
+/-! ### Simp lemmas pushing `unattach` inwards. -/
+
 @[simp] theorem unattach_filter {p : α → Prop} {l : Array { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (l.filter f).unattach = l.unattach.filter g := by
   cases l
   simp [hf]
 
-/-! ### Simp lemmas pushing `unattach` inwards. -/
-
 @[simp] theorem unattach_reverse {p : α → Prop} {l : Array { x // p x }} :
     l.reverse.unattach = l.unattach.reverse := by
   cases l
diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean
index 4838ad6408..d618c794e8 100644
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -4,12 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 prelude
-import Init.Data.List.Find
+import Init.Data.List.Nat.Find
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
+import Init.Data.Array.Range
 
 /-!
-# Lemmas about `Array.findSome?`, `Array.find?`.
+# Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.
 -/
 
 namespace Array
@@ -48,6 +49,9 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : Array α} {b : β} :
 @[simp] theorem findSome?_guard (l : Array α) : findSome? (Option.guard fun x => p x) l = find? p l := by
   cases l; simp
 
+theorem find?_eq_findSome?_guard (l : Array α) : find? p l = findSome? (Option.guard fun x => p x) l :=
+  (findSome?_guard l).symm
+
 @[simp] theorem getElem?_zero_filterMap (f : α → Option β) (l : Array α) : (l.filterMap f)[0]? = l.findSome? f := by
   cases l; simp [← List.head?_eq_getElem?]
 
@@ -206,22 +210,25 @@ theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
   cases xs using array₂_induction
   simp [List.findSome?_map, Function.comp_def]
 
-theorem find?_flatten_eq_none {xs : Array (Array α)} {p : α → Bool} :
+theorem find?_flatten_eq_none_iff {xs : Array (Array α)} {p : α → Bool} :
     xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
+@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
+
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
 Moreover, no earlier array in `xs` has an element satisfying `p`.
 -/
-theorem find?_flatten_eq_some {xs : Array (Array α)} {p : α → Bool} {a : α} :
+theorem find?_flatten_eq_some_iff {xs : Array (Array α)} {p : α → Bool} {a : α} :
     xs.flatten.find? p = some a ↔
       p a ∧ ∃ (as : Array (Array α)) (ys zs : Array α) (bs : Array (Array α)),
         xs = as.push (ys.push a ++ zs) ++ bs ∧
         (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
   cases xs using array₂_induction
-  simp only [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some]
+  simp only [flatten_toArray_map_toArray, List.find?_toArray, List.find?_flatten_eq_some_iff]
   simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
   intro w
   constructor
@@ -235,15 +242,21 @@ theorem find?_flatten_eq_some {xs : Array (Array α)} {p : α → Bool} {a : α}
       ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
         by simpa using h₁, by simpa using h₂⟩
 
+@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
+
 @[simp] theorem find?_flatMap (xs : Array α) (f : α → Array β) (p : β → Bool) :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
   simp [List.find?_flatMap, Array.flatMap_toArray]
 
-theorem find?_flatMap_eq_none {xs : Array α} {f : α → Array β} {p : β → Bool} :
+theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
+
 theorem find?_mkArray :
     find? p (mkArray n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
@@ -260,14 +273,20 @@ theorem find?_mkArray :
   simp [find?_mkArray, h]
 
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
-theorem find?_mkArray_eq_none {n : Nat} {a : α} {p : α → Bool} :
+theorem find?_mkArray_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (mkArray n a).find? p = none ↔ n = 0 ∨ !p a := by
-  simp [← List.toArray_replicate, List.find?_replicate_eq_none, Classical.or_iff_not_imp_left]
+  simp [← List.toArray_replicate, List.find?_replicate_eq_none_iff, Classical.or_iff_not_imp_left]
 
-@[simp] theorem find?_mkArray_eq_some {n : Nat} {a b : α} {p : α → Bool} :
+@[deprecated find?_mkArray_eq_none_iff (since := "2025-02-03")]
+abbrev find?_mkArray_eq_none := @find?_mkArray_eq_none_iff
+
+@[simp] theorem find?_mkArray_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (mkArray n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
+@[deprecated find?_mkArray_eq_some_iff (since := "2025-02-03")]
+abbrev find?_mkArray_eq_some := @find?_mkArray_eq_some_iff
+
 @[simp] theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
     ((mkArray n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
@@ -278,4 +297,275 @@ theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array 
   simp only [pmap_eq_map_attach, find?_map]
   rfl
 
+theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
+    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j] := by
+  rcases xs with ⟨xs⟩
+  simp [List.find?_eq_some_iff_getElem]
+
+/-! ### findFinIdx? -/
+
+@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := rfl
+
+-- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
+theorem findFinIdx?_congr {p : α → Bool} {l₁ : Array α} {l₂ : Array α} (w : l₁ = l₂) :
+    findFinIdx? p l₁ = (findFinIdx? p l₂).map (fun i => i.cast (by simp [w])) := by
+  subst w
+  simp
+
+@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
+  cases l
+  simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
+  rw [findFinIdx?_congr List.unattach_toArray]
+  simp [Function.comp_def]
+
+/-! ### findIdx -/
+
+theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
+  rcases xs with ⟨xs⟩
+  exact List.findIdx_of_getElem?_eq_some (by simpa using w)
+
+theorem findIdx_getElem {xs : Array α} {w : xs.findIdx p < xs.size} :
+    p xs[xs.findIdx p] :=
+  xs.findIdx_of_getElem?_eq_some (getElem?_eq_getElem w)
+
+theorem findIdx_lt_size_of_exists {xs : Array α} (h : ∃ x ∈ xs, p x) :
+    xs.findIdx p < xs.size := by
+  rcases xs with ⟨xs⟩
+  simpa using List.findIdx_lt_length_of_exists (by simpa using h)
+
+theorem findIdx_getElem?_eq_getElem_of_exists {xs : Array α} (h : ∃ x ∈ xs, p x) :
+    xs[xs.findIdx p]? = some (xs[xs.findIdx p]'(xs.findIdx_lt_size_of_exists h)) :=
+  getElem?_eq_getElem (findIdx_lt_size_of_exists h)
+
+@[simp]
+theorem findIdx_eq_size {p : α → Bool} {xs : Array α} :
+    xs.findIdx p = xs.size ↔ ∀ x ∈ xs, p x = false := by
+  rcases xs with ⟨xs⟩
+  simp
+
+theorem findIdx_eq_size_of_false {p : α → Bool} {xs : Array α} (h : ∀ x ∈ xs, p x = false) :
+    xs.findIdx p = xs.size := by
+  rcases xs with ⟨xs⟩
+  simp_all
+
+theorem findIdx_le_size (p : α → Bool) {xs : Array α} : xs.findIdx p ≤ xs.size := by
+  by_cases e : ∃ x ∈ xs, p x
+  · exact Nat.le_of_lt (findIdx_lt_size_of_exists e)
+  · simp at e
+    exact Nat.le_of_eq (findIdx_eq_size.mpr e)
+
+@[simp]
+theorem findIdx_lt_size {p : α → Bool} {xs : Array α} :
+    xs.findIdx p < xs.size ↔ ∃ x ∈ xs, p x := by
+  rcases xs with ⟨xs⟩
+  simp
+
+/-- `p` does not hold for elements with indices less than `xs.findIdx p`. -/
+theorem not_of_lt_findIdx {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.findIdx p) :
+    p (xs[i]'(Nat.le_trans h (findIdx_le_size p))) = false := by
+  rcases xs with ⟨xs⟩
+  simpa using List.not_of_lt_findIdx (by simpa using h)
+
+/-- If `¬ p xs[j]` for all `j < i`, then `i ≤ xs.findIdx p`. -/
+theorem le_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size)
+    (h2 : ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false) : i ≤ xs.findIdx p := by
+  apply Decidable.byContradiction
+  intro f
+  simp only [Nat.not_le] at f
+  exact absurd (@findIdx_getElem _ p xs (Nat.lt_trans f h)) (by simpa using h2 (xs.findIdx p) f)
+
+/-- If `¬ p xs[j]` for all `j ≤ i`, then `i < xs.findIdx p`. -/
+theorem lt_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size)
+    (h2 : ∀ j (hji : j ≤ i), ¬p (xs[j]'(Nat.lt_of_le_of_lt hji h))) : i < xs.findIdx p := by
+  apply Decidable.byContradiction
+  intro f
+  simp only [Nat.not_lt] at f
+  exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)
+
+/-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/
+theorem findIdx_eq {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
+    xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by
+  refine ⟨fun f ↦ ⟨f ▸ (@findIdx_getElem _ p xs (f ▸ h)), fun _ hji ↦ not_of_lt_findIdx (f ▸ hji)⟩,
+    fun ⟨_, h2⟩ ↦ ?_⟩
+  apply Nat.le_antisymm _ (le_findIdx_of_not h h2)
+  apply Decidable.byContradiction
+  intro h3
+  simp at h3
+  simp_all [not_of_lt_findIdx h3]
+
+theorem findIdx_append (p : α → Bool) (l₁ l₂ : Array α) :
+    (l₁ ++ l₂).findIdx p =
+      if l₁.findIdx p < l₁.size then l₁.findIdx p else l₂.findIdx p + l₁.size := by
+  rcases l₁ with ⟨l₁⟩
+  rcases l₂ with ⟨l₂⟩
+  simp [List.findIdx_append]
+
+theorem findIdx_le_findIdx {l : Array α} {p q : α → Bool} (h : ∀ x ∈ l, p x → q x) : l.findIdx q ≤ l.findIdx p := by
+  rcases l with ⟨l⟩
+  simp_all [List.findIdx_le_findIdx]
+
+@[simp] theorem findIdx_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findIdx f = l.unattach.findIdx g := by
+  cases l
+  simp [hf]
+
+/-! ### findIdx? -/
+
+@[simp] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := rfl
+
+@[simp]
+theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
+    xs.findIdx? p = none ↔ ∀ x, x ∈ xs → p x = false := by
+  rcases xs with ⟨xs⟩
+  simp
+
+theorem findIdx?_isSome {xs : Array α} {p : α → Bool} :
+    (xs.findIdx? p).isSome = xs.any p := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_isSome]
+
+theorem findIdx?_isNone {xs : Array α} {p : α → Bool} :
+    (xs.findIdx? p).isNone = xs.all (¬p ·) := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_isNone]
+
+theorem findIdx?_eq_some_iff_findIdx_eq {xs : Array α} {p : α → Bool} {i : Nat} :
+    xs.findIdx? p = some i ↔ i < xs.size ∧ xs.findIdx p = i := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_eq_some_iff_findIdx_eq]
+
+theorem findIdx?_eq_some_of_exists {xs : Array α} {p : α → Bool} (h : ∃ x, x ∈ xs ∧ p x) :
+    xs.findIdx? p = some (xs.findIdx p) := by
+  rw [findIdx?_eq_some_iff_findIdx_eq]
+  exact ⟨findIdx_lt_size_of_exists h, rfl⟩
+
+theorem findIdx?_eq_none_iff_findIdx_eq {xs : Array α} {p : α → Bool} :
+    xs.findIdx? p = none ↔ xs.findIdx p = xs.size := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_eq_none_iff_findIdx_eq]
+
+theorem findIdx?_eq_guard_findIdx_lt {xs : Array α} {p : α → Bool} :
+    xs.findIdx? p = Option.guard (fun i => i < xs.size) (xs.findIdx p) := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_eq_guard_findIdx_lt]
+
+theorem findIdx?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {i : Nat} :
+    xs.findIdx? p = some i ↔
+      ∃ h : i < xs.size, p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji h)) := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_eq_some_iff_getElem]
+
+theorem of_findIdx?_eq_some {xs : Array α} {p : α → Bool} (w : xs.findIdx? p = some i) :
+    match xs[i]? with | some a => p a | none => false := by
+  rcases xs with ⟨xs⟩
+  simpa using List.of_findIdx?_eq_some (by simpa using w)
+
+theorem of_findIdx?_eq_none {xs : Array α} {p : α → Bool} (w : xs.findIdx? p = none) :
+    ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true := by
+  rcases xs with ⟨xs⟩
+  simpa using List.of_findIdx?_eq_none (by simpa using w)
+
+@[simp] theorem findIdx?_map (f : β → α) (l : Array β) : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
+  rcases l with ⟨l⟩
+  simp [List.findIdx?_map]
+
+@[simp] theorem findIdx?_append :
+    (xs ++ ys : Array α).findIdx? p =
+      (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.size) := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp [List.findIdx?_append]
+
+theorem findIdx?_flatten {l : Array (Array α)} {p : α → Bool} :
+    l.flatten.findIdx? p =
+      (l.findIdx? (·.any p)).map
+        fun i => ((l.take i).map Array.size).sum +
+          (l[i]?.map fun xs => xs.findIdx p).getD 0 := by
+  cases l using array₂_induction
+  simp [List.findIdx?_flatten, Function.comp_def]
+
+@[simp] theorem findIdx?_mkArray :
+    (mkArray n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
+  rw [← List.toArray_replicate]
+  simp only [List.findIdx?_toArray]
+  simp
+
+theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α → Bool} :
+    xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_eq_findSome?_zipIdx]
+
+theorem findIdx?_eq_fst_find?_zipIdx {xs : Array α} {p : α → Bool} :
+    xs.findIdx? p = (xs.zipIdx.find? fun ⟨x, _⟩ => p x).map (·.2) := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_eq_fst_find?_zipIdx]
+
+-- See also `findIdx_le_findIdx`.
+theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : Array α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) :
+    xs.findIdx? q = none → xs.findIdx? p = none := by
+  rcases xs with ⟨xs⟩
+  simpa using List.findIdx?_eq_none_of_findIdx?_eq_none (by simpa using w)
+
+theorem findIdx_eq_getD_findIdx? {xs : Array α} {p : α → Bool} :
+    xs.findIdx p = (xs.findIdx? p).getD xs.size := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx_eq_getD_findIdx?]
+
+theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
+    (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j := by
+  rcases xs with ⟨xs⟩
+  simp [List.findIdx?_eq_some_le_of_findIdx?_eq_some (by simpa using w) (by simpa using h)]
+
+@[simp] theorem findIdx?_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findIdx? f = l.unattach.findIdx? g := by
+  cases l
+  simp [hf]
+
+/-! ### 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 idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : Array α} {a : α} :
+    (l₁ ++ l₂).idxOf a = if a ∈ l₁ then l₁.idxOf a else l₂.idxOf a + l₁.size := by
+  rw [idxOf, findIdx_append]
+  split <;> rename_i h
+  · rw [if_pos]
+    simpa using h
+  · rw [if_neg]
+    simpa using h
+
+theorem idxOf_eq_size [BEq α] [LawfulBEq α] {l : Array α} (h : a ∉ l) : l.idxOf a = l.size := by
+  rcases l with ⟨l⟩
+  simp [List.idxOf_eq_length (by simpa using h)]
+
+theorem idxOf_lt_length [BEq α] [LawfulBEq α] {l : Array α} (h : a ∈ l) : l.idxOf a < l.size := by
+  rcases l with ⟨l⟩
+  simp [List.idxOf_lt_length (by simpa using h)]
+
+
+/-! ### 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 idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := rfl
+
+@[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : Array α} {a : α} :
+    l.idxOf? a = none ↔ a ∉ l := by
+  rcases l with ⟨l⟩
+  simp [List.idxOf?_eq_none_iff]
+
+/-! ### finIdxOf? -/
+
+theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
+    xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
+  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
+
 end Array
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index f55af4793a..6e71c8efd9 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -3621,6 +3621,16 @@ theorem eraseIdx_eq_eraseIdxIfInBounds {a : Array α} {i : Nat} (h : i < a.size)
   cases as
   simp
 
+@[simp] theorem finIdxOf?_toList [BEq α] (a : α) (v : Array α) :
+    v.toList.finIdxOf? a = (v.finIdxOf? a).map (Fin.cast (by simp)) := by
+  rcases v with ⟨v⟩
+  simp
+
+@[simp] theorem findFinIdx?_toList (p : α → Bool) (v : Array α) :
+    v.toList.findFinIdx? p = (v.findFinIdx? p).map (Fin.cast (by simp)) := by
+  rcases v with ⟨v⟩
+  simp
+
 end Array
 
 open Array
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 23d9618993..1ea9144131 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -374,6 +374,8 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
+@[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
+
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
   Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
 
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 1a52badee3..09aa2224ca 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -740,6 +740,24 @@ and simplifies these to the function directly taking the value.
 
 @[deprecated flatMap_subtype (since := "2024-10-16")] abbrev bind_subtype := @flatMap_subtype
 
+@[simp] theorem findSome?_subtype {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findSome? f = l.unattach.findSome? g := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih => simp [ih, hf, findSome?_cons]
+
+@[simp] theorem find?_subtype {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    (l.find? f).map Subtype.val = l.unattach.find? g := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [hf, find?_cons]
+    split <;> simp [ih]
+
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 3f275c5360..050b9edb59 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -8,9 +8,10 @@ prelude
 import Init.Data.List.Lemmas
 import Init.Data.List.Sublist
 import Init.Data.List.Range
+import Init.Data.Fin.Lemmas
 
 /-!
-Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `List.indexOf`,
+Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `List.idxOf`,
 and `List.lookup`.
 -/
 
@@ -96,6 +97,9 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
     · simp only [Option.guard_eq_none] at h
       simp [ih, h]
 
+theorem find?_eq_findSome?_guard (l : List α) : find? p l = findSome? (Option.guard fun x => p x) l :=
+  (findSome?_guard l).symm
+
 @[simp] theorem head?_filterMap (f : α → Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f := by
   induction l with
   | nil => simp
@@ -339,16 +343,19 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
     simp only [flatten_cons, find?_append, findSome?_cons, ih]
     split <;> simp [*]
 
-theorem find?_flatten_eq_none {xs : List (List α)} {p : α → Bool} :
+theorem find?_flatten_eq_none_iff {xs : List (List α)} {p : α → Bool} :
     xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
+@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
+
 /--
 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`.
 -/
-theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
+theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a : α} :
     xs.flatten.find? p = some a ↔
       p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧
         (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
@@ -383,17 +390,23 @@ theorem find?_flatten_eq_some {xs : List (List α)} {p : α → Bool} {a : α} :
     · exact h₁ l ml a m
     · exact h₂ a m
 
+@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
+
 @[simp] theorem find?_flatMap (xs : List α) (f : α → List β) (p : β → Bool) :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [flatMap_def, findSome?_map]; rfl
 
 @[deprecated find?_flatMap (since := "2024-10-16")] abbrev find?_bind := @find?_flatMap
 
-theorem find?_flatMap_eq_none {xs : List α} {f : α → List β} {p : β → Bool} :
+theorem find?_flatMap_eq_none_iff {xs : List α} {f : α → List β} {p : β → Bool} :
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-@[deprecated find?_flatMap_eq_none (since := "2024-10-16")] abbrev find?_bind_eq_none := @find?_flatMap_eq_none
+@[deprecated find?_flatMap_eq_none_iff (since := "2024-10-16")]
+abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
+
+@[deprecated find?_flatMap_eq_none (since := "2024-10-16")] abbrev find?_bind_eq_none := @find?_flatMap_eq_none_iff
 
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
@@ -410,14 +423,20 @@ theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p
   simp [find?_replicate, h]
 
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
-theorem find?_replicate_eq_none {n : Nat} {a : α} {p : α → Bool} :
+theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [Classical.or_iff_not_imp_left]
 
-@[simp] theorem find?_replicate_eq_some {n : Nat} {a b : α} {p : α → Bool} :
+@[deprecated find?_replicate_eq_none_iff (since := "2025-02-03")]
+abbrev find?_replicate_eq_none := @find?_replicate_eq_none_iff
+
+@[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   cases n <;> simp
 
+@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
+abbrev find?_replicate_eq_some := @find?_replicate_eq_some_iff
+
 @[simp] theorem get_find?_replicate (n : Nat) (a : α) (p : α → Bool) (h) : ((replicate n a).find? p).get h = a := by
   cases n with
   | zero => simp at h
@@ -459,6 +478,79 @@ theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α
   simp only [pmap_eq_map_attach, find?_map]
   rfl
 
+/-! ### findIdx? (preliminary lemmas) -/
+
+@[local simp] private theorem findIdx?_go_nil {p : α → Bool} {i : Nat} :
+    findIdx?.go p [] i = none := rfl
+
+@[local simp] private theorem findIdx?_go_cons :
+    findIdx?.go p (x :: xs) i = if p x then some i else findIdx?.go p xs (i + 1) := rfl
+
+private theorem findIdx?_go_succ {p : α → Bool} {xs : List α} {i : Nat} :
+    findIdx?.go p xs (i+1) = (findIdx?.go p xs i).map fun i => i + 1 := by
+  induction xs generalizing i with simp
+  | cons _ _ _ => split <;> simp_all
+
+private theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
+    findIdx?.go p xs (i+1) = (findIdx?.go p xs 0).map fun k => k + (i + 1) := by
+  induction xs generalizing i with
+  | nil => simp
+  | cons _ _ _ =>
+    simp only [findIdx?_go_succ, findIdx?_go_cons, Nat.zero_add]
+    split
+    · simp_all
+    · simp_all only [findIdx?_go_succ, Bool.not_eq_true, Option.map_map, Nat.zero_add]
+      congr
+      ext
+      simp only [Nat.add_comm i, Function.comp_apply, Nat.add_assoc]
+
+@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p = none := rfl
+
+@[simp] theorem findIdx?_cons :
+    (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1 := by
+  simp [findIdx?, findIdx?_go_eq]
+
+/-! ### findFinIdx? -/
+
+@[simp] theorem findFinIdx?_nil {p : α → Bool} : findFinIdx? p [] = none := rfl
+
+theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
+    List.findIdx?.go p xs i =
+      (List.findFinIdx?.go p l xs i h).map (·.val) := by
+  unfold findIdx?.go
+  unfold findFinIdx?.go
+  split <;> rename_i a xs
+  · simp_all
+  · simp only
+    split
+    · simp
+    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
+theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
+  simp [findIdx?, findFinIdx?]
+  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
+@[simp] theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
+    findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ := by
+  rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]
+  rw [← findIdx?_eq_map_findFinIdx?_val]
+  rw [findIdx?_cons]
+  split
+  · simp
+  · rw [findIdx?_eq_map_findFinIdx?_val]
+    simp [Function.comp_def]
+
+@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [hf, findFinIdx?_cons]
+    split <;> simp [ih, Function.comp_def]
+
 /-! ### findIdx -/
 
 theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) :
@@ -580,7 +672,7 @@ theorem le_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
 
 /-- If `¬ p xs[j]` for all `j ≤ i`, then `i < xs.findIdx p`. -/
 theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length)
-    (h2 : ∀ j (hji : j ≤ i), ¬p (xs.get ⟨j, Nat.lt_of_le_of_lt hji h⟩)) : i < xs.findIdx p := by
+    (h2 : ∀ j (hji : j ≤ i), ¬p (xs[j]'(Nat.lt_of_le_of_lt hji h))) : i < xs.findIdx p := by
   apply Decidable.byContradiction
   intro f
   simp only [Nat.not_lt] at f
@@ -639,37 +731,16 @@ theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p
       · simp only [Nat.add_le_add_iff_right]
         exact ih fun _ m w => h _ (mem_cons_of_mem x m) w
 
-/-! ### findIdx? -/
-
-@[local simp] private theorem findIdx?_go_nil {p : α → Bool} {i : Nat} :
-    findIdx?.go p [] i = none := rfl
-
-@[local simp] private theorem findIdx?_go_cons :
-    findIdx?.go p (x :: xs) i = if p x then some i else findIdx?.go p xs (i + 1) := rfl
-
-private theorem findIdx?_go_succ {p : α → Bool} {xs : List α} {i : Nat} :
-    findIdx?.go p xs (i+1) = (findIdx?.go p xs i).map fun i => i + 1 := by
-  induction xs generalizing i with simp
-  | cons _ _ _ => split <;> simp_all
-
-private theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
-    findIdx?.go p xs (i+1) = (findIdx?.go p xs 0).map fun k => k + (i + 1) := by
-  induction xs generalizing i with
+@[simp] theorem findIdx_subtype {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findIdx f = l.unattach.findIdx g := by
+  unfold unattach
+  induction l with
   | nil => simp
-  | cons _ _ _ =>
-    simp only [findIdx?_go_succ, findIdx?_go_cons, Nat.zero_add]
-    split
-    · simp_all
-    · simp_all only [findIdx?_go_succ, Bool.not_eq_true, Option.map_map, Nat.zero_add]
-      congr
-      ext
-      simp only [Nat.add_comm i, Function.comp_apply, Nat.add_assoc]
+  | cons a l ih =>
+    simp [ih, hf, findIdx_cons]
 
-@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p = none := rfl
-
-@[simp] theorem findIdx?_cons :
-    (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1 := by
-  simp [findIdx?, findIdx?_go_eq]
+/-! ### findIdx? -/
 
 @[simp]
 theorem findIdx?_eq_none_iff {xs : List α} {p : α → Bool} :
@@ -764,7 +835,7 @@ theorem findIdx?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {i : Nat}
           refine ⟨i, ⟨Nat.succ_lt_succ_iff.mp h, by simpa, fun j hj => ?_⟩, rfl⟩
           simpa using h₂ (j + 1) (Nat.succ_lt_succ_iff.mpr hj)
 
-theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p = some i) :
+theorem of_findIdx?_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p = some i) :
     match xs[i]? with | some a => p a | none => false := by
   induction xs generalizing i with
   | nil => simp_all
@@ -772,7 +843,10 @@ theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p
     simp_all only [findIdx?_cons, Nat.zero_add]
     split at w <;> cases i <;> simp_all [succ_inj']
 
-theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
+@[deprecated of_findIdx?_eq_some (since := "2025-02-02")]
+abbrev findIdx?_of_eq_some := @of_findIdx?_eq_some
+
+theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
     ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true := by
   intro i
   induction xs generalizing i with
@@ -787,6 +861,9 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
       apply ih
       split at w <;> simp_all
 
+@[deprecated of_findIdx?_eq_none (since := "2025-02-02")]
+abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none
+
 @[simp] theorem findIdx?_map (f : β → α) (l : List β) : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
   induction l with
   | nil => simp
@@ -894,24 +971,15 @@ theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
     simp only [findIdx_cons, findIdx?_cons]
     split <;> simp_all [ih]
 
-/-! ### findFinIdx? -/
-
-theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
-    List.findIdx?.go p xs i =
-      (List.findFinIdx?.go p l xs i h).map (·.val) := by
-  unfold findIdx?.go
-  unfold findFinIdx?.go
-  split <;> rename_i a xs
-  · simp_all
-  · simp only
-    split
-    · simp
-    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
-
-theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
-  simp [findIdx?, findFinIdx?]
-  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+@[simp] theorem findIdx?_subtype {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findIdx? f = l.unattach.findIdx? g := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [hf, findIdx?_cons]
+    split <;> simp [ih, Function.comp_def]
 
 /-! ### idxOf
 
@@ -1101,8 +1169,8 @@ end lookup
 @[deprecated head_flatten (since := "2024-10-14")] abbrev head_join := @head_flatten
 @[deprecated getLast_flatten (since := "2024-10-14")] abbrev getLast_join := @getLast_flatten
 @[deprecated find?_flatten (since := "2024-10-14")] abbrev find?_join := @find?_flatten
-@[deprecated find?_flatten_eq_none (since := "2024-10-14")] abbrev find?_join_eq_none := @find?_flatten_eq_none
-@[deprecated find?_flatten_eq_some (since := "2024-10-14")] abbrev find?_join_eq_some := @find?_flatten_eq_some
+@[deprecated find?_flatten_eq_none (since := "2024-10-14")] abbrev find?_join_eq_none := @find?_flatten_eq_none_iff
+@[deprecated find?_flatten_eq_some (since := "2024-10-14")] abbrev find?_join_eq_some := @find?_flatten_eq_some_iff
 @[deprecated findIdx?_flatten (since := "2024-10-14")] abbrev findIdx?_join := @findIdx?_flatten
 
 end List
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 335ecb9dca..4a87969b88 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -94,6 +94,9 @@ theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l
       _ = drop (m + n) l := drop_drop n m l
       _ = drop ((m + 1) + n) (a :: l) := by rw [Nat.add_right_comm]; rfl
 
+theorem drop_add_one_eq_tail_drop (l : List α) : l.drop (i + 1) = (l.drop i).tail := by
+  rw [← drop_drop, drop_one]
+
 theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (take (m + n) l)
   | 0, _, _ => by simp
   | _, _, [] => by simp
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index c4a9a52dbb..c620ef6fe5 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -235,6 +235,87 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
     simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
     by_cases f a <;> simp_all
 
+private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :
+    Array.findFinIdx?.loop p l.toArray j = List.findFinIdx?.go p l l' j h := by
+  unfold findFinIdx?.loop
+  unfold findFinIdx?.go
+  split <;> rename_i h'
+  · cases l' with
+    | nil =>
+      simp at h h'
+      omega
+    | cons a l' =>
+      have : l[j] = a := by
+        rw [drop_eq_getElem_cons] at w
+        simp only [cons.injEq] at w
+        exact w.1.symm
+      simp only [getElem_toArray, this]
+      split
+      · rfl
+      · simp only [length_cons] at h
+        have : l.length - (j + 1) < l.length - j := by omega
+        rw [findFinIdx?_loop_toArray]
+        rw [drop_add_one_eq_tail_drop, ← w, tail_cons]
+  · have : l' = [] := by simp_all
+    subst this
+    simp
+termination_by l.length - j
+
+@[simp] theorem findFinIdx?_toArray (p : α → Bool) (l : List α) :
+    l.toArray.findFinIdx? p = l.findFinIdx? p := by
+  rw [Array.findFinIdx?, findFinIdx?, findFinIdx?_loop_toArray]
+  simp
+
+@[simp] theorem findIdx?_toArray (p : α → Bool) (l : List α) :
+    l.toArray.findIdx? p = l.findIdx? p := by
+  rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val]
+  simp
+
+private theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w : l' = l.drop j) (h) :
+    l.toArray.idxOfAux a j = findFinIdx?.go (fun x => x == a) l l' j h := by
+  unfold idxOfAux
+  unfold findFinIdx?.go
+  split <;> rename_i h'
+  · cases l' with
+    | nil =>
+      simp at h h'
+      omega
+    | cons b l' =>
+      simp at h'
+      have : l[j] = b := by
+        rw [drop_eq_getElem_cons h'] at w
+        simp only [cons.injEq] at w
+        exact w.1.symm
+      simp only [getElem_toArray, this]
+      split
+      · rfl
+      · simp only [length_cons] at h
+        have : l.length - (j + 1) < l.length - j := by omega
+        rw [idxAuxOf_toArray]
+        rw [drop_add_one_eq_tail_drop, ← w, tail_cons]
+  · have : l' = [] := by simp_all
+    subst this
+    simp
+termination_by l.length - j
+
+@[simp] theorem finIdxOf?_toArray [BEq α] (a : α) (l : List α) :
+    l.toArray.finIdxOf? a = l.finIdxOf? a := by
+  rw [Array.finIdxOf?, finIdxOf?, findFinIdx?]
+  simp [idxAuxOf_toArray]
+
+@[simp] theorem idxOf?_toArray [BEq α] (a : α) (l : List α) :
+    l.toArray.idxOf? a = l.idxOf? a := by
+  rw [Array.idxOf?, idxOf?]
+  simp [finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
+
+@[simp] theorem findIdx_toArray {as : List α} {p : α → Bool} :
+    as.toArray.findIdx p = as.findIdx p := by
+  rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?]
+
+@[simp] theorem idxOf_toArray [BEq α] {as : List α} {a : α} :
+    as.toArray.idxOf a = as.idxOf a := by
+  rw [Array.idxOf, findIdx_toArray, idxOf]
+
 theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
     Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
       Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
@@ -463,84 +544,6 @@ decreasing_by
   · simp
   · simp_all [eraseIdx_eq_self.2]
 
-@[simp] theorem findIdx?_toArray {as : List α} {p : α → Bool} :
-    as.toArray.findIdx? p = as.findIdx? p := by
-  unfold Array.findIdx?
-  suffices ∀ i, i ≤ as.length →
-      Array.findIdx?.loop p as.toArray (as.length - i) =
-        (findIdx? p (as.drop  (as.length - i))).map fun j => j +  (as.length - i) by
-    specialize this as.length
-    simpa
-  intro i
-  induction i with
-  | zero => simp [findIdx?.loop]
-  | succ i ih =>
-    unfold findIdx?.loop
-    simp only [size_toArray, getElem_toArray]
-    split <;> rename_i h
-    · rw [drop_eq_getElem_cons h]
-      rw [findIdx?_cons]
-      split <;> rename_i h'
-      · simp
-      · intro w
-        have : as.length - (i + 1) + 1 = as.length - i := by omega
-        specialize ih (by omega)
-        simp only [Option.map_map, this, ih]
-        congr
-        ext
-        simp
-        omega
-    · have : as.length = 0 := by omega
-      simp_all
-
-@[simp] theorem findFinIdx?_toArray {as : List α} {p : α → Bool} :
-    as.toArray.findFinIdx? p = as.findFinIdx? p := by
-  have h := findIdx?_toArray (as := as) (p := p)
-  rw [findIdx?_eq_map_findFinIdx?_val, Array.findIdx?_eq_map_findFinIdx?_val] at h
-  rwa [Option.map_inj_right] at h
-  rintro ⟨x, hx⟩ ⟨y, hy⟩ rfl
-  simp
-
-theorem findFinIdx?_go_beq_eq_idxOfAux_toArray [BEq α]
-    {xs as : List α} {a : α} {i : Nat} {h} (w : as = xs.drop i) :
-    findFinIdx?.go (fun x => x == a) xs as i h =
-      xs.toArray.idxOfAux a i := by
-  unfold findFinIdx?.go
-  unfold idxOfAux
-  split <;> rename_i b as
-  · simp at h
-    simp [h]
-  · simp at h
-    rw [dif_pos (by simp; omega)]
-    simp only [getElem_toArray]
-    erw [getElem_drop' (j := 0)]
-    simp only [← w, getElem_cons_zero]
-    have : xs.length - (i + 1) < xs.length - i := by omega
-    rw [findFinIdx?_go_beq_eq_idxOfAux_toArray]
-    rw [← drop_drop, ← w]
-    simp
-termination_by xs.length - i
-
-@[simp] theorem finIdxOf?_toArray [BEq α] {as : List α} {a : α} :
-    as.toArray.finIdxOf? a = as.finIdxOf? a := by
-  unfold Array.finIdxOf?
-  unfold finIdxOf?
-  unfold findFinIdx?
-  rw [findFinIdx?_go_beq_eq_idxOfAux_toArray]
-  simp
-
-@[simp] theorem findIdx_toArray [BEq α] {as : List α} {p : α → Bool} :
-    as.toArray.findIdx p = as.findIdx p := by
-  rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?]
-
-@[simp] theorem idxOf?_toArray [BEq α] {as : List α} {a : α} :
-    as.toArray.idxOf? a = as.idxOf? a := by
-  rw [Array.idxOf?, finIdxOf?_toArray, idxOf?_eq_map_finIdxOf?_val]
-
-@[simp] theorem idxOf_toArray [BEq α] {as : List α} {a : α} :
-    as.toArray.idxOf a = as.idxOf a := by
-  rw [Array.idxOf, findIdx_toArray, idxOf]
-
 @[simp] theorem eraseP_toArray {as : List α} {p : α → Bool} :
     as.toArray.eraseP p = (as.eraseP p).toArray := by
   rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray]
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 5c0fbbe5b3..5385069817 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -497,7 +497,7 @@ and simplifies these to the function directly taking the value.
     (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
     l.foldl f x = l.unattach.foldl g x := by
   rcases l with ⟨l, rfl⟩
-  simp [Array.foldl_subtype (hf := hf)]
+  simp [Array.foldl_subtype hf]
 
 /--
 This lemma identifies folds over arrays of subtypes, where the function only depends on the value, not the proposition,
@@ -508,7 +508,7 @@ and simplifies these to the function directly taking the value.
     (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
     l.foldr f x = l.unattach.foldr g x := by
   rcases l with ⟨l, rfl⟩
-  simp [Array.foldr_subtype (hf := hf)]
+  simp [Array.foldr_subtype hf]
 
 /--
 This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
@@ -518,7 +518,21 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → β} {g : α → β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.map f = l.unattach.map g := by
   rcases l with ⟨l, rfl⟩
-  simp [Array.map_subtype (hf := hf)]
+  simp [Array.map_subtype hf]
+
+@[simp] theorem findSome?_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findSome? f = l.unattach.findSome? g := by
+  rcases l with ⟨l, rfl⟩
+  simp
+  rw [Array.findSome?_subtype hf]
+
+@[simp] theorem find?_subtype {p : α → Prop} {l : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    (l.find? f).map Subtype.val = l.unattach.find? g := by
+  rcases l with ⟨l, rfl⟩
+  simp
+  rw [Array.find?_subtype hf]
 
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index de8b96e91d..128c30e131 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -371,7 +371,7 @@ abbrev indexOf? := @finIdxOf?
 
 /-- Finds the first index of a given value in a vector using a predicate. Returns `none` if the
 no element of the index matches the given value. -/
-@[inline] def findFinIdx? (v : Vector α n) (p : α → Bool) : Option (Fin n) :=
+@[inline] def findFinIdx? (p : α → Bool) (v : Vector α n) : Option (Fin n) :=
   (v.toArray.findFinIdx? p).map (Fin.cast v.size_toArray)
 
 /--
@@ -384,6 +384,28 @@ to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 @[inline] def findSomeM? [Monad m] (f : α → m (Option β)) (as : Vector α n) : m (Option β) :=
   as.toArray.findSomeM? f
 
+/--
+Note that the universe level is contrained to `Type` here,
+to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
+-/
+@[inline] def findRevM? {α : Type} {m : Type → Type} [Monad m] (f : α → m Bool) (as : Vector α n) : m (Option α) :=
+  as.toArray.findRevM? f
+
+@[inline] def findSomeRevM? [Monad m] (f : α → m (Option β)) (as : Vector α n) : m (Option β) :=
+  as.toArray.findSomeRevM? f
+
+@[inline] def find? {α : Type} (f : α → Bool) (as : Vector α n) : Option α :=
+  as.toArray.find? f
+
+@[inline] def findRev? {α : Type} (f : α → Bool) (as : Vector α n) : Option α :=
+  as.toArray.findRev? f
+
+@[inline] def findSome? (f : α → Option β) (as : Vector α n) : Option β :=
+  as.toArray.findSome? f
+
+@[inline] def findSomeRev? (f : α → Option β) (as : Vector α n) : Option β :=
+  as.toArray.findSomeRev? f
+
 /-- Returns `true` when `v` is a prefix of the vector `w`. -/
 @[inline] def isPrefixOf [BEq α] (v : Vector α m) (w : Vector α n) : Bool :=
   v.toArray.isPrefixOf w.toArray
diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean
new file mode 100644
index 0000000000..aa58dbbb0e
--- /dev/null
+++ b/src/Init/Data/Vector/Find.lean
@@ -0,0 +1,262 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Vector.Lemmas
+import Init.Data.Vector.Attach
+import Init.Data.Vector.Range
+import Init.Data.Array.Find
+
+/-!
+# Lemmas about `Vector.findSome?`, `Vector.find?, `Vector.findIdx?`, `Vector.idxOf?`.
+-/
+
+namespace Vector
+
+open Nat
+
+/-! ### findSome? -/
+
+@[simp] theorem findSomeRev?_push_of_isSome (l : Vector α n) (h : (f a).isSome) : (l.push a).findSomeRev? f = f a := by
+  rcases l with ⟨l, rfl⟩
+  simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isSome, h]
+
+@[simp] theorem findSomeRev?_push_of_isNone (l : Vector α n) (h : (f a).isNone) : (l.push a).findSomeRev? f = l.findSomeRev? f := by
+  rcases l with ⟨l, rfl⟩
+  simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isNone, h]
+
+theorem exists_of_findSome?_eq_some {f : α → Option β} {l : Vector α n} (w : l.findSome? f = some b) :
+    ∃ a, a ∈ l ∧ f a = b := by
+  rcases l with ⟨l, rfl⟩
+  simpa using Array.exists_of_findSome?_eq_some (by simpa using w)
+
+@[simp] theorem findSome?_eq_none_iff {f : α → Option β} {l : Vector α n} :
+    findSome? f l = none ↔ ∀ x ∈ l, f x = none := by
+  cases l; simp
+
+@[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : Vector α n} :
+    (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
+  cases l; simp
+
+theorem findSome?_eq_some_iff {f : α → Option β} {l : Vector α n} {b : β} :
+    l.findSome? f = some b ↔
+      ∃ (k₁ k₂ : Nat) (w : n = k₁ + 1 + k₂) (l₁ : Vector α k₁) (a : α) (l₂ : Vector α k₂),
+        l = (l₁.push a ++ l₂).cast w.symm ∧ f a = some b ∧ ∀ x ∈ l₁, f x = none := by
+  rcases l with ⟨l, rfl⟩
+  simp only [findSome?_mk, mk_eq]
+  rw [Array.findSome?_eq_some_iff]
+  constructor
+  · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
+    exact ⟨l₁.size, l₂.size, by simp, ⟨l₁, rfl⟩, a, ⟨l₂, rfl⟩, by simp, h₁, by simpa using h₂⟩
+  · rintro ⟨k₁, k₂, h, l₁, a, l₂, w, h₁, h₂⟩
+    exact ⟨l₁.toArray, a, l₂.toArray, by simp [w], h₁, by simpa using h₂⟩
+
+@[simp] theorem findSome?_guard (l : Vector α n) : findSome? (Option.guard fun x => p x) l = find? p l := by
+  cases l; simp
+
+theorem find?_eq_findSome?_guard (l : Vector α n) : find? p l = findSome? (Option.guard fun x => p x) l :=
+  (findSome?_guard l).symm
+
+@[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (l : Vector α n) :
+    (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
+  cases l; simp
+
+theorem findSome?_map (f : β → γ) (l : Vector β n) : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.findSome?_map]
+
+theorem findSome?_append {l₁ : Vector α n₁} {l₂ : Vector α n₂} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f) := by
+  cases l₁; cases l₂; simp [Array.findSome?_append]
+
+theorem getElem?_zero_flatten (L : Vector (Vector α m) n) :
+    (flatten L)[0]? = L.findSome? fun l => l[0]? := by
+  cases L using vector₂_induction
+  simp [Array.getElem?_zero_flatten, Array.findSome?_map, Function.comp_def]
+
+theorem getElem_zero_flatten.proof {L : Vector (Vector α m) n} (h : 0 < n * m) :
+    (L.findSome? fun l => l[0]?).isSome := by
+  cases L using vector₂_induction with
+  | of xss h₁ h₂ =>
+    have hn : 0 < n := Nat.pos_of_mul_pos_right h
+    have hm : 0 < m := Nat.pos_of_mul_pos_left h
+    simp only [hm, getElem?_eq_getElem, findSome?_mk, Array.findSome?_isSome_iff, Array.mem_map,
+      Array.mem_attach, mk_eq, true_and, Subtype.exists, exists_prop, exists_eq_right,
+      Option.isSome_some, and_true]
+    exact ⟨⟨xss[0], h₂ _ (by simp)⟩, by simp⟩
+
+theorem getElem_zero_flatten {L : Vector (Vector α m) n} (h : 0 < n * m) :
+    (flatten L)[0] = (L.findSome? fun l => l[0]?).get (getElem_zero_flatten.proof h) := by
+  have t := getElem?_zero_flatten L
+  simp [getElem?_eq_getElem, h] at t
+  simp [← t]
+
+theorem findSome?_mkVector : findSome? f (mkVector n a) = if n = 0 then none else f a := by
+  rw [mkVector_eq_mk_mkArray, findSome?_mk, Array.findSome?_mkArray]
+
+@[simp] theorem findSome?_mkVector_of_pos (h : 0 < n) : findSome? f (mkVector n a) = f a := by
+  simp [findSome?_mkVector, Nat.ne_of_gt h]
+
+-- Argument is unused, but used to decide whether `simp` should unfold.
+@[simp] theorem findSome?_mkVector_of_isSome (_ : (f a).isSome) :
+   findSome? f (mkVector n a) = if n = 0 then none else f a := by
+  simp [findSome?_mkVector]
+
+@[simp] theorem findSome?_mkVector_of_isNone (h : (f a).isNone) :
+    findSome? f (mkVector n a) = none := by
+  rw [Option.isNone_iff_eq_none] at h
+  simp [findSome?_mkVector, h]
+
+/-! ### find? -/
+
+@[simp] theorem find?_singleton (a : α) (p : α → Bool) :
+    #v[a].find? p = if p a then some a else none := by
+  simp
+
+@[simp] theorem findRev?_push_of_pos (l : Vector α n) (h : p a) :
+    findRev? p (l.push a) = some a := by
+  cases l; simp [h]
+
+@[simp] theorem findRev?_cons_of_neg (l : Vector α n) (h : ¬p a) :
+    findRev? p (l.push a) = findRev? p l := by
+  cases l; simp [h]
+
+@[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
+  cases l; simp
+
+theorem find?_eq_some_iff_append {xs : Vector α n} :
+    xs.find? p = some b ↔
+      p b ∧ ∃ (k₁ k₂ : Nat) (w : n = k₁ + 1 + k₂) (as : Vector α k₁) (bs : Vector α k₂),
+        xs = (as.push b ++ bs).cast w.symm ∧ ∀ a ∈ as, !p a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [find?_mk, Array.find?_eq_some_iff_append,
+    mk_eq, toArray_cast, toArray_append, toArray_push]
+  constructor
+  · rintro ⟨h, as, bs, rfl, w⟩
+    exact ⟨h, as.size, bs.size, by simp, ⟨as, rfl⟩, ⟨bs, rfl⟩, by simp, by simpa using w⟩
+  · rintro ⟨h, k₁, k₂, w, as, bs, h', w'⟩
+    exact ⟨h, as.toArray, bs.toArray, by simp [h'], by simpa using w'⟩
+
+@[simp]
+theorem find?_push_eq_some {xs : Vector α n} :
+    (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
+  cases xs; simp
+
+@[simp] theorem find?_isSome {xs : Vector α n} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
+  cases xs; simp
+
+theorem find?_some {xs : Vector α n} (h : find? p xs = some a) : p a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp at h
+  exact Array.find?_some h
+
+theorem mem_of_find?_eq_some {xs : Vector α n} (h : find? p xs = some a) : a ∈ xs := by
+  cases xs
+  simp at h
+  simpa using Array.mem_of_find?_eq_some h
+
+theorem get_find?_mem {xs : Vector α n} (h) : (xs.find? p).get h ∈ xs := by
+  cases xs
+  simp [Array.get_find?_mem]
+
+@[simp] theorem find?_filter {xs : Vector α n} (p q : α → Bool) :
+    (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
+  cases xs; simp
+
+@[simp] theorem getElem?_zero_filter (p : α → Bool) (l : Vector α n) :
+    (l.filter p)[0]? = l.find? p := by
+  cases l; simp [← List.head?_eq_getElem?]
+
+@[simp] theorem getElem_zero_filter (p : α → Bool) (l : Vector α n) (h) :
+    (l.filter p)[0] =
+      (l.find? p).get (by cases l; simpa [← Array.countP_eq_size_filter] using h) := by
+  cases l
+  simp [List.getElem_zero_eq_head]
+
+@[simp] theorem find?_map (f : β → α) (xs : Vector β n) :
+    find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
+  cases xs; simp
+
+@[simp] theorem find?_append {l₁ : Vector α n₁} {l₂ : Vector α n₂} :
+    (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p) := by
+  cases l₁
+  cases l₂
+  simp
+
+@[simp] theorem find?_flatten (xs : Vector (Vector α m) n) (p : α → Bool) :
+    xs.flatten.find? p = xs.findSome? (·.find? p) := by
+  cases xs using vector₂_induction
+  simp [Array.findSome?_map, Function.comp_def]
+
+theorem find?_flatten_eq_none_iff {xs : Vector (Vector α m) n} {p : α → Bool} :
+    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
+  simp
+
+@[simp] theorem find?_flatMap (xs : Vector α n) (f : α → Vector β m) (p : β → Bool) :
+    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
+  cases xs
+  simp [Array.find?_flatMap, Array.flatMap_toArray]
+
+
+theorem find?_flatMap_eq_none_iff {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
+  simp
+
+theorem find?_mkVector :
+    find? p (mkVector n a) = if n = 0 then none else if p a then some a else none := by
+  rw [mkVector_eq_mk_mkArray, find?_mk, Array.find?_mkArray]
+
+@[simp] theorem find?_mkVector_of_length_pos (h : 0 < n) :
+    find? p (mkVector n a) = if p a then some a else none := by
+  simp [find?_mkVector, Nat.ne_of_gt h]
+
+@[simp] theorem find?_mkVector_of_pos (h : p a) :
+    find? p (mkVector n a) = if n = 0 then none else some a := by
+  simp [find?_mkVector, h]
+
+@[simp] theorem find?_mkVector_of_neg (h : ¬ p a) : find? p (mkVector n a) = none := by
+  simp [find?_mkVector, h]
+
+-- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
+theorem find?_mkVector_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
+    (mkVector n a).find? p = none ↔ n = 0 ∨ !p a := by
+  simp [Classical.or_iff_not_imp_left]
+
+@[simp] theorem find?_mkVector_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
+    (mkVector n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+  rw [mkVector_eq_mk_mkArray, find?_mk]
+  simp
+
+@[simp] theorem get_find?_mkVector (n : Nat) (a : α) (p : α → Bool) (h) :
+    ((mkVector n a).find? p).get h = a := by
+  simp only [mkVector_eq_mk_mkArray, find?_mk]
+  simp
+
+theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
+    (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
+    (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
+  simp only [pmap_eq_map_attach, find?_map]
+  rfl
+
+theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α} :
+    xs.find? p = some b ↔ p b ∧ ∃ i h, xs[i] = b ∧ ∀ j : Nat, (hj : j < i) → !p xs[j] := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.find?_eq_some_iff_getElem]
+
+/-! ### findFinIdx? -/
+
+@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := rfl
+
+@[congr] theorem findFinIdx?_congr {p : α → Bool} {l₁ : Vector α n} {l₂ : Vector α n} (w : l₁ = l₂) :
+    findFinIdx? p l₁ = findFinIdx? p l₂ := by
+  subst w
+  simp
+
+@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : Vector { x // p x } n}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findFinIdx? f = l.unattach.findFinIdx? g := by
+  rcases l with ⟨l, rfl⟩
+  simp [hf, Function.comp_def]
+
+end Vector
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index eaf2dcc012..45e9b9ebcb 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -104,6 +104,9 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem finIdxOf?_mk [BEq α] (a : Array α) (h : a.size = n) (x : α) :
     (Vector.mk a h).finIdxOf? x = (a.finIdxOf? x).map (Fin.cast h) := rfl
 
+@[simp] theorem findFinIdx?_mk (a : Array α) (h : a.size = n) (f : α → Bool) :
+    (Vector.mk a h).findFinIdx? f = (a.findFinIdx? f).map (Fin.cast h) := rfl
+
 @[deprecated finIdxOf?_mk (since := "2025-01-29")]
 abbrev indexOf?_mk := @finIdxOf?_mk
 
@@ -113,6 +116,24 @@ abbrev indexOf?_mk := @finIdxOf?_mk
 @[simp] theorem findSomeM?_mk [Monad m] (a : Array α) (h : a.size = n) (f : α → m (Option β)) :
     (Vector.mk a h).findSomeM? f = a.findSomeM? f := rfl
 
+@[simp] theorem findRevM?_mk [Monad m] (a : Array α) (h : a.size = n) (f : α → m Bool) :
+    (Vector.mk a h).findRevM? f = a.findRevM? f := rfl
+
+@[simp] theorem findSomeRevM?_mk [Monad m] (a : Array α) (h : a.size = n) (f : α → m (Option β)) :
+    (Vector.mk a h).findSomeRevM? f = a.findSomeRevM? f := rfl
+
+@[simp] theorem find?_mk (a : Array α) (h : a.size = n) (f : α → Bool) :
+    (Vector.mk a h).find? f = a.find? f := rfl
+
+@[simp] theorem findSome?_mk (a : Array α) (h : a.size = n) (f : α → Option β) :
+    (Vector.mk a h).findSome? f = a.findSome? f := rfl
+
+@[simp] theorem findRev?_mk (a : Array α) (h : a.size = n) (f : α → Bool) :
+    (Vector.mk a h).findRev? f = a.findRev? f := rfl
+
+@[simp] theorem findSomeRev?_mk (a : Array α) (h : a.size = n) (f : α → Option β) :
+    (Vector.mk a h).findSomeRev? f = a.findSomeRev? f := rfl
+
 @[simp] theorem mk_isEqv_mk (r : α → α → Bool) (a b : Array α) (ha : a.size = n) (hb : b.size = n) :
     Vector.isEqv (Vector.mk a ha) (Vector.mk b hb) r = Array.isEqv a b r := by
   simp [Vector.isEqv, Array.isEqv, ha, hb]
@@ -366,6 +387,56 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (v : Vector
   cases v
   simp
 
+@[simp] theorem find?_toArray (p : α → Bool) (v : Vector α n) :
+    v.toArray.find? p = v.find? p := by
+  cases v
+  simp
+
+@[simp] theorem findSome?_toArray (f : α → Option β) (v : Vector α n) :
+    v.toArray.findSome? f = v.findSome? f := by
+  cases v
+  simp
+
+@[simp] theorem findRev?_toArray (p : α → Bool) (v : Vector α n) :
+    v.toArray.findRev? p = v.findRev? p := by
+  cases v
+  simp
+
+@[simp] theorem findSomeRev?_toArray (f : α → Option β) (v : Vector α n) :
+    v.toArray.findSomeRev? f = v.findSomeRev? f := by
+  cases v
+  simp
+
+@[simp] theorem findM?_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
+    v.toArray.findM? p = v.findM? p := by
+  cases v
+  simp
+
+@[simp] theorem findSomeM?_toArray [Monad m] (f : α → m (Option β)) (v : Vector α n) :
+    v.toArray.findSomeM? f = v.findSomeM? f := by
+  cases v
+  simp
+
+@[simp] theorem findRevM?_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
+    v.toArray.findRevM? p = v.findRevM? p := by
+  rcases v with ⟨v, rfl⟩
+  simp
+
+@[simp] theorem findSomeRevM?_toArray [Monad m] (f : α → m (Option β)) (v : Vector α n) :
+    v.toArray.findSomeRevM? f = v.findSomeRevM? f := by
+  rcases v with ⟨v, rfl⟩
+  simp
+
+@[simp] theorem finIdxOf?_toArray [BEq α] (a : α) (v : Vector α n) :
+    v.toArray.finIdxOf? a = (v.finIdxOf? a).map (Fin.cast v.size_toArray.symm) := by
+  rcases v with ⟨v, rfl⟩
+  simp
+
+@[simp] theorem findFinIdx?_toArray (p : α → Bool) (v : Vector α n) :
+    v.toArray.findFinIdx? p = (v.findFinIdx? p).map (Fin.cast v.size_toArray.symm) := by
+  rcases v with ⟨v, rfl⟩
+  simp
+
 @[simp] theorem toArray_mkVector : (mkVector n a).toArray = mkArray n a := rfl
 
 @[simp] theorem toArray_inj {v w : Vector α n} : v.toArray = w.toArray ↔ v = w := by
@@ -503,6 +574,36 @@ theorem toList_swap (a : Vector α n) (i j) (hi hj) :
   cases v
   simp
 
+@[simp] theorem find?_toList (p : α → Bool) (v : Vector α n) :
+    v.toList.find? p = v.find? p := by
+  cases v
+  simp
+
+@[simp] theorem findSome?_toList (f : α → Option β) (v : Vector α n) :
+    v.toList.findSome? f = v.findSome? f := by
+  cases v
+  simp
+
+@[simp] theorem findM?_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (v : Vector α n) :
+    v.toList.findM? p = v.findM? p := by
+  cases v
+  simp
+
+@[simp] theorem findSomeM?_toList [Monad m] [LawfulMonad m] (f : α → m (Option β)) (v : Vector α n) :
+    v.toList.findSomeM? f = v.findSomeM? f := by
+  cases v
+  simp
+
+@[simp] theorem finIdxOf?_toList [BEq α] (a : α) (v : Vector α n) :
+    v.toList.finIdxOf? a = (v.finIdxOf? a).map (Fin.cast v.size_toArray.symm) := by
+  rcases v with ⟨v, rfl⟩
+  simp
+
+@[simp] theorem findFinIdx?_toList (p : α → Bool) (v : Vector α n) :
+    v.toList.findFinIdx? p = (v.findFinIdx? p).map (Fin.cast v.size_toArray.symm) := by
+  rcases v with ⟨v, rfl⟩
+  simp
+
 @[simp] theorem toList_mkVector : (mkVector n a).toList = List.replicate n a := rfl
 
 theorem toList_inj {v w : Vector α n} : v.toList = w.toList ↔ v = w := by
@@ -2215,6 +2316,16 @@ defeq issues in the implicit size argument.
     subst h
     simp [back]
 
+/-! ### findRev? and findSomeRev? -/
+
+@[simp] theorem findRev?_eq_find?_reverse (f : α → Bool) (as : Vector α n) :
+    findRev? f as = find? f as.reverse := by
+  simp [findRev?, find?]
+
+@[simp] theorem findSomeRev?_eq_findSome?_reverse (f : α → Option β) (as : Vector α n) :
+    findSomeRev? f as = findSome? f as.reverse := by
+  simp [findSomeRev?, findSome?]
+
 /-! ### zipWith -/
 
 @[simp] theorem getElem_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) (i : Nat)