awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h :
  ∀ (h : AddCommGrpCat.of (ULift.{u, 0} ℤ) ⟶ A) (x : ℤ),
    Eq (α := (↑B : Type u))
      ((AddCommGrpCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u))
          ((AddCommGrpCat.Hom.hom h : (a : ULift.{u, 0} ℤ) → (↑A : Type u)) { down := x : ULift.{u, 0} ℤ } :
            (↑A : Type u)) :
        (↑B : Type u))
      ((AddCommGrpCat.Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u))
          ((AddCommGrpCat.Hom.hom h : (a : ULift.{u, 0} ℤ) → (↑A : Type u)) { down := x : ULift.{u, 0} ℤ } :
            (↑A : Type u)) :
        (↑B : Type u))
x : (↑A : Type u)
⊢ Eq (α := (↑B : Type u))
    ((AddCommGrpCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u))
        ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun (y : ULift.{u, 0} ℤ) ↦ y • x) ⋯)) :
              (a : ULift.{u, 0} ℤ) → (↑A : Type u))
            { down := 1 } :
          (↑A : Type u)) :
      (↑B : Type u))
    ((AddCommGrpCat.Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u))
        ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun (y : ULift.{u, 0} ℤ) ↦ y • x) ⋯)) :
              (a : ULift.{u, 0} ℤ) → (↑A : Type u))
            { down := 1 } :
          (↑A : Type u)) :
      (↑B : Type u))

Tactic:
specialize h (AddCommGrpCat.ofHom
    (AddMonoidHom.mk' (fun y => y • x) fun y z => by simp only [add_smul])) 1

Premises used: AddMonoidHom.mk', HSMul.hSMul, AddCommGrpCat.ofHom, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
x : (↑A : Type u)
h :
  Eq (α := (↑B : Type u))
    ((AddCommGrpCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u))
        ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun (y : ULift.{u, 0} ℤ) ↦ y • x) ⋯)) :
              (a : ULift.{u, 0} ℤ) → (↑A : Type u))
            { down := 1 } :
          (↑A : Type u)) :
      (↑B : Type u))
    ((AddCommGrpCat.Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u))
        ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun (y : ULift.{u, 0} ℤ) ↦ y • x) ⋯)) :
              (a : ULift.{u, 0} ℤ) → (↑A : Type u))
            { down := 1 } :
          (↑A : Type u)) :
      (↑B : Type u))
⊢ Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) f :
          (a : (↑A : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) g :
          (a : (↑A : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))

Tactic:
aesop
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : GrpCat
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
R : Type u
inst : Group R
⊢ (↑(of R) : Type u) = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : GrpCat
⊢ Hom.hom (𝟙 X) = MonoidHom.id (↑X : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : GrpCat
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y T : GrpCat
f : X ⟶ Y
g : Y ⟶ T
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y T : GrpCat
f : X ⟶ Y
g : Y ⟶ T
x : (↑X : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑X : Type u_1)) → (↑T : Type u_1))
        x :
      (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier) g :
          (a : (↑Y : Type u_1)) → (↑T : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
                f :
              (a : (↑X : Type u_1)) → (↑Y : Type u_1))
            x :
          (↑Y : Type u_1)) :
      (↑T : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: GrpCat.Hom.ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
R S : Type u
inst : Group R
inst_1 : Group S
f : R →* S
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : Type u
inst : Group X
⊢ ofHom (MonoidHom.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y Z : Type u
inst : Group X
inst_1 : Group Y
inst_2 : Group Z
f : X →* Y
g : Y →* Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : Group X
inst_1 : Group Y
f : X →* Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑Y : Type u_1)) → (↑X : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              e.hom :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : GrpCat
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              e.inv :
            (a : (↑Y : Type u_1)) → (↑X : Type u_1))
          s :
        (↑X : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : Group X
inst_1 : Group Y
f : X →* Y
⊢ CategoryTheory.Functor.map
      (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
        fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
      (ofHom f) =
    MonCat.ofHom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
R S : GrpCat
f : R ⟶ S
x :
  (↑(Functor.obj
        (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier) MonCat
          (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := MonCat.carrier))
        R) :
    Type u_1)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := MonCat.carrier))
          S) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            MonCat.carrier) (X :=
            Functor.obj
              (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
                MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := MonCat.carrier))
              R)
            (CategoryTheory.Functor.map
              (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
                MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := MonCat.carrier))
              f) :
          (a : (↑((forget₂ GrpCat MonCat).obj R) : Type u_1)) → (↑((forget₂ GrpCat MonCat).obj S) : Type u_1))
        x :
      (↑(Functor.obj
            (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
              MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD := MonCat.carrier))
            S) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier) f :
          (a : (↑R : Type u_1)) → (↑S : Type u_1))
        x :
      (↑S : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
G H : GrpCat
g : (↑G : Type u_1)
⊢ Eq (α := (↑H : Type u_1))
    ((@ConcreteCategory.hom _ instCategory (fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) carrier _
            _ G H 1 :
          (a : (↑G : Type u_1)) → (↑H : Type u_1))
        g :
      (↑H : Type u_1))
    (1 : (↑H : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : Group X
inst_1 : Group Y
a₁ : X →* Y
_ :
  ∀ ⦃a₂ : X →* Y⦄,
    Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂) → a₁ = a₂
⊢ ∀ ⦃a₂ : X →* Y⦄,
    Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂) → a₁ = a₂

Tactic:
_
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : Group X
inst_1 : Group Y
a₁ a₂ : X →* Y
h : Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂)
h₁ : ∀ (x : X), Eq (α := Y) ((a₁ : (a : X) → Y) x : Y) ((a₂ : (a : X) → Y) x : Y)
⊢ a₁ = a₂

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : Group X
inst_1 : Group Y
a₁ a₂ : X →* Y
h : Eq.{u + 1} (α := of X ⟶ of Y) ((fun (f : X →* Y) ↦ ofHom f) a₁) ((fun (f : X →* Y) ↦ ofHom f) a₂)
x : X
⊢ Eq (α := Y) ((a₁ : (a : X) → Y) x : Y) ((a₂ : (a : X) → Y) x : Y)

Tactic:
apply ConcreteCategory.congr_hom h

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
⊢ Functor.Full
    (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
      fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))

Tactic:
fullyFaithfulForget₂ToMonCat.full

Premises used: GrpCat.fullyFaithfulForget₂ToMonCat, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
R S : GrpCat
i : R ⟶ S
r : (↑R : Type u_1)
h : r = 1
⊢ Eq (α := (↑S : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier) i :
          (a : (↑R : Type u_1)) → (↑S : Type u_1))
        r :
      (↑S : Type u_1))
    (1 : (↑S : Type u_1))

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : GrpCat
⊢ ofHom
      (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
        ((Hom.hom (𝟙 X)).comp (MulEquiv.toMonoidHom MulEquiv.ulift))) =
    𝟙 (of (ULift.{u, v} (↑X : Type v)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y Z : GrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := of (ULift.{u, v} (↑X : Type v)) ⟶ of (ULift.{u, v} (↑Z : Type v)))
    (ofHom
      (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
        ((Hom.hom (f ≫ g)).comp (MulEquiv.toMonoidHom MulEquiv.ulift))))
    (CategoryStruct.comp (Y := of (ULift.{u, v} (↑Y : Type v)))
      (ofHom
        (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
          ((Hom.hom f).comp (MulEquiv.toMonoidHom MulEquiv.ulift))))
      (ofHom
        (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm MulEquiv.ulift))
          ((Hom.hom g).comp (MulEquiv.toMonoidHom MulEquiv.ulift)))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : CommGrpCat
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑X : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier) (𝟙 X)) :
      (a : (↑X : Type u_1)) → (↑X : Type u_1))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y Z : CommGrpCat
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier) (f ≫ g)) :
      (a : (↑X : Type u_1)) → (↑Z : Type u_1))
    (Function.comp (β := (↑Y : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) g) :
        (a : (↑Y : Type u_1)) → (↑Z : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) f) :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
f g : X ⟶ Y
w :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) f :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) g :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
⊢ f = g

Tactic:
ConcreteCategory.hom_ext _ _ w

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
R : Type u
inst : CommGroup R
⊢ (↑(of R) : Type u) = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : CommGrpCat
⊢ Hom.hom (𝟙 X) = MonoidHom.id (↑X : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : CommGrpCat
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          (𝟙 X) :
        (a : (↑X : Type u_1)) → (↑X : Type u_1))
      x =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y T : CommGrpCat
f : X ⟶ Y
g : Y ⟶ T
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y T : CommGrpCat
f : X ⟶ Y
g : Y ⟶ T
x : (↑X : Type u_1)
⊢ Eq (α := (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            (f ≫ g) :
          (a : (↑X : Type u_1)) → (↑T : Type u_1))
        x :
      (↑T : Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            g :
          (a : (↑Y : Type u_1)) → (↑T : Type u_1))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
                carrier) f :
              (a : (↑X : Type u_1)) → (↑Y : Type u_1))
            x :
          (↑Y : Type u_1)) :
      (↑T : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
f g : X ⟶ Y
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: CommGrpCat.Hom.ext
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : CommGroup X
inst_1 : CommGroup Y
f : X →* Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
f : X ⟶ Y
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X : Type u
inst : CommGroup X
⊢ ofHom (MonoidHom.id X) = 𝟙 (of X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y Z : Type u
inst : CommGroup X
inst_1 : CommGroup Y
inst_2 : CommGroup Z
f : X →* Y
g : Y →* Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : CommGroup X
inst_1 : CommGroup Y
f : X →* Y
x : X
⊢ Eq (α := (↑(of Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (ofHom f) :
          (a : (↑(of X) : Type u)) → (↑(of Y) : Type u))
        x :
      (↑(of Y) : Type u))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
e : X ≅ Y
x : (↑X : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.inv :
        (a : (↑Y : Type u_1)) → (↑X : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) e.hom :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : CommGrpCat
e : X ≅ Y
s : (↑Y : Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
          e.hom :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) e.inv :
            (a : (↑Y : Type u_1)) → (↑X : Type u_1))
          s :
        (↑X : Type u_1)) =
    s

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : CommGroup X
inst_1 : CommGroup Y
f : X →* Y
⊢ CategoryTheory.Functor.map
      (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
        (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
      (ofHom f) =
    GrpCat.ofHom f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
R S : CommGrpCat
f : R ⟶ S
x :
  (↑(Functor.obj
        (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
          GrpCat.carrier))
        R) :
    Type u_1)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
            GrpCat.carrier))
          S) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            GrpCat.carrier) (X :=
            Functor.obj
              (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
                carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
                GrpCat.carrier))
              R)
            (CategoryTheory.Functor.map
              (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
                carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
                GrpCat.carrier))
              f) :
          (a : (↑((forget₂ CommGrpCat GrpCat).obj R) : Type u_1)) → (↑((forget₂ CommGrpCat GrpCat).obj S) : Type u_1))
        x :
      (↑(Functor.obj
            (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
              GrpCat.carrier))
            S) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommGrpCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := carrier)
            f :
          (a : (↑R : Type u_1)) → (↑S : Type u_1))
        x :
      (↑S : Type u_1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
⊢ Functor.Full
    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
      (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))

Tactic:
fullyFaithfulForget₂ToGrp.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CommGrpCat.fullyFaithfulForget₂ToGrp
-- Module: Mathlib.Algebra.Category.Grp.Basic
Goal:
X Y : Type u
inst : CommGroup X
inst_1 : CommGroup Y
f : X →* Y
⊢ Eq (α :=
    Functor.obj
        (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
          CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
        (of X) ⟶
      Functor.obj
        (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
          CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
        (of Y))
    (CategoryTheory.Functor.map
      (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
        CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
      (ofHom f))
    (CommMonCat.ofHom f)

Tactic:
rfl

Premises used: rfl