chore: adaptations for batteries#1490 (#31270)

After [batteries#1490](leanprover-community/batteries#1490) is merged:

- [x] Edit the lakefile to point to leanprover-community/batteries:main
- [x] Run lake update batteries
- [x] Merge leanprover-community/mathlib4:master
- [ ] Wait for CI and merge

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

Author: fgdorais

Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -851,7 +851,7 @@ theorem exists_isTorsionBy {p : R} (hM : IsTorsion' M <| Submonoid.powers p) (d
   let oj := List.argmax (fun i => pOrder hM <| s i) (List.finRange d)
   have hoj : oj.isSome :=
     Option.ne_none_iff_isSome.mp fun eq_none =>
-      hd <| List.finRange_eq_nil.mp <| List.argmax_eq_none.mp eq_none
+      hd <| List.finRange_eq_nil_iff.mp <| List.argmax_eq_none.mp eq_none
   use Option.get _ hoj
   rw [isTorsionBy_iff_torsionBy_eq_top, eq_top_iff, ← hs, Submodule.span_le,
     Set.range_subset_iff]

Mathlib/Analysis/Calculus/FDeriv/Mul.lean

@@ -539,7 +539,7 @@ theorem hasStrictFDerivAt_list_prod [DecidableEq ι] [Fintype ι] {l : List ι}
     HasStrictFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.map x).prod)
       (l.map fun i ↦ ((l.erase i).map x).prod • proj i).sum x := by
   refine hasStrictFDerivAt_list_prod'.congr_fderiv ?_
-  conv_rhs => arg 1; arg 2; rw [← List.finRange_map_get l]
+  conv_rhs => arg 1; arg 2; rw [← List.map_get_finRange l]
   simp only [List.map_map, ← List.sum_toFinset _ (List.nodup_finRange _), List.toFinset_finRange,
     Function.comp_def, ((List.erase_getElem _).map _).prod_eq, List.eraseIdx_eq_take_drop_succ,
     List.map_append, List.prod_append, List.get_eq_getElem, Fin.getElem_fin, Nat.succ_eq_add_one]
@@ -575,7 +575,7 @@ theorem HasStrictFDerivAt.list_prod' {l : List ι} {x : E}
     HasStrictFDerivAt (fun x ↦ (l.map (f · x)).prod)
       (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
         f' l[i] <• ((l.drop (.succ i)).map (f · x)).prod) x := by
-  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
+  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
   -- After https://github.com/leanprover-community/mathlib4/issues/19108, we have to be optimistic with `:)`s; otherwise Lean decides it need to find
   -- `NormedAddCommGroup (List 𝔸)` which is nonsense.
   refine .congr_fderiv (hasStrictFDerivAt_list_prod_finRange'.comp x
@@ -593,7 +593,7 @@ theorem HasFDerivAt.list_prod' {l : List ι} {x : E}
     HasFDerivAt (fun x ↦ (l.map (f · x)).prod)
       (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
         f' l[i] <• ((l.drop (.succ i)).map (f · x)).prod) x := by
-  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
+  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
   refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp x
     (hasFDerivAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
   ext m
@@ -606,7 +606,7 @@ theorem HasFDerivWithinAt.list_prod' {l : List ι} {x : E}
     HasFDerivWithinAt (fun x ↦ (l.map (f · x)).prod)
       (∑ i : Fin l.length, ((l.take i).map (f · x)).prod •
         f' l[i] <• ((l.drop (.succ i)).map (f · x)).prod) s x := by
-  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.finRange_map_get l, List.map_map]
+  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
   refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
     (hasFDerivWithinAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
   ext m

Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean

@@ -730,7 +730,7 @@ theorem norm_mkPiAlgebraFin_succ_le : ‖ContinuousMultilinearMap.mkPiAlgebraFin
   simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
     Fin.prod_univ_def]
   refine (List.norm_prod_le' ?_).trans_eq ?_
-  · rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil]
+  · rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil_iff]
     exact Nat.succ_ne_zero _
   rw [List.map_map, Function.comp_def]
 

Mathlib/Data/Finset/Sort.lean

@@ -234,7 +234,7 @@ theorem map_orderEmbOfFin_univ (s : Finset α) {k : ℕ} (h : s.card = k) :
 theorem listMap_orderEmbOfFin_finRange (s : Finset α) {k : ℕ} (h : s.card = k) :
     (List.finRange k).map (s.orderEmbOfFin h) = s.sort := by
   obtain rfl : k = s.sort.length := by simp [h]
-  exact List.finRange_map_getElem s.sort
+  exact List.map_getElem_finRange s.sort
 
 /-- The bijection `orderEmbOfFin s h` sends `0` to the minimum of `s`. -/
 theorem orderEmbOfFin_zero {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k) :

Mathlib/Data/List/FinRange.lean

@@ -26,47 +26,24 @@ namespace List
 variable {α : Type u}
 
 
-theorem finRange_eq_pmap_range (n : ℕ) : finRange n = (range n).pmap Fin.mk (by simp) := by
-  apply List.ext_getElem <;> simp [finRange]
-
-theorem nodup_finRange (n : ℕ) : (finRange n).Nodup := by
-  rw [finRange_eq_pmap_range]
-  exact (Pairwise.pmap nodup_range _) fun _ _ _ _ => @Fin.ne_of_val_ne _ ⟨_, _⟩ ⟨_, _⟩
-
-@[simp]
-theorem finRange_eq_nil {n : ℕ} : finRange n = [] ↔ n = 0 := by
-  rw [← length_eq_zero_iff, length_finRange]
-
-theorem pairwise_lt_finRange (n : ℕ) : Pairwise (· < ·) (finRange n) := by
-  rw [finRange_eq_pmap_range]
-  exact List.pairwise_lt_range.pmap (by simp) (by simp)
-
-theorem pairwise_le_finRange (n : ℕ) : Pairwise (· ≤ ·) (finRange n) := by
-  rw [finRange_eq_pmap_range]
-  exact List.pairwise_le_range.pmap (by simp) (by simp)
-
 @[simp]
 lemma count_finRange {n : ℕ} (a : Fin n) : count a (finRange n) = 1 := by
   simp [List.Nodup.count (nodup_finRange n)]
 
-theorem get_finRange {n : ℕ} {i : ℕ} (h) :
-    (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange (n := n) ▸ h⟩ := by
-  simp
+@[simp] theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i := by
+  simpa using (nodup_finRange k).idxOf_getElem i
 
-@[simp]
-theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
-  List.ext_get (by simp) (by simp)
+@[deprecated finRange_eq_nil_iff (since := "2025-11-04")]
+alias finRange_eq_nil := finRange_eq_nil_iff
 
-@[simp]
-theorem finRange_map_getElem (l : List α) : (finRange l.length).map (l[·.1]) = l :=
-  finRange_map_get l
+@[deprecated (since := "2025-11-04")]
+alias finRange_map_get := map_get_finRange
 
-@[simp] theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i := by
-  simpa using (nodup_finRange k).idxOf_getElem i
+@[deprecated (since := "2025-11-04")]
+alias finRange_map_getElem := map_getElem_finRange
 
-@[simp]
-theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n := by
-  apply List.ext_getElem <;> simp
+@[deprecated (since := "2025-11-04")]
+alias map_coe_finRange := map_coe_finRange_eq_range
 
 @[deprecated finRange_succ (since := "2025-10-10")]
 theorem finRange_succ_eq_map (n : ℕ) : finRange n.succ = 0 :: (finRange n).map Fin.succ :=

Mathlib/Data/List/Sublists.lean

@@ -345,7 +345,7 @@ theorem sublists'_map (f : α → β) : ∀ (l : List α),
   | a::l => by simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]
 
 theorem sublists_perm_sublists' (l : List α) : sublists l ~ sublists' l := by
-  rw [← finRange_map_get l, sublists_map, sublists'_map]
+  rw [← map_get_finRange l, sublists_map, sublists'_map]
   apply Perm.map
   apply (perm_ext_iff_of_nodup _ _).mpr
   · simp

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6ac53033da7f895a7d7a8597d2455b5e68e296e6",
+   "rev": "f2aca6fc4a47c5b67fad08d3eda5e949d5b73ac0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",