Theorem: Network.Graph.Path.prefix?_cons_eq_cons_prefix? (Runtime/Network/Graph/Path/Subpaths.lean)

State before:
graph : Graph
start : Class graph
child : Class.Child start
subpath subprefix : Path graph (Class.Child.class child)
⊢ prefix? subpath = some subprefix → prefix? (cons child subpath) = some (cons child subprefix)
Tactic:
intro h
State after:
graph : Graph
start : Class graph
child : Class.Child start
subpath subprefix : Path graph (Class.Child.class child)
h : prefix? subpath = some subprefix
⊢ prefix? (cons child subpath) = some (cons child subprefix)

State before:
graph : Graph
start : Class graph
child : Class.Child start
subpath subprefix : Path graph (Class.Child.class child)
h : prefix? subpath = some subprefix
⊢ prefix? (cons child subpath) = some (cons child subprefix)
Tactic:
cases subpath
State after:
case nil
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
h : prefix? nil = some subprefix
⊢ prefix? (cons child nil) = some (cons child subprefix)

case cons
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some subprefix
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child subprefix)

State before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
h : prefix? nil = some subprefix
⊢ prefix? (cons child nil) = some (cons child subprefix)
Tactic:
case nil => simp [prefix?] at h
State after:
no goals

State before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ prefix? (cons child (cons child' subpath)) = some (cons child subprefix)
Tactic:
case cons child' subpath => simp [prefix?, h]; rfl
State after:
no goals

State before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
h : prefix? nil = some subprefix
⊢ prefix? (cons child nil) = some (cons child subprefix)
Tactic:
simp [prefix?] at h
State after:
no goals

State before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ prefix? (cons child (cons child' subpath)) = some (cons child subprefix)
Tactic:
simp [prefix?, h]
State after:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ (do
      let x ← some subprefix
      some (cons child x)) =
    some (cons child subprefix)

State before:
graph : Graph
start : Class graph
child : Class.Child start
subprefix : Path graph (Class.Child.class child)
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
h : prefix? (cons child' subpath) = some subprefix
⊢ (do
      let x ← some subprefix
      some (cons child x)) =
    some (cons child subprefix)
Tactic:
rfl
State after:
no goals