Theorem: SimpleGraph.Walk.init₀_copy (Untitled/Graphs/Walk.lean)

State before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
h1 : a = c
h2 : b = d
⊢ init₀ (Walk.copy p h1 h2) = init₀ p
Tactic:
subst_vars
State after:
V : Type u_1
V' : Type u_2
c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G c d
⊢ init₀ (Walk.copy p (_ : c = c) (_ : d = d)) = init₀ p

State before:
V : Type u_1
V' : Type u_2
c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G c d
⊢ init₀ (Walk.copy p (_ : c = c) (_ : d = d)) = init₀ p
Tactic:
rfl
State after:
no goals