Theorem: Graph.UniversalCover.rayTo_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 p
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayTo G x₀ τ p hyp)) = EdgePath.toList p
Tactic:
simp [rayTo, toList_shiftTarget, rayToRev_proj_list,
  reverse_toList, List.map_reverse]
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₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList 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₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList p
Tactic:
have : G.bar ∘ G.bar = id := by
  funext x
  simp only [Function.comp, bar_bar, id_eq]
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₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
this : G.bar ∘ G.bar = id
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList 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₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
this : G.bar ∘ G.bar = id
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList p
Tactic:
simp [this]
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₀ τ : V
p : EdgePath G x₀ τ
hyp : reduced p
⊢ G.bar ∘ G.bar = id
Tactic:
funext x
State after:
case h
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 p
x : E
⊢ (G.bar ∘ G.bar) x = id x

State before:
case h
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 p
x : E
⊢ (G.bar ∘ G.bar) x = id x
Tactic:
simp only [Function.comp, bar_bar, id_eq]
State after:
no goals