Theorem: Network.Graph.Path.isCons_def (Runtime/Network/Graph/Path/Basic.lean)

State before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true ↔ ∃ child subpath, path = cons child subpath
Tactic:
cases path <;> simp [isCons]
State after:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ ∃ child subpath, child✝ = child ∧ HEq a✝ subpath

State before:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ ∃ child subpath, child✝ = child ∧ HEq a✝ subpath
Tactic:
exists ‹_›, ‹_›
State after:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ child✝ = child✝ ∧ HEq a✝ a✝

State before:
case cons
graph : Graph
start : Class graph
child✝ : Class.Child start
a✝ : Path graph (Class.Child.class child✝)
⊢ child✝ = child✝ ∧ HEq a✝ a✝
Tactic:
simp
State after:
no goals