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

State before:
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ ↔ prefix? (cons child path₁) = some (cons child path₂)
Tactic:
constructor
State after:
case mp
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ → prefix? (cons child path₁) = some (cons child path₂)

case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? (cons child path₁) = some (cons child path₂) → prefix? path₁ = some path₂

State before:
case mp
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ → prefix? (cons child path₁) = some (cons child path₂)

case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? (cons child path₁) = some (cons child path₂) → prefix? path₁ = some path₂
Tactic:
all_goals
  intro h
  cases path₁
  case nil => simp [prefix?] at h
State after:
case mp.cons
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)

case mpr.cons
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
⊢ prefix? (cons child✝ a✝) = some path₂

State before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
Tactic:
case mp.cons => simp [prefix?, h]; rfl
State after:
no goals

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
⊢ prefix? (cons child subpath) = some path₂
Tactic:
case mpr.cons child subpath =>
  have hs := prefix?_isSome_iff_isCons.mpr (@isCons_of_cons _ _ child subpath)
  have ⟨_, hs⟩ := Option.isSome_iff_exists.mp hs
  simp [hs, prefix?] at h ⊢
  injection h with h
  injection h
State after:
no goals

State before:
case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? (cons child path₁) = some (cons child path₂) → prefix? path₁ = some path₂
Tactic:
intro h
State after:
case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child path₁) = some (cons child path₂)
⊢ prefix? path₁ = some path₂

State before:
case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child path₁) = some (cons child path₂)
⊢ prefix? path₁ = some path₂
Tactic:
cases path₁
State after:
case mpr.nil
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child nil) = some (cons child path₂)
⊢ prefix? nil = some path₂

case mpr.cons
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
⊢ prefix? (cons child✝ a✝) = some path₂

State before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child nil) = some (cons child path₂)
⊢ prefix? nil = some path₂
Tactic:
case nil => simp [prefix?] at h
State after:
no goals

State before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
h : prefix? (cons child nil) = some (cons child path₂)
⊢ prefix? nil = some path₂
Tactic:
simp [prefix?] at h
State after:
no goals

State before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)
Tactic:
simp [prefix?, h]
State after:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ (do
      let x ← some path₂
      some (cons child x)) =
    some (cons child path₂)

State before:
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ (do
      let x ← some path₂
      some (cons child x)) =
    some (cons child path₂)
Tactic:
rfl
State after:
no goals

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
⊢ prefix? (cons child subpath) = some path₂
Tactic:
have hs := prefix?_isSome_iff_isCons.mpr (@isCons_of_cons _ _ child subpath)
State after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs : Option.isSome (prefix? (cons child subpath)) = true
⊢ prefix? (cons child subpath) = some path₂

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs : Option.isSome (prefix? (cons child subpath)) = true
⊢ prefix? (cons child subpath) = some path₂
Tactic:
have ⟨_, hs⟩ := Option.isSome_iff_exists.mp hs
State after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
⊢ prefix? (cons child subpath) = some path₂

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
h : prefix? (cons child✝ (cons child subpath)) = some (cons child✝ path₂)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
⊢ prefix? (cons child subpath) = some path₂
Tactic:
simp [hs, prefix?] at h ⊢
State after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h :
  (do
      let x ← some w✝
      some (cons child✝ x)) =
    some (cons child✝ path₂)
⊢ w✝ = path₂

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h :
  (do
      let x ← some w✝
      some (cons child✝ x)) =
    some (cons child✝ path₂)
⊢ w✝ = path₂
Tactic:
injection h with h
State after:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h : cons child✝ w✝ = cons child✝ path₂
⊢ w✝ = path₂

State before:
graph : Graph
start : Class graph
child✝ : Class.Child start
path₂ : Path graph (Class.Child.class child✝)
child : Class.Child (Class.Child.class child✝)
subpath : Path graph (Class.Child.class child)
hs✝ : Option.isSome (prefix? (cons child subpath)) = true
w✝ : Path graph (Class.Child.class child✝)
hs : prefix? (cons child subpath) = some w✝
h : cons child✝ w✝ = cons child✝ path₂
⊢ w✝ = path₂
Tactic:
injection h
State after:
no goals