rw [inv_equiv_reverse,
  reverse_append,  reverse_reverse] at h'
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : PathClass.inv [[v₁ ++ reverse v₂]] ∈ H := inv_mem h
⊢ [[v₂ ++ reverse v₁]] ∈ H
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : [[v₂ ++ reverse v₁]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H