Theorem: Network.Graph.Path.split_class (Runtime/Network/Graph/Path/Subpaths.lean)

State before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ Class.Child.class (split path h).snd = class path
Tactic:
induction path
State after:
case nil
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Class.Child.class (split nil h).snd = class nil

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : ∀ (h : isCons a✝ = true), Class.Child.class (split a✝ h).snd = class a✝
h : isCons (cons child✝ a✝) = true
⊢ Class.Child.class (split (cons child✝ a✝) h).snd = class (cons child✝ a✝)

State before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Class.Child.class (split nil h).snd = class nil
Tactic:
case nil => contradiction
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
subpath : Path graph (Class.Child.class child)
hi : ∀ (h : isCons subpath = true), Class.Child.class (split subpath h).snd = class subpath
h : isCons (cons child subpath) = true
⊢ Class.Child.class (split (cons child subpath) h).snd = class (cons child subpath)
Tactic:
case cons child subpath hi =>
  cases subpath
  case nil => rfl
  case cons child' subpath => rw [split]; exact hi h
State after:
no goals

State before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Class.Child.class (split nil h).snd = class nil
Tactic:
contradiction
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
subpath : Path graph (Class.Child.class child)
hi : ∀ (h : isCons subpath = true), Class.Child.class (split subpath h).snd = class subpath
h : isCons (cons child subpath) = true
⊢ Class.Child.class (split (cons child subpath) h).snd = class (cons child subpath)
Tactic:
cases subpath
State after:
case nil
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
hi : ∀ (h : isCons nil = true), Class.Child.class (split nil h).snd = class nil
h : isCons (cons child nil) = true
⊢ Class.Child.class (split (cons child nil) h).snd = class (cons child nil)

case cons
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
hi : ∀ (h : isCons (cons child✝ a✝) = true), Class.Child.class (split (cons child✝ a✝) h).snd = class (cons child✝ a✝)
h : isCons (cons child (cons child✝ a✝)) = true
⊢ Class.Child.class (split (cons child (cons child✝ a✝)) h).snd = class (cons child (cons child✝ a✝))

State before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
hi : ∀ (h : isCons nil = true), Class.Child.class (split nil h).snd = class nil
h : isCons (cons child nil) = true
⊢ Class.Child.class (split (cons child nil) h).snd = class (cons child nil)
Tactic:
case nil => rfl
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class (split (cons child (cons child' subpath)) h).snd = class (cons child (cons child' subpath))
Tactic:
case cons child' subpath => rw [split]; exact hi h
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
hi : ∀ (h : isCons nil = true), Class.Child.class (split nil h).snd = class nil
h : isCons (cons child nil) = true
⊢ Class.Child.class (split (cons child nil) h).snd = class (cons child nil)
Tactic:
rfl
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class (split (cons child (cons child' subpath)) h).snd = class (cons child (cons child' subpath))
Tactic:
rw [split]
State after:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class
      (match split (cons child' subpath) (_ : isCons (cons child' subpath) = true) with
        | { fst := sub, snd := cls } => { fst := cons child sub, snd := cls }).snd =
    class (cons child (cons child' subpath))

State before:
graph : Graph
start start✝ : Class graph
child : Class.Child start✝
child' : Class.Child (Class.Child.class child)
subpath : Path graph (Class.Child.class child')
hi :
  ∀ (h : isCons (cons child' subpath) = true),
    Class.Child.class (split (cons child' subpath) h).snd = class (cons child' subpath)
h : isCons (cons child (cons child' subpath)) = true
⊢ Class.Child.class
      (match split (cons child' subpath) (_ : isCons (cons child' subpath) = true) with
        | { fst := sub, snd := cls } => { fst := cons child sub, snd := cls }).snd =
    class (cons child (cons child' subpath))
Tactic:
exact hi h
State after:
no goals