diff --git a/Batteries/Data/Vector/Lemmas.lean b/Batteries/Data/Vector/Lemmas.lean
index 8aa8f72966..0a71f0f5f9 100644
--- a/Batteries/Data/Vector/Lemmas.lean
+++ b/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