Theorem: Network.Graph.Path.Succ.cons (Runtime/Network/Graph/Path/Succ.lean)

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
cases h : (Path.cons child path₁).prefix?
State after:
case none
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂

case some
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
val✝ : Path graph✝ cls✝
h : prefix? (Path.cons child path₁) = some val✝
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
case none =>
  have h : ¬(Path.cons child path₁).prefix?.isSome := by simp_all [Option.isSome_iff_exists]
  have := mt prefix?_isSome_iff_isCons.mpr h
  contradiction
State after:
no goals

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
pre : Path graph✝ cls✝
h : prefix? (Path.cons child path₁) = some pre
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
case some pre => exists pre
State after:
no goals

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
have h : ¬(Path.cons child path₁).prefix?.isSome := by simp_all [Option.isSome_iff_exists]
State after:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
have := mt prefix?_isSome_iff_isCons.mpr h
State after:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
this : ¬Path.isCons (Path.cons child path₁) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
this : ¬Path.isCons (Path.cons child path₁) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
contradiction
State after:
no goals

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h : prefix? (Path.cons child path₁) = none
⊢ ¬Option.isSome (prefix? (Path.cons child path₁)) = true
Tactic:
simp_all [Option.isSome_iff_exists]
State after:
no goals

State before:
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
pre : Path graph✝ cls✝
h : prefix? (Path.cons child path₁) = some pre
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
Tactic:
exists pre
State after:
no goals