Theorem: Network.Graph.Path.Sibling.refl (Runtime/Network/Graph/Path/Sibling.lean)

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
subpath : Path graph (Class.Child.class child✝)
⊢ Path.cons child✝ subpath ≂ Path.cons child✝ subpath
Tactic:
have ⟨_, h⟩ := Succ.cons subpath
State after:
graph : Graph
start : Class graph
child✝ : Class.Child start
subpath : Path graph (Class.Child.class child✝)
w✝ : Path graph start
h : Path.cons child✝ subpath ≻ w✝
⊢ Path.cons child✝ subpath ≂ Path.cons child✝ subpath

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
subpath : Path graph (Class.Child.class child✝)
w✝ : Path graph start
h : Path.cons child✝ subpath ≻ w✝
⊢ Path.cons child✝ subpath ≂ Path.cons child✝ subpath
Tactic:
exact cons h h
State after:
no goals