Theorem: Graph.terminal_eq_of_toList_eq (Lectures/Graph.lean)

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₁ : EdgePath G v₁ w₁
p₂ : EdgePath G v₂ w₂
⊢ toList p₁ = toList p₂ → v₁ = v₂ → w₁ = w₂
Tactic:
induction p₁ with
| nil v₁' =>
  match p₂ with
  | EdgePath.nil v => 
    intro h heq
    rw [nil_toList] at h      
    exact heq
  | EdgePath.cons e₂ p₂  =>
    intro h
    simp [cons_toList, nil_toList] at h
| cons e p₁' ih =>    
  intro h heq
  match p₂ with
  | EdgePath.nil w =>
    simp [cons_toList, nil_toList] at h
  | EdgePath.cons e₂ p₂' =>
    simp [cons_toList] at h
    apply terminal_eq_of_toList_eq p₁' p₂' h.right
    rw [←e₂.term_eq, ←e.term_eq, h.left]
State after:
no goals

State before:
case nil
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' : V
⊢ toList (nil v₁') = toList p₂ → v₁' = v₂ → v₁' = w₂
Tactic:
match p₂ with
| EdgePath.nil v => 
  intro h heq
  rw [nil_toList] at h      
  exact heq
| EdgePath.cons e₂ p₂  =>
  intro h
  simp [cons_toList, nil_toList] at h
State after:
no goals

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
⊢ toList (nil v₁') = toList (nil v) → v₁' = v → v₁' = v
Tactic:
intro h heq
State after:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : toList (nil v₁') = toList (nil v)
heq : v₁' = v
⊢ v₁' = v

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : toList (nil v₁') = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Tactic:
rw [nil_toList] at h
State after:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : [] = toList (nil v)
heq : v₁' = v
⊢ v₁' = v

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v✝ w : V
e : EdgeBetween G✝ v✝ w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v₁' v : V
h : [] = toList (nil v)
heq : v₁' = v
⊢ v₁' = v
Tactic:
exact heq
State after:
no goals

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
⊢ toList (nil v₁') = toList (cons e₂ p₂) → v₁' = v₂ → v₁' = w₂
Tactic:
intro h
State after:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
h : toList (nil v₁') = toList (cons e₂ p₂)
⊢ v₁' = v₂ → v₁' = w₂

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂✝ : EdgePath G v₂✝ w₂✝
v₁' w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂ : EdgePath G w✝ w₂
h : toList (nil v₁') = toList (cons e₂ p₂)
⊢ v₁' = v₂ → v₁' = w₂
Tactic:
simp [cons_toList, nil_toList] at h
State after:
no goals

State before:
case cons
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
⊢ toList (cons e p₁') = toList p₂ → v✝ = v₂ → u✝ = w₂
Tactic:
intro h heq
State after:
case cons
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList p₂
heq : v✝ = v₂
⊢ u✝ = w₂

State before:
case cons
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList p₂
heq : v✝ = v₂
⊢ u✝ = w₂
Tactic:
match p₂ with
| EdgePath.nil w =>
  simp [cons_toList, nil_toList] at h
| EdgePath.cons e₂ p₂' =>
  simp [cons_toList] at h
  apply terminal_eq_of_toList_eq p₁' p₂' h.right
  rw [←e₂.term_eq, ←e.term_eq, h.left]
State after:
no goals

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v w✝¹ : V
e✝ : EdgeBetween G✝ v w✝¹
G : Graph V E
v₁ v₂ w₁ w₂ : V
p₂ : EdgePath G v₂ w₂
v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
w : V
ih : toList p₁' = toList (nil w) → w✝ = w → u✝ = w
h : toList (cons e p₁') = toList (nil w)
heq : v✝ = w
⊢ u✝ = w
Tactic:
simp [cons_toList, nil_toList] at h
State after:
no goals

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList (cons e₂ p₂')
heq : v✝ = v₂
⊢ u✝ = w₂
Tactic:
simp [cons_toList] at h
State after:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ u✝ = w₂

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ u✝ = w₂
Tactic:
apply terminal_eq_of_toList_eq p₁' p₂' h.right
State after:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ w✝¹ = w✝

State before:
V : Type u
E : Type v
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ w✝¹ = w✝
Tactic:
rw [←e₂.term_eq, ←e.term_eq, h.left]
State after:
no goals