Theorem: Network.Graph.Path.Child.parent_eq_nil_class (Runtime/Network/Graph/Path/Child.lean)

State before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
⊢ child.val = cons c nil → start = class path
Tactic:
intro h
State after:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
⊢ start = class path

State before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
⊢ start = class path
Tactic:
have h' := child.property
State after:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : child.val ≻ path
⊢ start = class path

State before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : child.val ≻ path
⊢ start = class path
Tactic:
simp [Succ, h, prefix?] at h'
State after:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : nil = path
⊢ start = class path

State before:
graph : Graph
start : Class graph
c : Class.Child start
path : Path graph start
child : Child path
h : child.val = cons c nil
h' : nil = path
⊢ start = class path
Tactic:
simp [←h']
State after:
no goals