internlm/Lean-Github huggingface dataset:
Theorem: Graph.SubgroupCover.proj_image
Proof 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]
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 η =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]
Theorem: Graph.SubgroupCover.proj_image
Proof 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 [[ η ]] = _
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']]
⊢ [[η]] =
    [[EdgePath.map
        (shiftTarget
          (lift (reduction η) (groupCoverProj H) (basepoint H)
              (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))).path
          term_lift')
        (groupCoverProj H)]]
Theorem: Graph.SubgroupCover.proj_image
Proof 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]
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']]
⊢ [[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)]]
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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)
Theorem: Graph.SubgroupCover.proj_image
Proof 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
Proof 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))
Theorem: Graph.SubgroupCover.proj_image
Proof 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]
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₀)
η : 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]
Proof 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
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₀)
η : 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]
Proof 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₀)) }⟧
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₀)
η : 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
Proof 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₀)) }
Theorem: Graph.SubgroupCover.proj_image
Proof 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]
Proof 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
Theorem: Graph.SubgroupCover.proj_image
Proof 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'
Proof state after:
no goals
Theorem: Graph.SubgroupCover.proj_image
Proof 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⟩
Proof 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
Theorem: Graph.SubgroupCover.proj_image
Proof 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]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.range_proj
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₀)
⊢ MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) =
    H
Tactic:
apply Subgroup.ext
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₀)
⊢ ∀ (x : π₁ G x₀),
    x ∈
        MonoidHom.range
          (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) ↔
      x ∈ H
Theorem: Graph.SubgroupCover.range_proj
Proof 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₀)
⊢ ∀ (x : π₁ G x₀),
    x ∈
        MonoidHom.range
          (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) ↔
      x ∈ H
Tactic:
intro x
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₀)
x : π₁ G x₀
⊢ x ∈
      MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) ↔
    x ∈ H
Theorem: Graph.SubgroupCover.range_proj
Proof 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₀)
x : π₁ G x₀
⊢ x ∈
      MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) ↔
    x ∈ H
Tactic:
simp [MonoidHom.mem_range]
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₀)
x : π₁ G x₀
⊢ (∃ x_1,
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
            (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))
          x_1 =
        x) ↔
    x ∈ H