Theorem: Digraph.Walk.map_eq_of_eq (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f'✝ : G' →g G''
u v u' v' : V
p : Walk G u v
f f' : G →g G'
h : f = f'
⊢ Walk.map f p = Walk.copy (Walk.map f' p) (_ : ↑f' u = ↑f u) (_ : ↑f' v = ↑f v)
Tactic:
subst_vars
State after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f : G →g G'
f'✝ : G' →g G''
u v u' v' : V
p : Walk G u v
f' : G →g G'
⊢ Walk.map f' p = Walk.copy (Walk.map f' p) (_ : ↑f' u = ↑f' u) (_ : ↑f' v = ↑f' v)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f : G →g G'
f'✝ : G' →g G''
u v u' v' : V
p : Walk G u v
f' : G →g G'
⊢ Walk.map f' p = Walk.copy (Walk.map f' p) (_ : ↑f' u = ↑f' u) (_ : ↑f' v = ↑f' v)
Tactic:
rfl
State after:
no goals