diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 309f34b786..0bfbc138dc 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -674,18 +674,30 @@ def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
+@[inline]
+def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
+
 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
+def idxOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
   if h : i < a.size then
     if a[i] == v then some ⟨i, h⟩
-    else indexOfAux a v (i+1)
+    else idxOfAux a v (i+1)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
+@[deprecated idxOfAux (since := "2025-01-29")]
+abbrev indexOfAux := @idxOfAux
 
-@[deprecated indexOf? (since := "2024-11-20")]
+def finIdxOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  idxOfAux a v 0
+
+@[deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")]
+abbrev indexOf? := @finIdxOf?
+
+def idxOf? [BEq α] (a : Array α) (v : α) : Option Nat :=
+  (a.finIdxOf? v).map (·.val)
+
+@[deprecated idxOf? (since := "2024-11-20")]
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
   a.findIdx? fun a => a == v
 
@@ -884,7 +896,7 @@ def eraseIdx! (a : Array α) (i : Nat) : Array α :=
 This function takes worst case O(n) time because
 it has to backshift all later elements. -/
 def erase [BEq α] (as : Array α) (a : α) : Array α :=
-  match as.indexOf? a with
+  match as.finIdxOf? a with
   | none   => as
   | some i => as.eraseIdx i
 
@@ -893,9 +905,9 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
 This function takes worst case O(n) time because
 it has to backshift all later elements. -/
 def eraseP (as : Array α) (p : α → Bool) : Array α :=
-  match as.findIdx? p with
+  match as.findFinIdx? p with
   | none   => as
-  | some i => as.eraseIdxIfInBounds i
+  | some i => as.eraseIdx i
 
 /-- Insert element `a` at position `i`. -/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index c246f63f67..d59a5708d0 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -1269,21 +1269,58 @@ theorem findSome?_cons {f : α → Option β} :
 /-! ### indexOf -/
 
 /-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
-def indexOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
+def idxOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
 
-@[simp] theorem indexOf_nil [BEq α] : ([] : List α).indexOf x = 0 := rfl
+/-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
+@[deprecated idxOf (since := "2025-01-29")] abbrev indexOf := @idxOf
+
+@[simp] theorem idxOf_nil [BEq α] : ([] : List α).idxOf x = 0 := rfl
+
+@[deprecated idxOf_nil (since := "2025-01-29")]
+theorem indexOf_nil [BEq α] : ([] : List α).idxOf x = 0 := rfl
 
 /-! ### findIdx? -/
 
 /-- Return the index of the first occurrence of an element satisfying `p`. -/
-def findIdx? (p : α → Bool) : List α → (start : Nat := 0) → Option Nat
-| [], _ => none
-| a :: l, i => if p a then some i else findIdx? p l (i + 1)
+def findIdx? (p : α → Bool) (l : List α) : Option Nat :=
+  go l 0
+where
+  go : List α → Nat → Option Nat
+  | [], _ => none
+  | a :: l, i => if p a then some i else go l (i + 1)
 
 /-! ### indexOf? -/
 
 /-- Return the index of the first occurrence of `a` in the list. -/
-@[inline] def indexOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
+@[inline] def idxOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
+
+/-- Return the index of the first occurrence of `a` in the list. -/
+@[deprecated idxOf? (since := "2025-01-29")]
+abbrev indexOf? := @idxOf?
+
+/-! ### findFinIdx? -/
+
+/-- Return the index of the first occurrence of an element satisfying `p`, as a `Fin l.length`,
+or `none` if no such element is found. -/
+@[inline] def findFinIdx? (p : α → Bool) (l : List α) : Option (Fin l.length) :=
+  go l 0 (by simp)
+where
+  go : (l' : List α) → (i : Nat) → (h : l'.length + i = l.length) → Option (Fin l.length)
+  | [], _, _ => none
+  | a :: l, i, h =>
+    if p a then
+      some ⟨i, by
+        simp only [Nat.add_comm _ i, ← Nat.add_assoc] at h
+        exact Nat.lt_of_add_right_lt (Nat.lt_of_succ_le (Nat.le_of_eq h))⟩
+    else
+      go l (i + 1) (by simp at h; simpa [← Nat.add_assoc, Nat.add_right_comm] using h)
+
+/-! ### finIdxOf? -/
+
+/-- Return the index of the first occurrence of `a`, as a `Fin l.length`,
+or `none` if no such element is found. -/
+@[inline] def finIdxOf? [BEq α] (a : α) : (l : List α) → Option (Fin l.length) :=
+  findFinIdx? (· == a)
 
 /-! ### countP -/
 
diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index 83970dcab0..25cbf623a0 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -472,13 +472,13 @@ theorem getLast_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).getLast h 
   (erase_sublist a xs).getLast_mem h
 
 theorem erase_eq_eraseIdx [LawfulBEq α] (l : List α) (a : α) :
-    l.erase a = match l.indexOf? a with
+    l.erase a = match l.idxOf? a with
     | none => l
     | some i => l.eraseIdx i := by
   induction l with
   | nil => simp
   | cons x xs ih =>
-    rw [erase_cons, indexOf?_cons]
+    rw [erase_cons, idxOf?_cons]
     split
     · simp
     · simp [ih]
@@ -600,8 +600,8 @@ protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
 -- See also `mem_eraseIdx_iff_getElem` and `mem_eraseIdx_iff_getElem?` in
 -- `Init/Data/List/Nat/Basic.lean`.
 
-theorem erase_eq_eraseIdx_of_indexOf [BEq α] [LawfulBEq α]
-    (l : List α) (a : α) (i : Nat) (w : l.indexOf a = i) :
+theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α]
+    (l : List α) (a : α) (i : Nat) (w : l.idxOf a = i) :
     l.erase a = l.eraseIdx i := by
   subst w
   rw [erase_eq_iff]
@@ -609,11 +609,14 @@ theorem erase_eq_eraseIdx_of_indexOf [BEq α] [LawfulBEq α]
   · right
     obtain ⟨as, bs, rfl, h'⟩ := eq_append_cons_of_mem h
     refine ⟨as, bs, h', by simp, ?_⟩
-    rw [indexOf_append, if_neg h', indexOf_cons_self, eraseIdx_append_of_length_le] <;>
+    rw [idxOf_append, if_neg h', idxOf_cons_self, eraseIdx_append_of_length_le] <;>
       simp
   · left
     refine ⟨h, ?_⟩
     rw [eq_comm, eraseIdx_eq_self]
-    exact Nat.le_of_eq (indexOf_eq_length h).symm
+    exact Nat.le_of_eq (idxOf_eq_length h).symm
+
+@[deprecated erase_eq_eraseIdx_of_idxOf (since := "2025-01-29")]
+abbrev erase_eq_eraseIdx_of_indexOf := @erase_eq_eraseIdx_of_idxOf
 
 end List
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 00c0ae4d6c..82f406b395 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -641,29 +641,36 @@ theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p
 
 /-! ### findIdx? -/
 
-@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
+@[local simp] private theorem findIdx?_go_nil {p : α → Bool} {i : Nat} :
+    findIdx?.go p [] i = none := rfl
 
-@[simp] theorem findIdx?_cons :
-    (x :: xs).findIdx? p i = if p x then some i else findIdx? p xs (i + 1) := 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
 
-theorem findIdx?_succ :
-    (xs : List α).findIdx? p (i+1) = (xs.findIdx? p i).map fun i => i + 1 := by
+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
 
-@[simp] theorem findIdx?_start_succ :
-    (xs : List α).findIdx? p (i+1) = (xs.findIdx? p 0).map fun k => k + (i + 1) := by
+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?_succ, findIdx?_cons, Nat.zero_add]
+    simp only [findIdx?_go_succ, findIdx?_go_cons, Nat.zero_add]
     split
     · simp_all
-    · simp_all only [findIdx?_succ, Bool.not_eq_true, Option.map_map, Nat.zero_add]
+    · 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]
+
 @[simp]
 theorem findIdx?_eq_none_iff {xs : List α} {p : α → Bool} :
     xs.findIdx? p = none ↔ ∀ x, x ∈ xs → p x = false := by
@@ -731,7 +738,7 @@ theorem findIdx?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {i : Nat}
   induction xs generalizing i with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ]
+    simp only [findIdx?_cons, Nat.zero_add]
     split
     · simp only [Option.some.injEq, Bool.not_eq_true, length_cons]
       cases i with
@@ -762,7 +769,7 @@ theorem findIdx?_of_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p
   induction xs generalizing i with
   | nil => simp_all
   | cons x xs ih =>
-    simp_all only [findIdx?_cons, Nat.zero_add, findIdx?_succ]
+    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) :
@@ -771,7 +778,7 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
   induction xs generalizing i with
   | nil => simp_all
   | cons x xs ih =>
-    simp_all only [Bool.not_eq_true, findIdx?_cons, Nat.zero_add, findIdx?_succ]
+    simp_all only [Bool.not_eq_true, findIdx?_cons, Nat.zero_add]
     cases i with
     | zero =>
       split at w <;> simp_all
@@ -784,7 +791,7 @@ theorem findIdx?_of_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
   induction l with
   | nil => simp
   | cons x xs ih =>
-    simp only [map_cons, findIdx?]
+    simp only [map_cons, findIdx?_cons]
     split <;> simp_all
 
 @[simp] theorem findIdx?_append :
@@ -801,25 +808,20 @@ theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
   induction l with
   | nil => simp
   | cons xs l ih =>
-    simp only [flatten, findIdx?_append, map_take, map_cons, findIdx?, any_eq_true, Nat.zero_add,
-      findIdx?_succ]
-    split
-    · simp only [Option.map_some', take_zero, sum_nil, length_cons, zero_lt_succ,
-        getElem?_eq_getElem, getElem_cons_zero, Option.getD_some, Nat.zero_add]
-      rw [Option.or_of_isSome (by simpa [findIdx?_isSome])]
-      rw [findIdx?_eq_some_of_exists ‹_›]
-    · simp_all only [map_take, not_exists, not_and, Bool.not_eq_true, Option.map_map]
-      rw [Option.or_of_isNone (by simpa [findIdx?_isNone])]
-      congr 1
-      ext i
-      simp [Nat.add_comm, Nat.add_assoc]
+    rw [flatten_cons, findIdx?_append, ih, findIdx?_cons]
+    split <;> rename_i h
+    · simp only [any_eq_true] at h
+      rw [Option.or_of_isSome (by simp_all [findIdx?_isSome])]
+      simp_all [findIdx?_eq_some_of_exists]
+    · rw [Option.or_of_isNone (by simp_all [findIdx?_isNone])]
+      simp [Function.comp_def, Nat.add_comm, Nat.add_assoc]
 
 @[simp] theorem findIdx?_replicate :
     (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
   cases n with
   | zero => simp
   | succ n =>
-    simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, zero_lt_succ, true_and]
+    simp only [replicate, findIdx?_cons, Nat.zero_add, zero_lt_succ, true_and]
     split <;> simp_all
 
 theorem findIdx?_eq_findSome?_zipIdx {xs : List α} {p : α → Bool} :
@@ -827,7 +829,7 @@ theorem findIdx?_eq_findSome?_zipIdx {xs : List α} {p : α → Bool} :
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, zipIdx]
+    simp only [findIdx?_cons, Nat.zero_add, zipIdx]
     split
     · simp_all
     · simp_all only [zipIdx_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
@@ -839,7 +841,7 @@ theorem findIdx?_eq_fst_find?_zipIdx {xs : List α} {p : α → Bool} :
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, zipIdx_cons]
+    simp only [findIdx?_cons, Nat.zero_add, zipIdx_cons]
     split
     · simp_all
     · rw [ih, ← map_snd_add_zipIdx_eq_zipIdx (n := 1) (k := 0)]
@@ -884,65 +886,80 @@ theorem IsInfix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l
     List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
   h.sublist.findIdx?_eq_none
 
-/-! ### indexOf
+/-! ### idxOf
 
-The verification API for `indexOf` is still incomplete.
+The verification API for `idxOf` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx` (and proved using them).
 -/
 
-theorem indexOf_cons [BEq α] :
-    (x :: xs : List α).indexOf y = bif x == y then 0 else xs.indexOf y + 1 := by
-  dsimp [indexOf]
+theorem idxOf_cons [BEq α] :
+    (x :: xs : List α).idxOf y = bif x == y then 0 else xs.idxOf y + 1 := by
+  dsimp [idxOf]
   simp [findIdx_cons]
 
-@[simp] theorem indexOf_cons_self [BEq α] [ReflBEq α] {l : List α} : (a :: l).indexOf a = 0 := by
-  simp [indexOf_cons]
+@[deprecated idxOf_cons (since := "2025-01-29")]
+abbrev indexOf_cons := @idxOf_cons
 
-theorem indexOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
-    (l₁ ++ l₂).indexOf a = if a ∈ l₁ then l₁.indexOf a else l₂.indexOf a + l₁.length := by
-  rw [indexOf, findIdx_append]
+@[simp] theorem idxOf_cons_self [BEq α] [ReflBEq α] {l : List α} : (a :: l).idxOf a = 0 := by
+  simp [idxOf_cons]
+
+@[deprecated idxOf_cons_self (since := "2025-01-29")]
+abbrev indexOf_cons_self := @idxOf_cons_self
+
+theorem idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
+    (l₁ ++ l₂).idxOf a = if a ∈ l₁ then l₁.idxOf a else l₂.idxOf a + l₁.length := by
+  rw [idxOf, findIdx_append]
   split <;> rename_i h
   · rw [if_pos]
     simpa using h
   · rw [if_neg]
     simpa using h
 
-theorem indexOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.indexOf a = l.length := by
+@[deprecated idxOf_append (since := "2025-01-29")]
+abbrev indexOf_append := @idxOf_append
+
+theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.idxOf a = l.length := by
   induction l with
   | nil => rfl
   | cons x xs ih =>
     simp only [mem_cons, not_or] at h
-    simp only [indexOf_cons, cond_eq_if, beq_iff_eq]
+    simp only [idxOf_cons, cond_eq_if, beq_iff_eq]
     split <;> simp_all
 
-theorem indexOf_lt_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∈ l) : l.indexOf a < l.length := by
+@[deprecated idxOf_eq_length (since := "2025-01-29")]
+abbrev indexOf_eq_length := @idxOf_eq_length
+
+theorem idxOf_lt_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∈ l) : l.idxOf a < l.length := by
   induction l with
   | nil => simp at h
   | cons x xs ih =>
     simp only [mem_cons] at h
     obtain rfl | h := h
     · simp
-    · simp only [indexOf_cons, cond_eq_if, beq_iff_eq, length_cons]
+    · simp only [idxOf_cons, cond_eq_if, beq_iff_eq, length_cons]
       specialize ih h
       split
       · exact zero_lt_succ xs.length
       · exact Nat.add_lt_add_right ih 1
 
-/-! ### indexOf?
+@[deprecated idxOf_lt_length (since := "2025-01-29")]
+abbrev indexOf_lt_length := @idxOf_lt_length
 
-The verification API for `indexOf?` is still incomplete.
+/-! ### 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 indexOf?_nil [BEq α] : ([] : List α).indexOf? a = none := rfl
+@[simp] theorem idxOf?_nil [BEq α] : ([] : List α).idxOf? a = none := rfl
 
-theorem indexOf?_cons [BEq α] (a : α) (xs : List α) (b : α) :
-    (a :: xs).indexOf? b = if a == b then some 0 else (xs.indexOf? b).map (· + 1) := by
-  simp [indexOf?]
+theorem idxOf?_cons [BEq α] (a : α) (xs : List α) (b : α) :
+    (a :: xs).idxOf? b = if a == b then some 0 else (xs.idxOf? b).map (· + 1) := by
+  simp [idxOf?]
 
-@[simp] theorem indexOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
-    l.indexOf? a = none ↔ a ∉ l := by
-  simp only [indexOf?, findIdx?_eq_none_iff, beq_eq_false_iff_ne, ne_eq]
+@[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+    l.idxOf? a = none ↔ a ∉ l := by
+  simp only [idxOf?, findIdx?_eq_none_iff, beq_eq_false_iff_ne, ne_eq]
   constructor
   · intro w h
     specialize w _ h
@@ -950,6 +967,9 @@ theorem indexOf?_cons [BEq α] (a : α) (xs : List α) (b : α) :
   · rintro w x h rfl
     contradiction
 
+@[deprecated idxOf?_eq_none_iff (since := "2025-01-29")]
+abbrev indexOf?_eq_none_iff := @idxOf?_eq_none_iff
+
 /-! ### lookup -/
 
 section lookup
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 133e76ffb3..813e114f02 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -343,8 +343,16 @@ instance [BEq α] : BEq (Vector α n) where
 Finds the first index of a given value in a vector using `==` for comparison. Returns `none` if the
 no element of the index matches the given value.
 -/
-@[inline] def indexOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) :=
-  (v.toArray.indexOf? x).map (Fin.cast v.size_toArray)
+@[inline] def finIdxOf? [BEq α] (v : Vector α n) (x : α) : Option (Fin n) :=
+  (v.toArray.finIdxOf? x).map (Fin.cast v.size_toArray)
+
+@[deprecated finIdxOf? (since := "2025-01-29")]
+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) :=
+  (v.toArray.findFinIdx? p).map (Fin.cast v.size_toArray)
 
 /--
 Note that the universe level is contrained to `Type` here,
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 35592506a0..2505e2af91 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -101,8 +101,11 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem extract_mk (a : Array α) (h : a.size = n) (start stop) :
     (Vector.mk a h).extract start stop = Vector.mk (a.extract start stop) (by simp [h]) := rfl
 
-@[simp] theorem indexOf?_mk [BEq α] (a : Array α) (h : a.size = n) (x : α) :
-    (Vector.mk a h).indexOf? x = (a.indexOf? x).map (Fin.cast h) := rfl
+@[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
+
+@[deprecated finIdxOf?_mk (since := "2025-01-29")]
+abbrev indexOf?_mk := @finIdxOf?_mk
 
 @[simp] theorem findM?_mk [Monad m] (a : Array α) (h : a.size = n) (f : α → m Bool) :
     (Vector.mk a h).findM? f = a.findM? f := rfl
diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean
index ad3747e090..4ca0e784ea 100644
--- a/src/Lean/Compiler/Specialize.lean
+++ b/src/Lean/Compiler/Specialize.lean
@@ -33,7 +33,7 @@ private def elabSpecArgs (declName : Name) (args : Array Syntax) : MetaM (Array
           result := result.push idx
       else
         let argName := arg.getId
-        if let some idx := argNames.indexOf? argName then
+        if let some idx := argNames.idxOf? argName then
           if result.contains idx then throwErrorAt arg "invalid specialization argument name `{argName}`, it has already been specified as a specialization candidate"
           result := result.push idx
         else
diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean
index 0308005867..8df0aa505c 100644
--- a/src/Lean/Data/PersistentHashMap.lean
+++ b/src/Lean/Data/PersistentHashMap.lean
@@ -231,7 +231,7 @@ def isUnaryNode : Node α β → Option (α × β)
 
 partial def eraseAux [BEq α] : Node α β → USize → α → Node α β
   | n@(Node.collision keys vals heq), _, k =>
-    match keys.indexOf? k with
+    match keys.finIdxOf? k with
     | some idx =>
       let keys' := keys.eraseIdx idx
       have keq := keys.size_eraseIdx idx _
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 566fec4d63..8a308c7b66 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -800,7 +800,7 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
         throwError "unexpected number of arguments at motive type{indentExpr motiveType}"
       unless motiveResultType.isSort do
         throwError "motive result type must be a sort{indentExpr motiveType}"
-    let some motivePos ← pure (xs.indexOf? motive) |
+    let some motivePos ← pure (xs.idxOf? motive) |
       throwError "unexpected eliminator type{indentExpr elimType}"
     /-
     Compute transitive closure of fvars appearing in arguments to the motive.
diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index b82b16f713..91ad989c0c 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -292,7 +292,7 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
     let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
-    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.indexOf? fnIdx
+    let some (size, idx) := positions.findSome? fun pos => (pos.size, ·) <$> pos.finIdxOf? fnIdx
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
     let brecOn ← PProdN.projM size idx brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)
diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index 4e70a4a496..786af4b14a 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
@@ -32,8 +32,8 @@ def prettyParameterSet (fnNames : Array Name) (xs : Array Expr) (values : Array
 private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := Id.run do
   let mut minPos := xs.size
   for index in indices do
-    match xs.indexOf? index with
-    | some pos => if pos.val < minPos then minPos := pos.val
+    match xs.idxOf? index with
+    | some pos => if pos < minPos then minPos := pos
     | _        => pure ()
   return minPos
 
@@ -91,8 +91,8 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
             throwError "its type is an inductive datatype{indentExpr xType}\nand the datatype parameter{indentExpr indParam}\ndepends on the function parameter{indentExpr y}\nwhich does not come before the varying parameters and before the indices of the recursion parameter."
           | none =>
             let indAll := indInfo.all.toArray
-            let .some indIdx := indAll.indexOf? indInfo.name | panic! "{indInfo.name} not in {indInfo.all}"
-            let indicesPos := indIndices.map fun index => match xs.indexOf? index with | some i => i.val | none => unreachable!
+            let .some indIdx := indAll.idxOf? indInfo.name | panic! "{indInfo.name} not in {indInfo.all}"
+            let indicesPos := indIndices.map fun index => match xs.idxOf? index with | some i => i | none => unreachable!
             let indGroupInst := {
               IndGroupInfo.ofInductiveVal indInfo with
               levels := us
@@ -208,7 +208,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr)
           if let some (_index, _y) ← hasBadIndexDep? ys indIndices then
             -- throwError "its type {indInfo.name} is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}"
             continue
-          let indicesPos := indIndices.map fun index => match (xs++ys).indexOf? index with | some i => i.val | none => unreachable!
+          let indicesPos := indIndices.map fun index => match (xs++ys).idxOf? index with | some i => i | none => unreachable!
           return .some
             { fnName       := recArgInfo.fnName
               numFixed     := recArgInfo.numFixed
diff --git a/src/Lean/Elab/PreDefinition/TerminationMeasure.lean b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
index 1d70811785..de827c16e7 100644
--- a/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
@@ -90,7 +90,7 @@ def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams :
 def TerminationMeasure.structuralArg (measure : TerminationMeasure) : MetaM Nat := do
   assert! measure.structural
   lambdaTelescope measure.fn fun ys e => do
-    let .some idx := ys.indexOf? e
+    let .some idx := ys.idxOf? e
       | panic! "TerminationMeasure.structuralArg: body not one of the parameters"
     return idx
 
diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean
index acc3daf507..59dd5149ed 100644
--- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean
+++ b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean
@@ -48,7 +48,7 @@ def packCalls (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Na
     let f := e.getAppFn
     if !f.isConst then
       return TransformStep.done e
-    if let some fidx := funNames.indexOf? f.constName! then
+    if let some fidx := funNames.idxOf? f.constName! then
       let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size
       let e' ← withAppN arity e fun args => do
         let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:]
diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean
index f950e3619c..e05da7b165 100644
--- a/src/Lean/Meta/Constructions/BRecOn.lean
+++ b/src/Lean/Meta/Constructions/BRecOn.lean
@@ -195,14 +195,14 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
     let rec go (prods : Array Expr) : List Expr → MetaM Expr
       | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
           let b ← PProdN.mk rlvl prods
-          let .some ⟨idx, _⟩ := motives.indexOf? minor_type_fn
+          let .some idx := motives.idxOf? minor_type_fn
             | throwError m!"Did not find {minor_type} in {motives}"
           mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
       | arg::args => do
         let argType ← inferType arg
         forallTelescope argType fun arg_args arg_type => do
           arg_type.withApp fun arg_type_fn arg_type_args => do
-            if let .some idx := motives.indexOf? arg_type_fn then
+            if let .some idx := motives.idxOf? arg_type_fn then
               let name ← arg.fvarId!.getUserName
               let type' ← mkForallFVars arg_args
                 (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
@@ -264,7 +264,7 @@ private def mkBRecOnFromRec (recName : Name) (ind reflexive : Bool) (nParams : N
     let indices : Array Expr := refArgs[nParams + recVal.numMotives + recVal.numMinors:refArgs.size - 1]
     let major   : Expr       := refArgs[refArgs.size - 1]!
 
-    let some idx := motives.indexOf? refBody.getAppFn
+    let some idx := motives.idxOf? refBody.getAppFn
       | throwError "result type of {refType} is not one of {motives}"
 
     -- universe parameter of the type fomer.
diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean
index a64119e31c..be9f618409 100644
--- a/src/Lean/Meta/FunInfo.lean
+++ b/src/Lean/Meta/FunInfo.lean
@@ -31,9 +31,9 @@ private def collectDeps (fvars : Array Expr) (e : Expr) : Array Nat :=
     | .proj _ _ e      => visit e deps
     | .mdata _ e       => visit e deps
     | .fvar ..         =>
-      match fvars.indexOf? e with
+      match fvars.idxOf? e with
       | none   => deps
-      | some i => if deps.contains i.val then deps else deps.push i.val
+      | some i => if deps.contains i then deps else deps.push i
     | _ => deps
   let deps := visit e #[]
   deps.qsort (fun i j => i < j)
@@ -82,7 +82,7 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
                   for h2 : i in [:args.size] do
                     if outParamPositions.contains i then
                       let arg := args[i]
-                      if let some idx := fvars.indexOf? arg then
+                      if let some idx := fvars.idxOf? arg then
                         if (← whnf (← inferType arg)).isForall then
                           paramInfo := paramInfo.modify idx fun info => { info with higherOrderOutParam := true }
                           higherOrderOutParams := higherOrderOutParams.insert arg.fvarId!
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index b355414a66..0b19de3aeb 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -562,7 +562,7 @@ where
 def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
   xs.findSomeM? fun x => do
   (← whnf (← inferType x)).withApp fun f _ =>
-  match f.constName?, xs.indexOf? x with
+  match f.constName?, xs.idxOf? x with
   | some name, some idx => do
     if (← isInductivePredicate name) then
       let (_, belowTy) ← belowType motive xs idx
@@ -571,7 +571,7 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
         trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
         if (← below.mvarId!.applyRules { backtracking := false, maxDepth := 1 } []).isEmpty then
           trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
-          if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx.val)
+          if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx)
         else
           trace[Meta.IndPredBelow.match] "could not find below term in the local context"
           pure none
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index d602bdb831..d8909221a4 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -751,9 +751,9 @@ private partial def process (p : Problem) : StateRefT State MetaM Unit := do
 private def getUElimPos? (matcherLevels : List Level) (uElim : Level) : MetaM (Option Nat) :=
   if uElim == levelZero then
     return none
-  else match matcherLevels.toArray.indexOf? uElim with
+  else match matcherLevels.idxOf? uElim with
     | none => throwError "dependent match elimination failed, universe level not found"
-    | some pos => return some pos.val
+    | some pos => return some pos
 
 /- See comment at `mkMatcher` before `mkAuxDefinition` -/
 register_builtin_option bootstrap.genMatcherCode : Bool := {
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 1186d2ccb9..9c08c3f01b 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -129,9 +129,9 @@ where
           let typeNew := b.instantiate1 y
           if let some (_, lhs, rhs) ← matchEq? d then
             if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-               let some j  := ys.indexOf? lhs | unreachable!
+               let some j  := ys.finIdxOf? lhs | unreachable!
                let ys      := ys.eraseIdx j
-               let some k  := args.indexOf? lhs | unreachable!
+               let some k  := args.idxOf? lhs | unreachable!
                let mask    := mask.set! k false
                let args    := args.map fun arg => if arg == lhs then rhs else arg
                let arg     ← mkEqRefl rhs
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index 3fb7544119..6c5c14adac 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -107,7 +107,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     if motiveArgs.isEmpty then
       throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)"
     let major := motiveArgs.back!
-    match xs.indexOf? major with
+    match xs.idxOf? major with
     | some majorPos => pure (major, majorPos, true)
     | none          => throwError "ill-formed recursor '{declName}'"
 
diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index 630b30017d..00e2ce222a 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -60,12 +60,12 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me
         throwError "unexpected number of arguments at motive type{indentExpr motiveType}"
       unless motiveResultType.isSort do
         throwError "motive result type must be a sort{indentExpr motiveType}"
-    let some motivePos ← pure (xs.indexOf? motive) |
+    let some motivePos ← pure (xs.idxOf? motive) |
       throwError "unexpected eliminator type{indentExpr elimType}"
     let targetsPos ← targets.mapM fun target => do
-      match xs.indexOf? target with
+      match xs.idxOf? target with
       | none => throwError "unexpected eliminator type{indentExpr elimType}"
-      | some targetPos => pure targetPos.val
+      | some targetPos => pure targetPos
     let mut altsInfo := #[]
     let env ← getEnv
     for h : i in [:xs.size] do
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index ef1a3d45d9..39148b7f1b 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -982,7 +982,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
           let fns := infos.map fun info =>
             mkAppN (.const info.name (info.levelParams.map mkLevelParam)) xs
           let isRecCall : Expr → Option Expr := fun e => do
-            if let .some i := motives.indexOf? e.getAppFn then
+            if let .some i := motives.idxOf? e.getAppFn then
               if e.getAppNumArgs = motiveArities[i]! then
                 return mkAppN fns[i]! e.getAppArgs
             .none