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

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✝ w v : V
p₂ : EdgePath G v v
⊢ toList (nil v) = toList p₂ → nil v = p₂
Tactic:
match p₂ with
| EdgePath.nil v => 
  intro h
  rw [nil_toList] at h      
| 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✝¹ w v✝ : V
p₂ : EdgePath G v✝ v✝
v : V
⊢ toList (nil v) = toList (nil v) → nil v = nil v
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✝¹ w v✝ : V
p₂ : EdgePath G v✝ v✝
v : V
h : toList (nil v) = toList (nil v)
⊢ nil v = nil 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✝¹ w v✝ : V
p₂ : EdgePath G v✝ v✝
v : V
h : toList (nil v) = toList (nil v)
⊢ nil v = nil v
Tactic:
rw [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✝¹ w v✝ : V
p₂✝ : EdgePath G v✝ v✝
v w✝ : V
e₂ : EdgeBetween G v w✝
p₂ : EdgePath G w✝ v
⊢ toList (nil v) = toList (cons e₂ p₂) → nil v = cons e₂ p₂
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✝¹ w v✝ : V
p₂✝ : EdgePath G v✝ v✝
v w✝ : V
e₂ : EdgeBetween G v w✝
p₂ : EdgePath G w✝ v
h : toList (nil v) = toList (cons e₂ p₂)
⊢ nil v = cons e₂ p₂

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✝¹ w v✝ : V
p₂✝ : EdgePath G v✝ v✝
v w✝ : V
e₂ : EdgeBetween G v w✝
p₂ : EdgePath G w✝ v
h : toList (nil v) = toList (cons e₂ p₂)
⊢ nil v = cons e₂ p₂
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 w v✝ w✝ u✝ : V
e₁ : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G w✝ u✝), toList p₁' = toList p₂ → p₁' = p₂
p₂ : EdgePath G v✝ u✝
⊢ toList (cons e₁ p₁') = toList p₂ → cons e₁ p₁' = p₂
Tactic:
intro h
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 w v✝ w✝ u✝ : V
e₁ : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : ∀ (p₂ : EdgePath G w✝ u✝), toList p₁' = toList p₂ → p₁' = p₂
p₂ : EdgePath G v✝ u✝
h : toList (cons e₁ p₁') = toList p₂
⊢ cons e₁ p₁' = p₂

State before:
case cons.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 w✝¹ v✝ w✝ u✝ w : V
e₁ : EdgeBetween G w w✝
p₁' : EdgePath G w✝ w
ih : ∀ (p₂ : EdgePath G w✝ w), toList p₁' = toList p₂ → p₁' = p₂
h : toList (cons e₁ p₁') = toList (nil w)
⊢ cons e₁ p₁' = nil w
Tactic:
simp [cons_toList, nil_toList] at h
State after:
no goals

State before:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : toList (cons e₁ p₁') = toList (cons e₂ p₂')
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
simp [cons_toList] at h
State after:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ cons e₁ p₁' = cons e₂ p₂'

State before:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
have e1t := e₁.term_eq
State after:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
⊢ cons e₁ p₁' = cons e₂ p₂'

State before:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
have e2t := e₂.term_eq
State after:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'

State before:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₁.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
rw [h.1] at e1t
State after:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'

State before:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : τ G e₂.edge = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
rw [e1t] at e2t
State after:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'

State before:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
simp [h.2] at ih
State after:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ cons e₁ p₁' = cons e₂ p₂'

State before:
case cons.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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ cons e₁ p₁' = cons e₂ p₂'
Tactic:
apply cons_eq'
State after:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₂.edge = e₁.edge

case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'

case cons.cons.eq₂
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ w✝¹ = w✝

State before:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₂.edge = e₁.edge
Tactic:
symm
State after:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₁.edge = e₂.edge

State before:
case cons.cons.eq₁
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ e₁.edge = e₂.edge
Tactic:
exact h.1
State after:
no goals

State before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'
Tactic:
let step := ih (e2t ▸ p₂')
State after:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'

State before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ (_ : w✝ = w✝¹) ▸ p₂' = p₁'
Tactic:
symm
State after:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'

State before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Tactic:
have : p₁' = (e2t ▸ p₂')  := by
  apply step
  exact toList_cast_init p₂' (Eq.symm e2t)
State after:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
this : p₁' = (_ : w✝ = w✝¹) ▸ p₂'
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'

State before:
case cons.cons.eq₃
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
this : p₁' = (_ : w✝ = w✝¹) ▸ p₂'
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Tactic:
rw [this]
State after:
case cons.cons.eq₂
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = 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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ p₁' = (_ : w✝ = w✝¹) ▸ p₂'
Tactic:
apply step
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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂')

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 w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
step : toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂') → p₁' = (_ : w✝ = w✝¹) ▸ p₂' := ih (e2t.symm ▸ p₂')
⊢ toList p₂' = toList ((_ : w✝ = w✝¹) ▸ p₂')
Tactic:
exact toList_cast_init p₂' (Eq.symm e2t)
State after:
no goals

State before:
case cons.cons.eq₂
V : Type u
E : Type v
G✝ : Graph V E
u v✝² w✝² : V
e : EdgeBetween G✝ v✝² w✝²
G : Graph V E
v w v✝¹ w✝¹ u✝¹ v✝ w✝ u✝ : V
e₂ : EdgeBetween G v✝ w✝
p₂' : EdgePath G w✝ u✝
a_ih✝ :
  ∀ (e₁ : EdgeBetween G w✝ w✝¹) (p₁' : EdgePath G w✝¹ u✝),
    (∀ (p₂ : EdgePath G w✝¹ u✝), toList p₁' = toList p₂ → p₁' = p₂) →
      toList (cons e₁ p₁') = toList p₂' → cons e₁ p₁' = p₂'
e₁ : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
h : e₁.edge = e₂.edge ∧ toList p₁' = toList p₂'
e1t : τ G e₂.edge = w✝¹
e2t : w✝¹ = w✝
ih : ∀ (p₂ : EdgePath G w✝¹ u✝), toList p₂' = toList p₂ → p₁' = p₂
⊢ w✝¹ = w✝
Tactic:
assumption
State after:
no goals