Theorem: Graph.EdgeBetween.bar_bar (GroupComp/Graph.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ bar (bar e) = e
Tactic:
ext
State after:
case edge
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ (bar (bar e)).edge = e.edge

State before:
case edge
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u v w : V
e : EdgeBetween G v w
⊢ (bar (bar e)).edge = e.edge
Tactic:
aesop (add norm simp [EdgeBetween.bar])
State after:
no goals