From b374853205d7f14ee0ed7ca4ac270a1940352456 Mon Sep 17 00:00:00 2001 From: WANG Yiyang Date: Tue, 25 Nov 2025 21:58:07 +0800 Subject: [PATCH 1/2] feat(Combinatorics/SimpleGraph): add simp lemma `getVert_map` for `Walk.map` --- Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean index 8ccb3bd4622484..a14700de97208b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean @@ -100,6 +100,12 @@ 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 (i : ℕ) : (p.map f).getVert i = f (p.getVert i) := by + revert u; induction i with + | zero => simp + | succ => intro _ p; cases p <;> 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 From 349868da808067660e536306e18330c506149189 Mon Sep 17 00:00:00 2001 From: WANG Yiyang <59402841+maix00@users.noreply.github.com> Date: Wed, 26 Nov 2025 02:17:00 +0000 Subject: [PATCH 2/2] feat(Combinatorics/SimpleGraph) `getVert_map` same proof as other operations --- Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean index a14700de97208b..a46f55b6538bc5 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean @@ -101,10 +101,8 @@ theorem edges_map : (p.map f).edges = p.edges.map (Sym2.map f) := by theorem edgeSet_map : (p.map f).edgeSet = Sym2.map f '' p.edgeSet := by ext; simp @[simp] -theorem getVert_map (i : ℕ) : (p.map f).getVert i = f (p.getVert i) := by - revert u; induction i with - | zero => simp - | succ => intro _ p; cases p <;> 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