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

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v w v' w' : V
h : G.Adj u v
p : Walk G v' w'
hv : v' = v
hw : w' = w
⊢ cons h (Walk.copy p hv hw) = Walk.copy (cons (_ : G.Adj u v') p) (_ : u = u) hw
Tactic:
subst_vars
State after:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v' w' : V
p : Walk G v' w'
h : G.Adj u v'
⊢ cons h (Walk.copy p (_ : v' = v') (_ : w' = w')) = Walk.copy (cons (_ : G.Adj u v') p) (_ : u = u) (_ : w' = w')

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v' w' : V
p : Walk G v' w'
h : G.Adj u v'
⊢ cons h (Walk.copy p (_ : v' = v') (_ : w' = w')) = Walk.copy (cons (_ : G.Adj u v') p) (_ : u = u) (_ : w' = w')
Tactic:
rfl
State after:
no goals