Theorem: Graph.cons_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 w w' u : V
e : EdgeBetween G v w
e' : EdgeBetween G v w'
p : EdgePath G w u
p' : EdgePath G w' u
eq₁ : e.edge = e'.edge
eq₂ : w = w'
eq₃ : p = (_ : w' = w) ▸ p'
⊢ cons e' p' = cons e p
Tactic:
match p, p', e, e', eq₂ with
| p, p', e, e', rfl => 
  simp [cons_toList,  eq₃]
  ext
  symm
  assumption
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 w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ cons e' p' = cons e p
Tactic:
simp [cons_toList,  eq₃]
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 w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e' = e

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 w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e' = e
Tactic:
ext
State after:
case edge
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 w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e'.edge = e.edge

State before:
case edge
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 w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e'.edge = e.edge
Tactic:
symm
State after:
case edge
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 w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e.edge = e'.edge

State before:
case edge
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 w' u : V
e✝ : EdgeBetween G v w
e'✝ : EdgeBetween G v w'
p✝ : EdgePath G w u
p'✝ : EdgePath G w' u
eq₂ : w = w'
p p' : EdgePath G w u
e e' : EdgeBetween G v w
eq₁ : e.edge = e'.edge
eq₃ : p = (_ : w = w) ▸ p'
⊢ e.edge = e'.edge
Tactic:
assumption
State after:
no goals