Theorem: Graph.reduction_eq_self_of_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 : V
p : EdgePath G v w
hyp : reduced p
⊢ reduction p = p
Tactic:
induction p with
| nil _ =>
  simp [reduction_nil]
| cons e p ih =>
  rw [reduction_cons]
  have teq : reduction p = p := by
    apply ih
    apply tail_reduced
    assumption
  rw [teq]
  apply redCons_eq_cons_of_reduced
  assumption
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 w v✝ : V
hyp : reduced (nil v✝)
⊢ reduction (nil v✝) = nil v✝
Tactic:
simp [reduction_nil]
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 w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduction (cons e p) = cons e p
Tactic:
rw [reduction_cons]
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ redCons e (reduction p) = cons e p

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ redCons e (reduction p) = cons e p
Tactic:
have teq : reduction p = p := by
  apply ih
  apply tail_reduced
  assumption
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e (reduction p) = cons e p

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e (reduction p) = cons e p
Tactic:
rw [teq]
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e p = cons e p

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ redCons e p = cons e p
Tactic:
apply redCons_eq_cons_of_reduced
State after:
case cons.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ reduced (cons e p)

State before:
case cons.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
teq : reduction p = p
⊢ reduced (cons e p)
Tactic:
assumption
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduction p = p
Tactic:
apply ih
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced p

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced p
Tactic:
apply tail_reduced
State after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced (cons ?e p)

case u
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ V

case e
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ EdgeBetween G ?u w✝

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ reduced (cons ?e p)

case u
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ V

case e
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p : EdgePath G w✝ u✝
ih : reduced p → reduction p = p
hyp : reduced (cons e p)
⊢ EdgeBetween G ?u w✝
Tactic:
assumption
State after:
no goals