rw [Quotient.eq (r := vertSetoid H)] at term_eqn
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn :
  ⟦{ τ := x₀, p := reduction (EdgePath.map η (groupCoverProj H)), is_reduced := (_ : reduced (reduction θ)) }⟧ =
    ⟦{ τ := x₀, p := nil x₀, is_reduced := (_ : reduced (nil x₀)) }⟧
⊢ [[reduction θ]] ∈ H
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn :
  { τ := x₀, p := reduction (EdgePath.map η (groupCoverProj H)), is_reduced := (_ : reduced (reduction θ)) } ≈
    { τ := x₀, p := nil x₀, is_reduced := (_ : reduced (nil x₀)) }
⊢ [[reduction θ]] ∈ H