[Merged by Bors] - chore: adaptation for batteries#1500

Mathlib/Data/FinEnum.lean

@@ -51,7 +51,7 @@ def ofNodupList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) (h' :
   card := xs.length
   equiv :=
     ⟨fun x => ⟨xs.idxOf x, by rw [List.idxOf_lt_length_iff]; apply h⟩, xs.get, fun x => by simp,
-      fun i => by ext; simp [List.idxOf_getElem h']⟩
+      fun i => by ext; simp [h'.idxOf_getElem]⟩
 
 /-- create a `FinEnum` instance from an exhaustive list; duplicates are removed -/
 def ofList [DecidableEq α] (xs : List α) (h : ∀ x : α, x ∈ xs) : FinEnum α :=

Mathlib/Data/List/Basic.lean

@@ -574,13 +574,6 @@ theorem ext_getElem! [Inhabited α] (hl : length l₁ = length l₂) (h : ∀ n
     l₁ = l₂ :=
   ext_getElem hl fun n h₁ h₂ ↦ by simpa only [← getElem!_pos] using h n
 
-@[simp]
-theorem getElem_idxOf [BEq α] [LawfulBEq α] {a : α} : ∀ {l : List α} (h : idxOf a l < l.length),
-    l[idxOf a l] = a
-  | b :: l, h => by
-    by_cases h' : b = a <;>
-    simp [h', getElem_idxOf]
-
 -- This is incorrectly named and should be `get_idxOf`;
 -- this already exists, so will require a deprecation dance.
 theorem idxOf_get [BEq α] [LawfulBEq α] {a : α} {l : List α} (h) : get l ⟨idxOf a l, h⟩ = a := by

Mathlib/Data/List/FinRange.lean

@@ -62,7 +62,7 @@ theorem finRange_map_getElem (l : List α) : (finRange l.length).map (l[·.1]) =
   finRange_map_get l
 
 @[simp] theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i := by
-  simpa using idxOf_getElem (nodup_finRange k) i
+  simpa using (nodup_finRange k).idxOf_getElem i
 
 @[simp]
 theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n := by

Mathlib/Data/List/Lattice.lean

@@ -194,7 +194,7 @@ theorem mem_bagInter {a : α} {l₁ l₂ : List α} : a ∈ l₁.bagInter l₂ 
 @[simp]
 theorem count_bagInter {a : α} {l₁ l₂ : List α} :
     count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂) := by
-  fun_induction List.bagInter with grind [count_pos_iff]
+  fun_induction List.bagInter with grind
 
 theorem bagInter_sublist_left {l₁ l₂ : List α} : l₁.bagInter l₂ <+ l₁ := by
   fun_induction List.bagInter with grind

Mathlib/Data/List/Nodup.lean

@@ -120,16 +120,14 @@ theorem not_nodup_of_get_eq_of_ne (xs : List α) (n m : Fin xs.length)
   rw [nodup_iff_injective_get]
   exact fun hinj => hne (hinj h)
 
-theorem idxOf_getElem [BEq α] [LawfulBEq α] {l : List α} (H : Nodup l) (i : Nat)
-    (h : i < l.length) : idxOf l[i] l = i := by
-  rw [← H.getElem_inj_iff, getElem_idxOf]
-  simp [idxOf_lt_length_iff]
+@[deprecated Nodup.idxOf_getElem (since := "2025-11-10")]
+theorem idxOf_getElem [DecidableEq α] {l : List α} : Nodup l → (i : Nat) → (h : i < l.length) →
+    idxOf l[i] l = i := Nodup.idxOf_getElem
 
 -- This is incorrectly named and should be `idxOf_get`;
 -- this already exists, so will require a deprecation dance.
-theorem get_idxOf [BEq α] [LawfulBEq α] {l : List α} (H : Nodup l) (i : Fin l.length) :
-    idxOf (get l i) l = i := by
-  simp [idxOf_getElem, H]
+theorem get_idxOf [DecidableEq α] {l : List α} (H : Nodup l) (i : Fin l.length) :
+    idxOf (get l i) l = i := by grind
 
 theorem nodup_iff_count_le_one [BEq α] [LawfulBEq α] {l : List α} : Nodup l ↔ ∀ a, count a l ≤ 1 :=
   nodup_iff_sublist.trans <|

Mathlib/Data/List/NodupEquivFin.lean

@@ -67,7 +67,7 @@ def getEquivOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈
     Fin l.length ≃ α where
   toFun i := l.get i
   invFun a := ⟨_, idxOf_lt_length_iff.2 (h a)⟩
-  left_inv i := by simp [List.idxOf_getElem, nd]
+  left_inv i := by simp [nd]
   right_inv a := by simp
 
 end Nodup

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "30cfb2255996f3e6217a77fd940fde1f3e12ccc2",
+   "rev": "26884086fb66f99b56ed363c5e54bfcc70238599",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",