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

State before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
⊢ cons c₁ (cons c₂ path₁) ≻ path₂ → Path.isCons path₂ = true
Tactic:
intro h
State after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
⊢ Path.isCons path₂ = true

State before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
⊢ Path.isCons path₂ = true
Tactic:
have ⟨subpath, hp⟩ := prefix?_isSome_iff_isCons.mpr (@isCons_of_cons _ _ c₂ path₁) |> Option.isSome_iff_exists.mp
State after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
⊢ Path.isCons path₂ = true

State before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
⊢ Path.isCons path₂ = true
Tactic:
simp [Succ, prefix?, hp] at h
State after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ Path.isCons path₂ = true

State before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ Path.isCons path₂ = true
Tactic:
simp [isCons_def]
State after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ ∃ child subpath, path₂ = cons child subpath

State before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ ∃ child subpath, path₂ = cons child subpath
Tactic:
exists c₁, subpath
State after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ path₂ = cons c₁ subpath

State before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h :
  (do
      let x ← some subpath
      some (cons c₁ x)) =
    some path₂
⊢ path₂ = cons c₁ subpath
Tactic:
injection h with h
State after:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h : cons c₁ subpath = path₂
⊢ path₂ = cons c₁ subpath

State before:
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
subpath : Path graph✝ (Class.Child.class c₁)
hp : prefix? (cons c₂ path₁) = some subpath
h : cons c₁ subpath = path₂
⊢ path₂ = cons c₁ subpath
Tactic:
exact h.symm
State after:
no goals