Theorem: Network.Graph.Path.Sibling.iff_eq_prefix (Runtime/Network/Graph/Path/Sibling.lean)

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ ↔ prefix? path₁ = prefix? path₂
Tactic:
constructor
State after:
case mp
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂

case mpr
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ prefix? path₁ = prefix? path₂ → path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂
Tactic:
case mp =>
  cases path₁ <;> cases path₂
  case nil.nil => simp
  case cons.cons => intro h; cases h; simp_all [Succ]
  case nil.cons => intro h; cases h; case _ h _ => have := h.isCons; contradiction
  case cons.nil => intro h; cases h; case _ h   => have := h.isCons; contradiction
State after:
no goals

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ prefix? path₁ = prefix? path₂ → path₁ ≂ path₂
Tactic:
case mpr =>
  intro h
  by_cases path₁.prefix?.isSome
  case inr hp =>
    have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₁
    rw [h] at hp
    have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₂
    simp [hc₁, hc₂, Sibling.nil]
  case inl hp =>
    have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
    rw [h] at hp
    have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
    simp_all
    exact Sibling.cons hp₁ hp₂
State after:
no goals

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ path₁ ≂ path₂ → prefix? path₁ = prefix? path₂
Tactic:
cases path₁ <;> cases path₂
State after:
case nil.nil
graph✝ : Graph
a✝ : Class graph✝
⊢ Path.nil ≂ Path.nil → prefix? Path.nil = prefix? Path.nil

case nil.cons
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.nil ≂ Path.cons child✝ a✝ → prefix? Path.nil = prefix? (Path.cons child✝ a✝)

case cons.nil
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝ a✝ ≂ Path.nil → prefix? (Path.cons child✝ a✝) = prefix? Path.nil

case cons.cons
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝ → prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)

State before:
graph✝ : Graph
a✝ : Class graph✝
⊢ Path.nil ≂ Path.nil → prefix? Path.nil = prefix? Path.nil
Tactic:
case nil.nil => simp
State after:
no goals

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝ → prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Tactic:
case cons.cons => intro h; cases h; simp_all [Succ]
State after:
no goals

State before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.nil ≂ Path.cons child✝ a✝ → prefix? Path.nil = prefix? (Path.cons child✝ a✝)
Tactic:
case nil.cons => intro h; cases h; case _ h _ => have := h.isCons; contradiction
State after:
no goals

State before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝ a✝ ≂ Path.nil → prefix? (Path.cons child✝ a✝) = prefix? Path.nil
Tactic:
case cons.nil => intro h; cases h; case _ h   => have := h.isCons; contradiction
State after:
no goals

State before:
graph✝ : Graph
a✝ : Class graph✝
⊢ Path.nil ≂ Path.nil → prefix? Path.nil = prefix? Path.nil
Tactic:
simp
State after:
no goals

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝ → prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Tactic:
intro h
State after:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝
⊢ prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝¹ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝²
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝¹ a✝¹ ≂ Path.cons child✝ a✝
⊢ prefix? (Path.cons child✝¹ a✝¹) = prefix? (Path.cons child✝ a✝)
Tactic:
cases h
State after:
case cons
graph✝ : Graph
a✝⁴ : Class graph✝
child✝¹ : Class.Child a✝⁴
a✝³ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝⁴
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝⁴
a✝¹ : Path.cons child✝¹ a✝³ ≻ parent✝
a✝ : Path.cons child✝ a✝² ≻ parent✝
⊢ prefix? (Path.cons child✝¹ a✝³) = prefix? (Path.cons child✝ a✝²)

State before:
case cons
graph✝ : Graph
a✝⁴ : Class graph✝
child✝¹ : Class.Child a✝⁴
a✝³ : Path graph✝ (Class.Child.class child✝¹)
child✝ : Class.Child a✝⁴
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝⁴
a✝¹ : Path.cons child✝¹ a✝³ ≻ parent✝
a✝ : Path.cons child✝ a✝² ≻ parent✝
⊢ prefix? (Path.cons child✝¹ a✝³) = prefix? (Path.cons child✝ a✝²)
Tactic:
simp_all [Succ]
State after:
no goals

State before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.nil ≂ Path.cons child✝ a✝ → prefix? Path.nil = prefix? (Path.cons child✝ a✝)
Tactic:
intro h
State after:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.nil ≂ Path.cons child✝ a✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝)

State before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.nil ≂ Path.cons child✝ a✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝)
Tactic:
cases h
State after:
case cons
graph✝ : Graph
a✝³ : Class graph✝
child✝ : Class.Child a✝³
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝³
a✝¹ : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝² ≻ parent✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝²)

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
Tactic:
case _ h _ => have := h.isCons; contradiction
State after:
no goals

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
Tactic:
have := h.isCons
State after:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
h : Path.nil ≻ parent✝
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? Path.nil = prefix? (Path.cons child✝ a✝¹)
Tactic:
contradiction
State after:
no goals

State before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
⊢ Path.cons child✝ a✝ ≂ Path.nil → prefix? (Path.cons child✝ a✝) = prefix? Path.nil
Tactic:
intro h
State after:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝ a✝ ≂ Path.nil
⊢ prefix? (Path.cons child✝ a✝) = prefix? Path.nil

State before:
graph✝ : Graph
a✝¹ : Class graph✝
child✝ : Class.Child a✝¹
a✝ : Path graph✝ (Class.Child.class child✝)
h : Path.cons child✝ a✝ ≂ Path.nil
⊢ prefix? (Path.cons child✝ a✝) = prefix? Path.nil
Tactic:
cases h
State after:
case cons
graph✝ : Graph
a✝³ : Class graph✝
child✝ : Class.Child a✝³
a✝² : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝³
a✝¹ : Path.cons child✝ a✝² ≻ parent✝
a✝ : Path.nil ≻ parent✝
⊢ prefix? (Path.cons child✝ a✝²) = prefix? Path.nil

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil
Tactic:
case _ h   => have := h.isCons; contradiction
State after:
no goals

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil
Tactic:
have := h.isCons
State after:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil

State before:
graph✝ : Graph
a✝² : Class graph✝
child✝ : Class.Child a✝²
a✝¹ : Path graph✝ (Class.Child.class child✝)
parent✝ : Path graph✝ a✝²
a✝ : Path.cons child✝ a✝¹ ≻ parent✝
h : Path.nil ≻ parent✝
this : isCons Path.nil = true
⊢ prefix? (Path.cons child✝ a✝¹) = prefix? Path.nil
Tactic:
contradiction
State after:
no goals

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
⊢ prefix? path₁ = prefix? path₂ → path₁ ≂ path₂
Tactic:
intro h
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
⊢ path₁ ≂ path₂
Tactic:
by_cases path₁.prefix?.isSome
State after:
case inl
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
h✝ : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂

case inr
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
h✝ : ¬Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
case inr hp =>
  have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₁
  rw [h] at hp
  have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp; simp at hc₂
  simp [hc₁, hc₂, Sibling.nil]
State after:
no goals

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
case inl hp =>
  have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
  rw [h] at hp
  have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
  simp_all
  exact Sibling.cons hp₁ hp₂
State after:
no goals

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
have hc₁ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : isNil path₁ = true
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : isNil path₁ = true
⊢ path₁ ≂ path₂
Tactic:
simp at hc₁
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₁) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂
Tactic:
rw [h] at hp
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
⊢ path₁ ≂ path₂
Tactic:
have hc₂ := isNil_iff_not_isCons.mpr <| mt prefix?_isSome_iff_isCons.mpr hp
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : isNil path₂ = true
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : isNil path₂ = true
⊢ path₁ ≂ path₂
Tactic:
simp at hc₂
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : path₂ = Path.nil
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : ¬Option.isSome (prefix? path₂) = true
hc₁ : path₁ = Path.nil
hc₂ : path₂ = Path.nil
⊢ path₁ ≂ path₂
Tactic:
simp [hc₁, hc₂, Sibling.nil]
State after:
no goals

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
⊢ path₁ ≂ path₂
Tactic:
have ⟨_, hp₁⟩ := Option.isSome_iff_exists.mp hp
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₁) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂
Tactic:
rw [h] at hp
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝
⊢ path₁ ≂ path₂
Tactic:
have ⟨_, hp₂⟩ := Option.isSome_iff_exists.mp hp
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝¹ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝¹
w✝ : Path graph✝ a✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ : Path graph✝ a✝
h : prefix? path₁ = prefix? path₂
hp : Option.isSome (prefix? path₂) = true
w✝¹ : Path graph✝ a✝
hp₁ : prefix? path₁ = some w✝¹
w✝ : Path graph✝ a✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂
Tactic:
simp_all
State after:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ w✝¹ w✝ : Path graph✝ a✝
h : w✝¹ = w✝
hp₁ : prefix? path₁ = some w✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂

State before:
graph✝ : Graph
a✝ : Class graph✝
path₁ path₂ w✝¹ w✝ : Path graph✝ a✝
h : w✝¹ = w✝
hp₁ : prefix? path₁ = some w✝
hp₂ : prefix? path₂ = some w✝
⊢ path₁ ≂ path₂
Tactic:
exact Sibling.cons hp₁ hp₂
State after:
no goals