Theorem: Graph.reducedConcat_cancel_pair (GroupComp/Graph/ReducedPaths.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
⊢ p:+e:+EdgeBetween.bar e = p
Tactic:
have hyp' :=  reverse_reduced p hyp
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ p:+e:+EdgeBetween.bar e = p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ p:+e:+EdgeBetween.bar e = p
Tactic:
simp only [reducedConcat, EdgeBetween.bar_bar, reverse_reverse]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Tactic:
let lm :
  redCons e.bar.bar (redCons (EdgeBetween.bar e) (reverse p))
    = reverse p :=
  by
    apply cancelling_steps_redCons
    assumption
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons (EdgeBetween.bar (EdgeBetween.bar e)) (redCons (EdgeBetween.bar e) (reverse p)) = reverse p :=
  cancelling_steps_redCons (EdgeBetween.bar e) (reverse p) hyp'
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons (EdgeBetween.bar (EdgeBetween.bar e)) (redCons (EdgeBetween.bar e) (reverse p)) = reverse p :=
  cancelling_steps_redCons (EdgeBetween.bar e) (reverse p) hyp'
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Tactic:
simp at lm
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons e (redCons (EdgeBetween.bar e) (reverse p)) = reverse p
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
lm : redCons e (redCons (EdgeBetween.bar e) (reverse p)) = reverse p
⊢ reverse (redCons e (redCons (EdgeBetween.bar e) (reverse p))) = p
Tactic:
rw [lm, reverse_reverse]
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ redCons (EdgeBetween.bar (EdgeBetween.bar e)) (redCons (EdgeBetween.bar e) (reverse p)) = reverse p
Tactic:
apply cancelling_steps_redCons
State after:
case hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reduced (reverse p)

State before:
case hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w u : V
p : EdgePath G v w
e : EdgeBetween G w u
hyp : reduced p
hyp' : reduced (reverse p)
⊢ reduced (reverse p)
Tactic:
assumption
State after:
no goals