rw [reduced_liftTerminal_factor' H (reduction θ)
  (by apply reduction_reduced)] 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 :
  liftTerminal (groupCoverProj H) (basepoint H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) (reduction θ) =
    basepoint H
⊢ [[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 θ, is_reduced := (_ : reduced (reduction θ)) }⟧ = basepoint H
⊢ [[reduction θ]] ∈ H