Theorem: Graph.not_reduced_of_split (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 u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
⊢ p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) → ¬reduced p
Tactic:
intro eqn 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 u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced 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 u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
⊢ False
Tactic:
have red' := red (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✝
v w u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction p (p₁ ++ 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 u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction p (p₁ ++ p₂)
⊢ False
Tactic:
rw [eqn] at 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 u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ 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 u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ False
Tactic:
apply 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 u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ Reduction (p₁ ++ cons e (cons (EdgeBetween.bar 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✝
v w u u' : V
p : EdgePath G v w
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u w
eqn : p = p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)
red : reduced p
red' : ¬Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
⊢ Reduction (p₁ ++ cons e (cons (EdgeBetween.bar e) p₂)) (p₁ ++ p₂)
Tactic:
apply Reduction.step
State after:
no goals