Theorem: Graph.UniversalCover.rayToRev_proj_list (GroupComp/Graph/UniversalCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G τ x₀
hyp : reduced (reverse p)
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G x₀ τ p hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList p))
Tactic:
induction p with
| nil _ =>
simp [rayToRev, nil_toList]
| cons e p' ih =>
rename_i x₀' u u'
have red_cons : reduced (cons e p') := by
  rw [← reverse_reverse (cons e p')]
  apply reverse_reduced
  assumption
have red_p' : reduced p' := by
  apply tail_reduced e p'
  assumption
have red' : reduced p'.reverse := by
  apply reverse_reduced
  assumption
simp [rayToRev, cons_toList, concat_toList, ih red']
State after:
no goals

State before:
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ v✝ : V
hyp : reduced (reverse (nil v✝))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G v✝ v✝ (nil v✝) hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (nil v✝)))
Tactic:
simp [rayToRev, nil_toList]
State after:
no goals

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u✝ w✝ p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u✝ v✝ (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
rename_i x₀' u u'
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
have red_cons : reduced (cons e p') := by
  rw [← reverse_reverse (cons e p')]
  apply reverse_reduced
  assumption
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
have red_p' : reduced p' := by
  apply tail_reduced e p'
  assumption
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
have red' : reduced p'.reverse := by
  apply reverse_reduced
  assumption
State after:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
red' : reduced (reverse p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))

State before:
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
red' : reduced (reverse p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
Tactic:
simp [rayToRev, cons_toList, concat_toList, ih red']
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (cons e p')
Tactic:
rw [← reverse_reverse (cons e p')]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (reverse (cons e p')))

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (reverse (cons e 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
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (cons e p'))

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ reduced (reverse (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
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ reduced p'
Tactic:
apply tail_reduced e p'
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ reduced (cons e p')

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e 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
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ reduced (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
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ reduced p'

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
red_p' : reduced p'
⊢ reduced p'
Tactic:
assumption
State after:
no goals