chore: adaptations for batteries#1588 (leanprover-community#33681)

After [batteries#1588](leanprover-community/batteries#1588) 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/Vector/Basic.lean

@@ -316,7 +316,8 @@ into the provided starting value `b : β` and the recursed `scanl`
 This lemma is the `cons` version of `scanl_get`.
 -/
 @[simp]
-theorem scanl_cons (x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v := rfl
+theorem scanl_cons (x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v := by
+  apply Vector.eq; simp [scanl]
 
 /-- The underlying `List` of a `Vector` after a `scanl` is the `List.scanl`
 of the underlying `List` of the original `Vector`.

lake-manifest.json

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