chore: adaptations for batteries#1489 (leanprover-community#31220)

After [batteries#1489](leanprover-community/batteries#1489) 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/Data/Array/Extract.lean

@@ -6,6 +6,7 @@ Authors: Jiecheng Zhao
 module
 
 public import Mathlib.Init
+public import Batteries.Data.Array.Lemmas
 /-!
 # Lemmas about `Array.extract`
 
@@ -19,30 +20,16 @@ variable {α : Type u} {i : Nat}
 
 namespace Array
 
-@[simp]
-theorem extract_eq_nil_of_start_eq_end {a : Array α} :
-    a.extract i i = #[] := by
-  refine extract_empty_of_stop_le_start ?h
-  exact Nat.le_refl i
+@[deprecated (since := "2025-11-03")]
+alias extract_eq_nil_of_start_eq_end := extract_empty_of_start_eq_stop
 
-/--
-This is a stronger version of `Array.extract_append_left`,
-and should be upstreamed to replace that.
--/
-theorem extract_append_left' {a b : Array α} {i j : Nat} (h : j ≤ a.size) :
-    (a ++ b).extract i j = a.extract i j := by
-  simp [h]
+@[deprecated (since := "2025-11-03")]
+alias extract_append_left' := extract_append_of_stop_le_size_left
 
-/--
-This is a stronger version of `Array.extract_append_right`,
-and should be upstreamed to replace that.
--/
-theorem extract_append_right' {a b : Array α} {i j : Nat} (h : a.size ≤ i) :
-    (a ++ b).extract i j = b.extract (i - a.size) (j - a.size) := by
-  grind
+@[deprecated (since := "2025-11-03")]
+alias extract_append_right' := extract_append_of_size_left_le_start
 
-theorem extract_eq_of_size_le_end {l p : Nat} {a : Array α} (h : a.size ≤ l) :
-    a.extract p l = a.extract p a.size := by
-  simp only [extract, Nat.min_eq_right h, Nat.sub_eq, Nat.min_self]
+@[deprecated (since := "2025-11-03")]
+alias extract_eq_of_size_le_end := extract_eq_of_size_le_stop
 
 end Array

lake-manifest.json

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