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

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
⊢ reduced (nil v)
Tactic:
intro p' red'
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
⊢ False
Tactic:
let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G v u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
cases p₁ with
| nil _ =>
  rw [nil_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList] at leqn
| cons h t =>
  rw [cons_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList, append_toList] at leqn
State after:
no goals

State before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : nil v ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
rw [nil_append] at eqn
State after:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False

State before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
let leqn := congrArg EdgePath.toList eqn
State after:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (nil v) := congrArg toList eqn
⊢ False

State before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u' : V
e : EdgeBetween G v u'
p₂ : EdgePath G v v
eqn : cons e (cons (EdgeBetween.bar e) p₂) = nil v
leqn : toList (cons e (cons (EdgeBetween.bar e) p₂)) = toList (nil v) := congrArg toList eqn
⊢ False
Tactic:
simp [cons_toList, nil_toList] at leqn
State after:
no goals

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h t ++ cons e (cons (EdgeBetween.bar e) p₂) = nil v
⊢ False
Tactic:
rw [cons_append] at eqn
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
⊢ False

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
⊢ False
Tactic:
let leqn := congrArg EdgePath.toList eqn
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
leqn : toList (cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂))) = toList (nil v) := congrArg toList eqn
⊢ False

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v : V
p' : EdgePath G v v
red' : Reduction (nil v) p'
u u' : V
e : EdgeBetween G u u'
p₂ : EdgePath G u v
w✝ : V
h : EdgeBetween G v w✝
t : EdgePath G w✝ u
eqn : cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂)) = nil v
leqn : toList (cons h (t ++ cons e (cons (EdgeBetween.bar e) p₂))) = toList (nil v) := congrArg toList eqn
⊢ False
Tactic:
simp [cons_toList, nil_toList, append_toList] at leqn
State after:
no goals