Theorem: Network.Graph.Path.extend_prefix?_eq_self (Runtime/Network/Graph/Path/Extend.lean)

State before:
graph : Graph
start : Class graph
path : Path graph start
leaf : Class.Child (class path)
⊢ prefix? (extend path leaf) = some path
Tactic:
induction path
State after:
case nil
graph : Graph
start x✝ : Class graph
leaf : Class.Child (class nil)
⊢ prefix? (extend nil leaf) = some nil

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : ∀ {leaf : Class.Child (class a✝)}, prefix? (extend a✝ leaf) = some a✝
leaf : Class.Child (class (cons child✝ a✝))
⊢ prefix? (extend (cons child✝ a✝) leaf) = some (cons child✝ a✝)

State before:
graph : Graph
start x✝ : Class graph
leaf : Class.Child (class nil)
⊢ prefix? (extend nil leaf) = some nil
Tactic:
case nil => simp [extend, prefix?]
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
subpath : Path graph (Class.Child.class child✝)
hi : ∀ {leaf : Class.Child (class subpath)}, prefix? (extend subpath leaf) = some subpath
leaf : Class.Child (class (cons child✝ subpath))
⊢ prefix? (extend (cons child✝ subpath) leaf) = some (cons child✝ subpath)
Tactic:
case cons subpath hi => simp [extend, prefix?_cons_eq_cons_prefix? hi]
State after:
no goals

State before:
graph : Graph
start x✝ : Class graph
leaf : Class.Child (class nil)
⊢ prefix? (extend nil leaf) = some nil
Tactic:
simp [extend, prefix?]
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
subpath : Path graph (Class.Child.class child✝)
hi : ∀ {leaf : Class.Child (class subpath)}, prefix? (extend subpath leaf) = some subpath
leaf : Class.Child (class (cons child✝ subpath))
⊢ prefix? (extend (cons child✝ subpath) leaf) = some (cons child✝ subpath)
Tactic:
simp [extend, prefix?_cons_eq_cons_prefix? hi]
State after:
no goals