Theorem: Graph.left_append_step (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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
rel : Reduction b₁ b₂
⊢ [[a ++ b₁]] = [[a ++ b₂]]
Tactic:
induction rel
State after:
case step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[a ++ (p₁✝ ++ p₂✝)]]

State before:
case step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ (p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝))]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
repeat (rw [← append_assoc])
State after:
case step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]

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

State before:
case step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
(rw [← append_assoc])
State after:
case step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]

State before:
case step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ (p₁✝ ++ p₂✝)]]
Tactic:
rw [← append_assoc]
State after:
case step
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✝
v w u : V
a : EdgePath G v w
b₁ b₂ : EdgePath G w u
u✝ u'✝ : V
e✝ : EdgeBetween G u✝ u'✝
p₁✝ : EdgePath G w u✝
p₂✝ : EdgePath G u✝ u
⊢ [[a ++ p₁✝ ++ cons e✝ (cons (EdgeBetween.bar e✝) p₂✝)]] = [[a ++ p₁✝ ++ p₂✝]]