rw [← heqn]
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 θ
⊢ [[EdgePath.map η (groupCoverProj H)]] ∈ 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 θ
⊢ [[reduction θ]] ∈ H