simp only [reverse_append_self] 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₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * ([[reverse v₂ ++ v₂]] * [[reverse v₃]]) ∈ 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₂ v₃ : EdgePath G x₀ τ
h₁ : [[v₁ ++ reverse v₂]] ∈ H
h₂ : [[v₂ ++ reverse v₃]] ∈ H
h₃ : [[v₁]] * ([[nil τ]] * [[reverse v₃]]) ∈ H
⊢ [[v₁ ++ reverse v₃]] ∈ H