feat(Combinatorics/SimpleGraph/Walk): induce.mapLe = induce (leanprover-community#30873)

Inducing a walk to `G[s]` and then mapping to `G[s']` is the same as inducing to `G[s']` when `s ⊆ s'`.

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Walk.lean

@@ -1417,7 +1417,7 @@ theorem reverse_transfer (hp) :
 
 /-! ### Inducing a walk -/
 
-variable {s : Set V}
+variable {s s' : Set V}
 
 variable (s) in
 /-- A walk in `G` which is fully contained in a set `s` of vertices lifts to a walk of `G[s]`. -/
@@ -1442,6 +1442,11 @@ protected def induce {u v : V} :
   | .nil, hw => rfl
   | .cons (v := u') huu' w, hw => by simp [map_induce]
 
+lemma map_induce_induceHomOfLE (hs : s ⊆ s') {u v : V} : ∀ (w : G.Walk u v) (hw),
+    (w.induce s hw).map (G.induceHomOfLE hs).toHom = w.induce s' (subset_trans hw hs)
+  | .nil, hw => rfl
+  | .cons (v := u') huu' w, hw => by simp [map_induce_induceHomOfLE]
+
 end Walk
 
 /-! ## Deleting edges -/