[GOAL]
⊢ ConcreteCategory GroupCat
[PROOFSTEP]
dsimp only [GroupCat]
[GOAL]
⊢ ConcreteCategory (Bundled Group)
[PROOFSTEP]
infer_instance
[GOAL]
R S : GroupCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
[GOAL]
⊢ ConcreteCategory CommGroupCat
[PROOFSTEP]
dsimp only [CommGroupCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommGroup)
[PROOFSTEP]
infer_instance
[GOAL]
R S : CommGroupCat
i : R ⟶ S
r : ↑R
h : r = 1
⊢ ↑i r = 1
[PROOFSTEP]
simp [h]
[GOAL]
G : AddCommGroupCat
h k : ↑G
w : asHom h = asHom k
⊢ h = k
[PROOFSTEP]
convert congr_arg (fun k : AddCommGroupCat.of ℤ ⟶ G => (k : ℤ → G) (1 : ℤ)) w
[GOAL]
case h.e'_2
G : AddCommGroupCat
h k : ↑G
w : asHom h = asHom k
⊢ h = ↑(asHom h) 1
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
G : AddCommGroupCat
h k : ↑G
w : asHom h = asHom k
⊢ k = ↑(asHom k) 1
[PROOFSTEP]
simp
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ g₁ = g₂
[PROOFSTEP]
have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by aesop_cat
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
⊢ asHom g₁ ≫ f = asHom g₂ ≫ f
[PROOFSTEP]
aesop_cat
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂
[PROOFSTEP]
have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0
[GOAL]
G H : AddCommGroupCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : ↑f g₁ = ↑f g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂
[PROOFSTEP]
apply asHom_injective t1
[GOAL]
α : Type u
⊢ (fun g => g.toEquiv) 1 = 1
[PROOFSTEP]
aesop
[GOAL]
α : Type u
⊢ ∀ (x y : ↑(GroupCat.of (Aut α))),
    OneHom.toFun { toFun := fun g => g.toEquiv, map_one' := (_ : (fun g => g.toEquiv) 1 = 1) } (x * y) =
      OneHom.toFun { toFun := fun g => g.toEquiv, map_one' := (_ : (fun g => g.toEquiv) 1 = 1) } x *
        OneHom.toFun { toFun := fun g => g.toEquiv, map_one' := (_ : (fun g => g.toEquiv) 1 = 1) } y
[PROOFSTEP]
aesop
[GOAL]
α : Type u
⊢ (fun g => Equiv.toIso g) 1 = 1
[PROOFSTEP]
aesop
[GOAL]
α : Type u
⊢ ∀ (x y : ↑(GroupCat.of (Equiv.Perm α))),
    OneHom.toFun { toFun := fun g => Equiv.toIso g, map_one' := (_ : (fun g => Equiv.toIso g) 1 = 1) } (x * y) =
      OneHom.toFun { toFun := fun g => Equiv.toIso g, map_one' := (_ : (fun g => Equiv.toIso g) 1 = 1) } x *
        OneHom.toFun { toFun := fun g => Equiv.toIso g, map_one' := (_ : (fun g => Equiv.toIso g) 1 = 1) } y
[PROOFSTEP]
aesop
[GOAL]
X Y : GroupCat
f : X ⟶ Y
x✝ : IsIso ((forget GroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget GroupCat).map f)
[GOAL]
X Y : GroupCat
f : X ⟶ Y
x✝ : IsIso ((forget GroupCat).map f)
i : (forget GroupCat).obj X ≅ (forget GroupCat).obj Y := asIso ((forget GroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f))
[GOAL]
X Y : GroupCat
f : X ⟶ Y
x✝ : IsIso ((forget GroupCat).map f)
i : (forget GroupCat).obj X ≅ (forget GroupCat).obj Y := asIso ((forget GroupCat).map f)
e : ↑X ≃* ↑Y :=
  { toEquiv := i.toEquiv,
    map_mul' :=
      (_ :
        ∀ (a b : ↑X),
          ↑(let_fun this := f;
                this)
              (a * b) =
            ↑(let_fun this := f;
                  this)
                a *
              ↑(let_fun this := f;
                  this)
                b) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toGroupCatIso
[GOAL]
X Y : CommGroupCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommGroupCat).map f)
[GOAL]
X Y : CommGroupCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGroupCat).map f)
i : (forget CommGroupCat).obj X ≅ (forget CommGroupCat).obj Y := asIso ((forget CommGroupCat).map f)
⊢ IsIso f
[PROOFSTEP]
let e : X ≃* Y := MulEquiv.mk i.toEquiv (MonoidHom.map_mul (show MonoidHom X Y from f))
[GOAL]
X Y : CommGroupCat
f : X ⟶ Y
x✝ : IsIso ((forget CommGroupCat).map f)
i : (forget CommGroupCat).obj X ≅ (forget CommGroupCat).obj Y := asIso ((forget CommGroupCat).map f)
e : ↑X ≃* ↑Y :=
  { toEquiv := i.toEquiv,
    map_mul' :=
      (_ :
        ∀ (a b : ↑X),
          ↑(let_fun this := f;
                this)
              (a * b) =
            ↑(let_fun this := f;
                  this)
                a *
              ↑(let_fun this := f;
                  this)
                b) }
⊢ IsIso f
[PROOFSTEP]
exact IsIso.of_iso e.toCommGroupCatIso
