Theorem: Graph.SubgroupCover.path_eq_iff_r (GroupComp/Graph/SubgroupCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
p₁ p₂ : EdgePath G x₀ τ
red₁ : reduced p₁
red₂ : reduced p₂
⊢ Setoid.r { τ := τ, p := p₁, is_reduced := red₁ } { τ := τ, p := p₂, is_reduced := red₂ } ↔ [[p₁ ++ reverse p₂]] ∈ H
Tactic:
simp [Setoid.r, relH]
State after:
no goals