Theorem: Network.Graph.Path.prefix?_isSome_iff_isCons (Runtime/Network/Graph/Path/Subpaths.lean)

State before:
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true ↔ isCons path = true
Tactic:
constructor
State after:
case mp
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true

case mpr
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true

State before:
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true
Tactic:
case mp =>
  intro h
  induction path
  case nil => simp [prefix?] at h
  case cons child₁ subpath₁ hi =>
    cases subpath₁
    case nil => rfl
    case cons child₂ subpath₂ => simp [isCons]
State after:
no goals

State before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true
Tactic:
case mpr =>
  intro h
  induction path
  case nil =>
    have ⟨_, _, _⟩ := isCons_def.mp h
    contradiction
  case cons child₁ subpath₁ hi =>
    cases subpath₁
    case nil => simp [prefix?, Option.isSome]
    case cons child₂ subpath₂ =>
      specialize hi isCons_of_cons
      have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
      simp [prefix?, hi, Option.isSome_iff_exists]
      exists .cons child₁ subpath
State after:
no goals

State before:
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true
Tactic:
intro h
State after:
graph : Graph
start : Class graph
path : Path graph start
h : Option.isSome (prefix? path) = true
⊢ isCons path = true

State before:
graph : Graph
start : Class graph
path : Path graph start
h : Option.isSome (prefix? path) = true
⊢ isCons path = true
Tactic:
induction path
State after:
case nil
graph : Graph
start x✝ : Class graph
h : Option.isSome (prefix? nil) = true
⊢ isCons nil = true

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : Option.isSome (prefix? a✝) = true → isCons a✝ = true
h : Option.isSome (prefix? (cons child✝ a✝)) = true
⊢ isCons (cons child✝ a✝) = true

State before:
graph : Graph
start x✝ : Class graph
h : Option.isSome (prefix? nil) = true
⊢ isCons nil = true
Tactic:
case nil => simp [prefix?] at h
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : Option.isSome (prefix? subpath₁) = true → isCons subpath₁ = true
h : Option.isSome (prefix? (cons child₁ subpath₁)) = true
⊢ isCons (cons child₁ subpath₁) = true
Tactic:
case cons child₁ subpath₁ hi =>
  cases subpath₁
  case nil => rfl
  case cons child₂ subpath₂ => simp [isCons]
State after:
no goals

State before:
graph : Graph
start x✝ : Class graph
h : Option.isSome (prefix? nil) = true
⊢ isCons nil = true
Tactic:
simp [prefix?] at h
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
subpath₁ : Path graph (Class.Child.class child₁)
hi : Option.isSome (prefix? subpath₁) = true → isCons subpath₁ = true
h : Option.isSome (prefix? (cons child₁ subpath₁)) = true
⊢ isCons (cons child₁ subpath₁) = true
Tactic:
cases subpath₁
State after:
case nil
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : Option.isSome (prefix? nil) = true → isCons nil = true
h : Option.isSome (prefix? (cons child₁ nil)) = true
⊢ isCons (cons child₁ nil) = true

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 : Option.isSome (prefix? (cons child✝ a✝)) = true → isCons (cons child✝ a✝) = true
h : Option.isSome (prefix? (cons child₁ (cons child✝ a✝))) = true
⊢ isCons (cons child₁ (cons child✝ a✝)) = true

State before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : Option.isSome (prefix? nil) = true → isCons nil = true
h : Option.isSome (prefix? (cons child₁ nil)) = true
⊢ isCons (cons child₁ nil) = true
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 : Option.isSome (prefix? (cons child₂ subpath₂)) = true → isCons (cons child₂ subpath₂) = true
h : Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
⊢ isCons (cons child₁ (cons child₂ subpath₂)) = true
Tactic:
case cons child₂ subpath₂ => simp [isCons]
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : Option.isSome (prefix? nil) = true → isCons nil = true
h : Option.isSome (prefix? (cons child₁ nil)) = true
⊢ isCons (cons child₁ nil) = true
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 : Option.isSome (prefix? (cons child₂ subpath₂)) = true → isCons (cons child₂ subpath₂) = true
h : Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
⊢ isCons (cons child₁ (cons child₂ subpath₂)) = true
Tactic:
simp [isCons]
State after:
no goals

State before:
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true
Tactic:
intro h
State after:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ Option.isSome (prefix? path) = true

State before:
graph : Graph
start : Class graph
path : Path graph start
h : isCons path = true
⊢ Option.isSome (prefix? path) = true
Tactic:
induction path
State after:
case nil
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Option.isSome (prefix? nil) = true

case cons
graph : Graph
start start✝ : Class graph
child✝ : Class.Child start✝
a✝ : Path graph (Class.Child.class child✝)
a_ih✝ : isCons a✝ = true → Option.isSome (prefix? a✝) = true
h : isCons (cons child✝ a✝) = true
⊢ Option.isSome (prefix? (cons child✝ a✝)) = true

State before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Option.isSome (prefix? nil) = true
Tactic:
case nil =>
  have ⟨_, _, _⟩ := isCons_def.mp h
  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 : isCons subpath₁ = true → Option.isSome (prefix? subpath₁) = true
h : isCons (cons child₁ subpath₁) = true
⊢ Option.isSome (prefix? (cons child₁ subpath₁)) = true
Tactic:
case cons child₁ subpath₁ hi =>
  cases subpath₁
  case nil => simp [prefix?, Option.isSome]
  case cons child₂ subpath₂ =>
    specialize hi isCons_of_cons
    have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
    simp [prefix?, hi, Option.isSome_iff_exists]
    exists .cons child₁ subpath
State after:
no goals

State before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
⊢ Option.isSome (prefix? nil) = true
Tactic:
have ⟨_, _, _⟩ := isCons_def.mp h
State after:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
w✝¹ : Class.Child x✝
w✝ : Path graph (Class.Child.class w✝¹)
h✝ : nil = cons w✝¹ w✝
⊢ Option.isSome (prefix? nil) = true

State before:
graph : Graph
start x✝ : Class graph
h : isCons nil = true
w✝¹ : Class.Child x✝
w✝ : Path graph (Class.Child.class w✝¹)
h✝ : nil = cons w✝¹ w✝
⊢ Option.isSome (prefix? nil) = true
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 : isCons subpath₁ = true → Option.isSome (prefix? subpath₁) = true
h : isCons (cons child₁ subpath₁) = true
⊢ Option.isSome (prefix? (cons child₁ subpath₁)) = true
Tactic:
cases subpath₁
State after:
case nil
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : isCons nil = true → Option.isSome (prefix? nil) = true
h : isCons (cons child₁ nil) = true
⊢ Option.isSome (prefix? (cons child₁ nil)) = true

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 : isCons (cons child✝ a✝) = true → Option.isSome (prefix? (cons child✝ a✝)) = true
h : isCons (cons child₁ (cons child✝ a✝)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child✝ a✝))) = true

State before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : isCons nil = true → Option.isSome (prefix? nil) = true
h : isCons (cons child₁ nil) = true
⊢ Option.isSome (prefix? (cons child₁ nil)) = true
Tactic:
case nil => simp [prefix?, Option.isSome]
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 : isCons (cons child₂ subpath₂) = true → Option.isSome (prefix? (cons child₂ subpath₂)) = true
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Tactic:
case cons child₂ subpath₂ =>
  specialize hi isCons_of_cons
  have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
  simp [prefix?, hi, Option.isSome_iff_exists]
  exists .cons child₁ subpath
State after:
no goals

State before:
graph : Graph
start start✝ : Class graph
child₁ : Class.Child start✝
hi : isCons nil = true → Option.isSome (prefix? nil) = true
h : isCons (cons child₁ nil) = true
⊢ Option.isSome (prefix? (cons child₁ nil)) = true
Tactic:
simp [prefix?, Option.isSome]
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 : isCons (cons child₂ subpath₂) = true → Option.isSome (prefix? (cons child₂ subpath₂)) = true
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Tactic:
specialize hi isCons_of_cons
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₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi : Option.isSome (prefix? (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true

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₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi : Option.isSome (prefix? (cons child₂ subpath₂)) = true
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Tactic:
have ⟨subpath, hi⟩ := Option.isSome_iff_exists.mp hi
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₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true

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₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ Option.isSome (prefix? (cons child₁ (cons child₂ subpath₂))) = true
Tactic:
simp [prefix?, hi, Option.isSome_iff_exists]
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₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ ∃ a,
    (do
        let x ← some subpath
        some (cons child₁ x)) =
      some a

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₂)
h : isCons (cons child₁ (cons child₂ subpath₂)) = true
hi✝ : Option.isSome (prefix? (cons child₂ subpath₂)) = true
subpath : Path graph (Class.Child.class child₁)
hi : prefix? (cons child₂ subpath₂) = some subpath
⊢ ∃ a,
    (do
        let x ← some subpath
        some (cons child₁ x)) =
      some a
Tactic:
exists .cons child₁ subpath
State after:
no goals