diff --git a/Batteries/Data/List/Basic.lean b/Batteries/Data/List/Basic.lean
index c02b309f75..301a6beebd 100644
--- a/Batteries/Data/List/Basic.lean
+++ b/Batteries/Data/List/Basic.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 
 module
+import Batteries.Tactic.Alias
 
 @[expose] public section
 
@@ -242,16 +243,22 @@ also receives each element's index.
 Returns the elements of `l` that satisfy `p` together with their indexes in
 `l`. The returned list is ordered by index.
 -/
-@[inline] def indexesValues (p : α → Bool) (l : List α) : List (Nat × α) :=
+@[inline] def findIdxsValues (p : α → Bool) (l : List α) : List (Nat × α) :=
   foldrIdx (fun i a l => if p a then (i, a) :: l else l) [] l
 
+@[deprecated (since := "2025-11-06")]
+alias indexsValues := findIdxsValues
+
 /--
-`indexesOf a l` is the list of all indexes of `a` in `l`. For example:
+`idxsOf a l` is the list of all indexes of `a` in `l`. For example:
 ```
-indexesOf a [a, b, a, a] = [0, 2, 3]
+idxsOf a [a, b, a, a] = [0, 2, 3]
 ```
 -/
-@[inline] def indexesOf [BEq α] (a : α) : List α → List Nat := findIdxs (· == a)
+@[inline] def idxsOf [BEq α] (a : α) : List α → List Nat := findIdxs (· == a)
+
+@[deprecated (since := "2025-11-06")]
+alias indexesOf := idxsOf
 
 /--
 `lookmap` is a combination of `lookup` and `filterMap`.
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 3dc54db783..e1ab5fed1e 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -429,7 +429,7 @@ theorem isChain_lt_range' (s n : Nat) (h : 0 < step) :
 theorem chain_lt_range' (s n : Nat) (h : 0 < step) :
     IsChain (· < ·) (s :: range' (s + step) n step) := isChain_lt_range' _ (n + 1) h
 
-/-! ### indexOf and indexesOf -/
+/-! ### idxOf and idxsOf -/
 
 theorem foldrIdx_start :
     (xs : List α).foldrIdx f i s = (xs : List α).foldrIdx (fun i => f (i + s)) i := by
@@ -449,22 +449,22 @@ theorem findIdxs_cons :
   dsimp [findIdxs]
   rw [cond_eq_if]
   split <;>
-  · simp only [foldrIdx_start, Nat.add_zero, cons.injEq, true_and]
+  · simp [foldrIdx_start, Nat.add_zero, true_and]
     apply findIdxs_cons_aux
 
-@[simp, grind =] theorem indexesOf_nil [BEq α] : ([] : List α).indexesOf x = [] := rfl
+@[simp, grind =] theorem idxsOf_nil [BEq α] : ([] : List α).idxsOf x = [] := rfl
 
 @[grind =]
-theorem indexesOf_cons [BEq α] : (x :: xs : List α).indexesOf y =
-    bif x == y then 0 :: (xs.indexesOf y).map (· + 1) else (xs.indexesOf y).map (· + 1) := by
-  simp [indexesOf, findIdxs_cons]
+theorem idxsOf_cons [BEq α] : (x :: xs : List α).idxsOf y =
+    bif x == y then 0 :: (xs.idxsOf y).map (· + 1) else (xs.idxsOf y).map (· + 1) := by
+  simp [idxsOf, findIdxs_cons]
 
 @[simp] theorem eraseIdx_idxOf_eq_erase [BEq α] (a : α) (l : List α) :
     l.eraseIdx (l.idxOf a) = l.erase a := by
   induction l with grind
 
-theorem idxOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) :
-    xs.idxOf x ∈ xs.indexesOf x := by
+theorem idxOf_mem_idxsOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) :
+    xs.idxOf x ∈ xs.idxsOf x := by
   induction xs with grind
 
 theorem idxOf_eq_idxOf? [BEq α] (a : α) (l : List α) :