Theorem: Graph.SubgroupCover.proj_image (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₀)
⊢ ∀ (g : π₁ G x₀),
    g ∈ H ↔
      ∃ h',
        g =
          (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
            h'
Tactic:
apply Quot.ind
State after:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : EdgePath G x₀ x₀),
    Quot.mk Reduction a ∈ H ↔
      ∃ h',
        Quot.mk Reduction a =
          (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
            h'

State before:
case mk
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (a : EdgePath G x₀ x₀),
    Quot.mk Reduction a ∈ H ↔
      ∃ h',
        Quot.mk Reduction a =
          (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
            h'
Tactic:
intro η
State after:
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 G x₀ x₀
⊢ Quot.mk Reduction η ∈ H ↔
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'

State before:
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 G x₀ x₀
⊢ Quot.mk Reduction η ∈ H ↔
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'
Tactic:
let η' := reduction η
State after:
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 G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
⊢ Quot.mk Reduction η ∈ H ↔
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'

State before:
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 G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
⊢ Quot.mk Reduction η ∈ H ↔
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'
Tactic:
apply Iff.intro
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
⊢ Quot.mk Reduction η ∈ H →
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'

case mk.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
⊢ (∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h') →
    Quot.mk Reduction η ∈ H

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
⊢ Quot.mk Reduction η ∈ H →
    ∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h'
Tactic:
intro mem
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
have mem' :  [[ η ]] ∈ H := mem
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[η]] ∈ H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[η]] ∈ H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
rw [← reduction_homotopic_self] at mem'
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
let pL := η'.lift (groupCoverProj H) (basepoint H) rfl
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
let p := pL.path
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
have term_lift : pL.τ = _ :=
  reduced_liftTerminal_factor H η' (reduction_reduced η)
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
have term_lift' : pL.τ = basepoint H := by
  rw [term_lift]
  simp [basepoint, UniversalCover.basepoint]
  apply Quotient.sound
  simp [HasEquiv.Equiv, Setoid.r, relH]
  exact mem'
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
let p' := p.shiftTarget term_lift'
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
let h' : π₁ (groupCover H) (basepoint H) :=
  [[ p' ]]
State after:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'

State before:
case mk.mp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ ∃ h',
    Quot.mk Reduction η =
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
        h'
Tactic:
use h'
State after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ Quot.mk Reduction η =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h'

State before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ Quot.mk Reduction η =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h'
Tactic:
simp [Morphism.π₁map, PathClass.map]
State after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ Quot.mk Reduction η =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]

State before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ Quot.mk Reduction η =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]
Tactic:
show [[ η ]] = _
State after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ [[η]] =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]

State before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ [[η]] =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]
Tactic:
rw [← reduction_homotopic_self]
State after:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ [[reduction η]] =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]

State before:
case h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ [[reduction η]] =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]
Tactic:
congr
State after:
case h.e_p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ reduction η =
    EdgePath.map
      (shiftTarget
        (lift (reduction η) (groupCoverProj H) (basepoint H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
        term_lift')
      (groupCoverProj H)

State before:
case h.e_p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ reduction η =
    EdgePath.map
      (shiftTarget
        (lift (reduction η) (groupCoverProj H) (basepoint H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
        term_lift')
      (groupCoverProj H)
Tactic:
apply eq_of_toList_eq
State after:
case h.e_p.a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ EdgePath.toList (reduction η) =
    EdgePath.toList
      (EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H))

State before:
case h.e_p.a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
term_lift' : pL.τ = basepoint H
p' : EdgePath (groupCover H) (basepoint H) (basepoint H) := shiftTarget p term_lift'
h' : π₁ (groupCover H) (basepoint H) := [[p']]
⊢ EdgePath.toList (reduction η) =
    EdgePath.toList
      (EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H))
Tactic:
rw [EdgePath.map_toList, toList_shiftTarget,
  pL.list_pushdown]
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ pL.τ = basepoint H
Tactic:
rw [term_lift]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧ = basepoint H

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧ = basepoint H
Tactic:
simp [basepoint, UniversalCover.basepoint]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ ⟦{ τ := x₀, p := reduction η, is_reduced := (_ : reduced (reduction η)) }⟧ =
    ⟦{ τ := x₀, p := nil x₀, is_reduced := (_ : reduced (nil x₀)) }⟧

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ ⟦{ τ := x₀, p := reduction η, is_reduced := (_ : reduced (reduction η)) }⟧ =
    ⟦{ τ := x₀, p := nil x₀, is_reduced := (_ : reduced (nil x₀)) }⟧
Tactic:
apply Quotient.sound
State after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ { τ := x₀, p := reduction η, is_reduced := (_ : reduced (reduction η)) } ≈
    { τ := x₀, p := nil x₀, is_reduced := (_ : reduced (nil x₀)) }

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ { τ := x₀, p := reduction η, is_reduced := (_ : reduced (reduction η)) } ≈
    { τ := x₀, p := nil x₀, is_reduced := (_ : reduced (nil x₀)) }
Tactic:
simp [HasEquiv.Equiv, Setoid.r, relH]
State after:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ [[reduction η]] ∈ H

State before:
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
mem : Quot.mk Reduction η ∈ H
mem' : [[reduction η]] ∈ H
pL : PathLift (groupCoverProj H) (basepoint H)
  (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)) η' :=
  lift η' (groupCoverProj H) (basepoint H)
    (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))
p : EdgePath (groupCover H) (basepoint H) pL.τ := pL.path
term_lift : pL.τ = ⟦{ τ := x₀, p := η', is_reduced := (_ : reduced (reduction η)) }⟧
⊢ [[reduction η]] ∈ H
Tactic:
exact mem'
State after:
no goals

State before:
case mk.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
⊢ (∃ h',
      Quot.mk Reduction η =
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          h') →
    Quot.mk Reduction η ∈ H
Tactic:
intro ⟨h, heqn⟩
State after:
case mk.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
h : π₁ (groupCover H) (basepoint H)
heqn :
  Quot.mk Reduction η =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
⊢ Quot.mk Reduction η ∈ H

State before:
case mk.mpr
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
η : EdgePath G x₀ x₀
η' : EdgePath G x₀ x₀ := reduction η
h : π₁ (groupCover H) (basepoint H)
heqn :
  Quot.mk Reduction η =
    (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
      h
⊢ Quot.mk Reduction η ∈ H
Tactic:
simp [imageInSubgroup H h, heqn]
State after:
no goals