[Merged by Bors] - chore: adaptations for batteries#1588

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",