V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v' w' : V
p : Walk G v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ u ∈ support p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w v' w' : V
p : Walk G v w
hv : v = v'
hw : w = w'
h : u ∈ support (Walk.copy p hv hw)
⊢ u ∈ support p
subst_vars
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v' w' : V
p : Walk G v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ u ∈ support p
exact h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v' w' : V
p : Walk G v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ dropUntil (Walk.copy p (_ : v' = v') (_ : w' = w')) u h =
    Walk.copy (dropUntil p u (_ : u ∈ support p)) (_ : u = u) (_ : w' = w')
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w v' w' : V
p : Walk G v w
hv : v = v'
hw : w = w'
h : u ∈ support (Walk.copy p hv hw)
⊢ dropUntil (Walk.copy p hv hw) u h = Walk.copy (dropUntil p u (_ : u ∈ support p)) (_ : u = u) hw
subst_vars
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v' w' : V
p : Walk G v' w'
h : u ∈ support (Walk.copy p (_ : v' = v') (_ : w' = w'))
⊢ dropUntil (Walk.copy p (_ : v' = v') (_ : w' = w')) u h =
    Walk.copy (dropUntil p u (_ : u ∈ support p)) (_ : u = u) (_ : w' = w')
rfl