Theorem: Graph.reverse_reduced (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 : V
p : EdgePath G v w
⊢ reduced p → reduced (reverse p)
Tactic:
intro red rev_targ rev_red
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
⊢ False

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 : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
⊢ False
Tactic:
let ⟨u, u', e, p₁, p₂, eqn⟩   := rev_red.property
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ False

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 : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ False
Tactic:
apply red (reverse p₂ ++ reverse 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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ Reduction p (reverse p₂ ++ reverse 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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
let eqn' := congrArg reverse eqn
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = reverse (reverse p) := congrArg reverse eqn
⊢ Reduction p (reverse p₂ ++ reverse 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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = reverse (reverse p) := congrArg reverse eqn
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
simp [reverse_reverse] at eqn'
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ Reduction p (reverse p₂ ++ reverse 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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
have eqn'' : (reverse p₂) ++ (cons e (cons e.bar (reverse p₁))) =
  p := by
    rw [←eqn', reverse_append]
    simp [reverse_cons]
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction p (reverse p₂ ++ reverse 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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction p (reverse p₂ ++ reverse p₁)
Tactic:
rw [←eqn'']
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction (reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁))) (reverse p₂ ++ reverse 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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
eqn'' : reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
⊢ Reduction (reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁))) (reverse p₂ ++ reverse p₁)
Tactic:
apply Reduction.step
State after:
no goals

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 : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) = p
Tactic:
rw [←eqn', reverse_append]
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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) =
    reverse (cons e (cons (EdgeBetween.bar e) p₂)) ++ reverse 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✝
v w : V
p : EdgePath G v w
red : reduced p
rev_targ : EdgePath G w v
rev_red : Reduction (reverse p) rev_targ
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G w u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = reverse p
eqn' : reverse (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) = p
⊢ reverse p₂ ++ cons e (cons (EdgeBetween.bar e) (reverse p₁)) =
    reverse (cons e (cons (EdgeBetween.bar e) p₂)) ++ reverse p₁
Tactic:
simp [reverse_cons]
State after:
no goals