diff --git a/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean
index 8ccb3bd4622484..a46f55b6538bc5 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean
@@ -100,6 +100,10 @@ theorem edges_map : (p.map f).edges = p.edges.map (Sym2.map f) := by
 @[simp]
 theorem edgeSet_map : (p.map f).edgeSet = Sym2.map f '' p.edgeSet := by ext; simp
 
+@[simp]
+theorem getVert_map (n : ℕ) : (p.map f).getVert n = f (p.getVert n) := by
+  induction p generalizing n <;> cases n <;> simp [*]
+
 theorem map_injective_of_injective {f : G →g G'} (hinj : Function.Injective f) (u v : V) :
     Function.Injective (Walk.map f : G.Walk u v → G'.Walk (f u) (f v)) := by
   intro p p' h