Theorem: Graph.reducedConcat_reduced (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
⊢ reduced (p:+e)
Tactic:
simp only [reducedConcat]
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
⊢ reduced (reverse (redCons (EdgeBetween.bar e) (reverse 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
⊢ reduced (reverse (redCons (EdgeBetween.bar e) (reverse p)))
Tactic:
apply reverse_reduced
State after:
case a
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
⊢ reduced (redCons (EdgeBetween.bar e) (reverse p))

State before:
case a
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
⊢ reduced (redCons (EdgeBetween.bar e) (reverse p))
Tactic:
apply reduced_redCons
State after:
case a.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
⊢ reduced (reverse p)

State before:
case a.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
⊢ reduced (reverse p)
Tactic:
apply reverse_reduced
State after:
case a.hyp.a
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
⊢ reduced p

State before:
case a.hyp.a
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
⊢ reduced p
Tactic:
apply hyp
State after:
no goals