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₃ : (_ : w = w') ▸ p = p'
⊢ cons e' p' = cons e p
Tactic:
match p, p', e, e', eq₂ with
| p, p', e, e', rfl => 
  simp [cons_toList, Eq.symm 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₃ : (_ : w' = w') ▸ p = p'
⊢ cons e' p' = cons e p
Tactic:
simp [cons_toList, Eq.symm 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₃ : (_ : w' = w') ▸ p = 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₃ : (_ : w' = w') ▸ p = 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₃ : (_ : w' = w') ▸ p = 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₃ : (_ : w' = w') ▸ p = 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₃ : (_ : w' = w') ▸ p = 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₃ : (_ : w' = w') ▸ p = p'
⊢ e.edge = e'.edge
Tactic:
assumption
State after:
no goals