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

State before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class (suffix path h) = class path
Tactic:
rw [suffix]
State after:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class
      (match path, h with
      | nil, h => Bool.noConfusion h
      | cons child subpath, h => subpath) =
    class path

State before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ class
      (match path, h with
      | nil, h => Bool.noConfusion h
      | cons child subpath, h => subpath) =
    class path
Tactic:
split
State after:
case h_1
graph : Graph
start : Class graph
path✝ : Path graph start
x✝¹ : isCons path✝ = true
x✝ : isCons nil = true
⊢ class (Bool.noConfusion x✝) = class nil

case h_2
graph : Graph
start : Class graph
path✝ : Path graph start
x✝¹ : isCons path✝ = true
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
x✝ : isCons (cons child✝ a✝) = true
⊢ class a✝ = class (cons child✝ a✝)

State before:
graph : Graph
start : Class graph
path✝ : Path graph start
x✝ : isCons path✝ = true
h : isCons nil = true
⊢ class (Bool.noConfusion h) = class nil
Tactic:
case _ h => simp [isCons] at h
State after:
no goals

State before:
graph : Graph
start : Class graph
path✝ : Path graph start
x✝ : isCons path✝ = true
h : isCons nil = true
⊢ class (Bool.noConfusion h) = class nil
Tactic:
simp [isCons] at h
State after:
no goals