fix: Vector lemma

Batteries/Data/Vector/Lemmas.lean

@@ -19,8 +19,7 @@ namespace Vector
 
 /-- An `empty` vector maps to a `empty` vector. -/
 @[simp]
-theorem map_empty (f : α → β) : map f empty = empty :=
-  rfl
+theorem map_empty (f : α → β) : map f empty = empty := by with_unfolding_all rfl
 
 
 theorem eq : ∀ v w : Vector α n, v.toArray = w.toArray → v = w