Theorem: Graph.SubgroupCover.group_of_cover_is_subgroup (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₀)
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Tactic:
let hf :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Tactic:
let lem := MonoidHom.ofInjective hf
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ π₁ (groupCover H) (basepoint H) ≃* ↥H
Tactic:
apply MulEquiv.trans lem
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ ↥(MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) ≃*
    ↥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₀)
hf : Function.Injective
  ⇑(Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
      (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H))) :=
  cover_π₁injective (groupCoverProj H) (basepoint H) x₀ rfl
lem : π₁ (groupCover H) (basepoint H) ≃*
  ↥(MonoidHom.range
      (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
        (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) :=
  MonoidHom.ofInjective hf
⊢ ↥(MonoidHom.range
        (Morphism.π₁map (basepoint H) x₀ (groupCoverProj H)
          (_ : (groupCoverProj H).toFuncV (basepoint H) = (groupCoverProj H).toFuncV (basepoint H)))) ≃*
    ↥H
Tactic:
rw [range_proj]
State after:
no goals