chore: adaptations for batteries#1491 (#31334)

After [batteries#1491](leanprover-community/batteries#1491) 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>
Co-authored-by: Wrenna Robson <wrenna.robson@bristol.ac.uk>

Author: 3 people

Mathlib/Data/List/Sublists.lean

@@ -118,14 +118,6 @@ theorem sublistsAux_eq_flatMap :
       rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]
       simp [sublistsAux])
 
-@[csimp] theorem sublists_eq_sublistsFast : @sublists = @sublistsFast := by
-  ext α l : 2
-  trans l.foldr sublistsAux [[]]
-  · rw [sublistsAux_eq_flatMap, sublists]
-  · simp only [sublistsFast, sublistsAux_eq_array_foldl]
-    rw [← foldr_hom Array.toList]
-    · intros; congr
-
 theorem sublists_append (l₁ l₂ : List α) :
     sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (· ++ x)) := by
   simp only [sublists, foldr_append]

lake-manifest.json

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