Theorem: Graph.append_cons_cons_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
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Tactic:
have := append_cons_bar_cons e.bar p₁ p₂
State after:
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
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : [[p₁ ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) p₂)]] = [[p₁ ++ p₂]]
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]

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
u' : V
e : EdgeBetween G u' u
p₁ : EdgePath G v u
p₂ : EdgePath G u w
this : [[p₁ ++ cons (EdgeBetween.bar e) (cons (EdgeBetween.bar (EdgeBetween.bar e)) p₂)]] = [[p₁ ++ p₂]]
⊢ [[p₁ ++ cons (EdgeBetween.bar e) (cons e p₂)]] = [[p₁ ++ p₂]]
Tactic:
aesop
State after:
no goals