internlm/Lean-Github huggingface dataset:
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof 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 (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
Tactic:
rw [Quotient.eq (r := vertSetoid H)] at term_eqn
Proof 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 (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
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof 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 (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
Tactic:
simp [HasEquiv.Equiv, Setoid.r, relH] at term_eqn
Proof 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 (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn : [[reduction (EdgePath.map η (groupCoverProj H))]] ∈ H
⊢ [[reduction θ]] ∈ H
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof 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 (groupCover H) (basepoint H) (basepoint H)
θ : EdgePath G x₀ x₀ := EdgePath.map η (groupCoverProj H)
heqn : [[reduction θ]] = [[θ]] := reduction_homotopic_self θ
term_eqn : [[reduction (EdgePath.map η (groupCoverProj H))]] ∈ H
⊢ [[reduction θ]] ∈ H
Tactic:
exact term_eqn
Proof state after:
no goals
Theorem: Graph.SubgroupCover.imageInSubgroup
Proof 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 (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
⊢ reduced (reduction θ)
Tactic:
apply reduction_reduced
Proof state after:
no goals
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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 η
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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 η
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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'
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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 η)
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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'
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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'
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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' ]]
Proof 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'
Theorem: Graph.SubgroupCover.proj_image
Proof 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'
Proof 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'