feat: simplification lemmas for Vector.map / Vector.mapAccumr (#5558)

Primarily focused on folding nested applications of `mapAccumr` into a single `mapAccumr`



Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

Author: alexkeizer

Mathlib.lean

@@ -1795,6 +1795,7 @@ import Mathlib.Data.ULift
 import Mathlib.Data.UnionFind
 import Mathlib.Data.Vector
 import Mathlib.Data.Vector.Basic
+import Mathlib.Data.Vector.MapLemmas
 import Mathlib.Data.Vector.Mem
 import Mathlib.Data.Vector.Snoc
 import Mathlib.Data.Vector.Zip

Mathlib/Data/Vector/Basic.lean

@@ -810,8 +810,6 @@ theorem get_map₂ (v₁ : Vector α n) (v₂ : Vector β n) (f : α → β →
     · simp only [get_zero, head_cons]
     · simp only [get_cons_succ, ih]
 
-
-
 @[simp]
 theorem mapAccumr_cons :
     mapAccumr f (x ::ᵥ xs) s