awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
F : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
α :
  (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
          GrpCat.carrier)).RepresentableBy
    X
⊢ HMul.hMul (α := (↑(F.obj (op X)) : Type w)) (β := (↑(F.obj (op X)) : Type w))
      ((((α.homEquiv :
                Equiv.{v + 1, w + 1} (X ⟶ X)
                  ((F ⋙
                        forget GrpCat (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                          GrpCat.carrier)).obj
                    (op X))) :
              (a : X ⟶ X) → ToType (F.obj (op X)))
            (𝟙 X))⁻¹ :
        ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
          (F.obj (op X)))
      (((α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
              Equiv.{v + 1, w + 1} (X ⟶ X)
                (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                  (F.obj (op X)))) :
            (a : X ⟶ X) → ToType (F.obj (op X)))
          (𝟙 X) :
        ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
          (F.obj (op X))) =
    1

Tactic:
exact inv_mul_cancel (α.homEquiv (𝟙 X))

Premises used: inv_mul_cancel, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.RepresentableBy.homEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
f : X ⟶ G
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (f ≫ @GrpObj.inv _ _ inst_1 _ _) f) μ =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (f ≫ lift (@GrpObj.inv _ _ inst_1 _ _) (𝟙 G)) μ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
f : X ⟶ G
rw :
  f ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (@GrpObj.inv _ _ inst_1 _ _) (𝟙 G)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit X) η
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (f ≫ lift (@GrpObj.inv _ _ inst_1 _ _) (𝟙 G)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit X) η

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
f : X ⟶ G
⊢ f ≫ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (@GrpObj.inv _ _ inst_1 _ _) (𝟙 G)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit X) η

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G X : C
inst_2 : GrpObj G
f : X ⟶ G
⊢ f⁻¹ = f ≫ @GrpObj.inv _ _ inst_1 _ _

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
H : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) μ μ
⊢ ofRepresentableBy G (yonedaGrpObj G) (yonedaGrpObjRepresentableBy G) = inst_2

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
H :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (fst G G) (snd G G)) μ) μ
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) μ μ

Tactic:
change lift (fst G G) (snd G G) ≫ μ = μ

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
H : 𝟙 (tensorObj.{v, u} (𝒞 := inst) G G) ≫ μ = μ
H₁ H₂ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G) μ μ
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) G G ⟶ G)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift (fst G G) (snd G G)) μ) μ

Tactic:
rw [lift_fst_snd, Category.id_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G H X Y : C
inst_2 : GrpObj G
inst_3 : GrpObj H
α : Quiver.Hom (V := Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat) (yonedaGrpObj G) (yonedaGrpObj H)
f : X ⟶ Y
g : Y ⟶ G
⊢ Eq (α := (↑(Functor.obj (yonedaGrpObj H) (op X)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
            (X := Functor.obj (yonedaGrpObj G) (op X)) (α.app (op X)) :
          (a : (↑((yonedaGrpObj G).obj (op X)) : Type v)) → (↑((yonedaGrpObj H).obj (op X)) : Type v))
        (f ≫ g) :
      (↑(Functor.obj (yonedaGrpObj H) (op X)) : Type v))
    (f ≫
        (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
              (X := Functor.obj (yonedaGrpObj G) (op Y)) (α.app (op Y)) :
            (a : (↑((yonedaGrpObj G).obj (op Y)) : Type v)) → (↑((yonedaGrpObj H).obj (op Y)) : Type v))
          g :
      X ⟶ H)

Tactic:
congr($(α.naturality f.op) g)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, id, CategoryTheory.NatTrans.naturality, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G_1 H_1 X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G_1
inst_4 : GrpObj H_1
G H : Grp.{v, u} C
α : Functor.obj yonedaGrp G ⟶ Functor.obj yonedaGrp H
w :
  ∀ (X : Cᵒᵖ),
    GrpCat.Hom.hom
        (NatTrans.app
          (Functor.map yonedaGrp
            (Grp.homMk'
              (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
                (Functor.whiskerRight α
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))))))
          X) =
      GrpCat.Hom.hom (α.app X)
⊢ Functor.map yonedaGrp
      (Grp.homMk'
        (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
          (Functor.whiskerRight α
            (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
              MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier))))) =
    α

Tactic:
ext X : 3
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G_1 H_1 X_1 Y : C
inst_2 : MonObj M
inst_3 : GrpObj G_1
inst_4 : GrpObj H_1
G H : Grp.{v, u} C
α : Functor.obj yonedaGrp G ⟶ Functor.obj yonedaGrp H
X : Cᵒᵖ
⊢ GrpCat.Hom.hom
      (NatTrans.app
        (Functor.map yonedaGrp
          (Grp.homMk'
            (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
              (Functor.whiskerRight α
                (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                  GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                  MonCat.carrier))))))
        X) =
    GrpCat.Hom.hom (α.app X)

Tactic:
congr(($(yonedaMonFullyFaithful.map_preimage (X := G.toMon) (Y := H.toMon)
      (Functor.whiskerRight α (forget₂ GrpCat MonCat))).app X).hom)

Premises used: GrpCat, congrArg, MonCat.Hom.hom, id, MonCat, CategoryTheory.yonedaMonFullyFaithful, CategoryTheory.Functor.whiskerRight, CategoryTheory.forget₂, CategoryTheory.Functor.FullyFaithful.map_preimage, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G_1 H_1 X_1 Y : C
inst_2 : MonObj M
inst_3 : GrpObj G_1
inst_4 : GrpObj H_1
G H : Grp.{v, u} C
α : Functor.obj yonedaGrp G ⟶ Functor.obj yonedaGrp H
X : Cᵒᵖ
⊢ GrpCat.Hom.hom
      (NatTrans.app
        (Functor.map yonedaGrp
          (Grp.homMk'
            (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
              (Functor.whiskerRight α
                (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                  GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                  MonCat.carrier))))))
        X) =
    GrpCat.Hom.hom (α.app X)

Tactic:
exact congr(($(yonedaMonFullyFaithful.map_preimage (X := G.toMon) (Y := H.toMon)
      (Functor.whiskerRight α (forget₂ GrpCat MonCat))).app X).hom)
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
X_1 Y_1 : Grp.{v, u} C
f : X_1 ⟶ Y_1
h :
  Mon.Hom.hom
      (InducedCategory.Hom.hom
        (Grp.homMk'
          (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
            (Functor.whiskerRight (Functor.map yonedaGrp f)
              (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
                MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier)))))) =
    f.hom.hom
⊢ Grp.homMk'
      (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
        (Functor.whiskerRight (Functor.map yonedaGrp f)
          (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
            MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier)))) =
    f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
X_1 Y_1 : Grp.{v, u} C
f : X_1 ⟶ Y_1
h :
  Functor.FullyFaithful.preimage yonedaMonFullyFaithful
      (Functor.whiskerRight (Functor.map yonedaGrp f)
        (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
          MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier))) =
    f.hom
⊢ Mon.Hom.hom
      (InducedCategory.Hom.hom
        (Grp.homMk'
          (Functor.FullyFaithful.preimage yonedaMonFullyFaithful
            (Functor.whiskerRight (Functor.map yonedaGrp f)
              (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
                MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier)))))) =
    f.hom.hom

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
X_1 Y_1 : Grp.{v, u} C
f : X_1 ⟶ Y_1
⊢ Functor.FullyFaithful.preimage yonedaMonFullyFaithful
      (Functor.whiskerRight (Functor.map yonedaGrp f)
        (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := GrpCat.carrier)
          MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD := MonCat.carrier))) =
    f.hom

Tactic:
apply yonedaMonFullyFaithful.preimage_map

Premises used: CategoryTheory.Functor.FullyFaithful.preimage_map, CategoryTheory.yonedaMonFullyFaithful
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
⊢ Functor.Full (C := Grp.{v, u} C) yonedaGrp

Tactic:
yonedaGrpFullyFaithful.full

Premises used: CategoryTheory.yonedaGrpFullyFaithful, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
⊢ Functor.Faithful (C := Grp.{v, u} C) yonedaGrp

Tactic:
yonedaGrpFullyFaithful.faithful

Premises used: CategoryTheory.yonedaGrpFullyFaithful, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
h :
  ∀ (F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat),
    Functor.essImage (C := Grp.{v, u} C) yonedaGrp F ↔
      (F ⋙
          forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
            GrpCat.carrier)).IsRepresentable
⊢ Eq (α := ObjectProperty (Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat)) (Functor.essImage (C := Grp.{v, u} C) yonedaGrp)
    fun (F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat) ↦
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable

Tactic:
ext F
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat
h :
  Functor.essImage (C := Grp.{v, u} C) yonedaGrp F →
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable
h₁ :
  (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable →
    Functor.essImage (C := Grp.{v, u} C) yonedaGrp F
⊢ Functor.essImage (C := Grp.{v, u} C) yonedaGrp F ↔
    (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).IsRepresentable

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat
G : Grp.{v, u} C
α : Functor.obj yonedaGrp G ≅ F
⊢ (F ⋙
      forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
        GrpCat.carrier)).IsRepresentable

Tactic:
⟨G.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩

Premises used: CategoryTheory.Functor.representableByEquiv, CategoryTheory.Functor.IsRepresentable.mk, Nonempty.intro, Exists.intro, CategoryTheory.forget, Equiv.symm, CategoryTheory.Functor.isoWhiskerRight, DFunLike.coe, CategoryTheory.Grp.X
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat
G : Grp.{v, u} C
α : Functor.obj yonedaGrp G ≅ F
⊢ (F ⋙
      forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
        GrpCat.carrier)).IsRepresentable

Tactic:
exact ⟨G.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat
X : C
e :
  (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).RepresentableBy
    X
this : GrpObj X := GrpObj.ofRepresentableBy X F e
⊢ Functor.essImage (C := Grp.{v, u} C) yonedaGrp F

Tactic:
⟨⟨X⟩, ⟨yonedaGrpObjIsoOfRepresentableBy X F e⟩⟩

Premises used: CategoryTheory.Grp.mk, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy, CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
F : Functor.{v, v, u, v + 1} Cᵒᵖ GrpCat
X : C
e :
  (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
          GrpCat.carrier)).RepresentableBy
    X
this : GrpObj X := GrpObj.ofRepresentableBy X F e
⊢ Functor.essImage (C := Grp.{v, u} C) yonedaGrp F

Tactic:
exact ⟨⟨X⟩, ⟨yonedaGrpObjIsoOfRepresentableBy X F e⟩⟩
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G H X : C
inst_2 : GrpObj G
inst_3 : GrpObj H
f : X ⟶ G
g : G ⟶ H
inst_4 : IsMonHom g
⊢ f⁻¹ ≫ g = (f ≫ g)⁻¹

Tactic:
simp [Hom.inv_def]

Premises used: CategoryTheory.Hom.inv_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G H X : C
inst_2 : GrpObj G
inst_3 : GrpObj H
f g : X ⟶ G
h : G ⟶ H
inst_4 : IsMonHom h
⊢ (f / g) ≫ h = f ≫ h / g ≫ h

Tactic:
((yonedaGrp.map (Grp.homMk (A := .mk G) (B := .mk H) h)).app (op X)).hom.map_div f g

Premises used: GrpCat.Hom.hom, CategoryTheory.Functor.map, MonoidHom.map_div, Opposite.op, CategoryTheory.Grp.homMk, CategoryTheory.yonedaGrp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G H X : C
inst_2 : GrpObj G
inst_3 : GrpObj H
f : X ⟶ G
n : ℤ
g : G ⟶ H
inst_4 : IsMonHom g
⊢ (f ^ n) ≫ g = (f ≫ g) ^ n

Tactic:
((yonedaGrp.map (Grp.homMk (A := .mk G) (B := .mk H) g)).app (op X)).hom.map_zpow f n

Premises used: GrpCat.Hom.hom, CategoryTheory.Functor.map, Opposite.op, CategoryTheory.Grp.homMk, CategoryTheory.yonedaGrp, MonoidHom.map_zpow, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G X Y : C
inst_2 : GrpObj G
f : X ⟶ Y
g : Y ⟶ G
⊢ f ≫ g⁻¹ = (f ≫ g)⁻¹

Tactic:
((yonedaGrp.obj ⟨G⟩).map f.op).hom.map_inv g

Premises used: CategoryTheory.Grp.mk, GrpCat.Hom.hom, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.map, CategoryTheory.yonedaGrp, MonoidHom.map_inv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G X Y : C
inst_2 : GrpObj G
f : X ⟶ Y
g h : Y ⟶ G
⊢ f ≫ (g / h) = f ≫ g / f ≫ h

Tactic:
((yonedaGrp.obj ⟨G⟩).map f.op).hom.map_div g h

Premises used: CategoryTheory.Grp.mk, GrpCat.Hom.hom, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Functor.map, MonoidHom.map_div, CategoryTheory.yonedaGrp, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G X Y : C
inst_2 : GrpObj G
f : X ⟶ Y
g : Y ⟶ G
n : ℕ
⊢ f ≫ HPow.hPow (β := ℤ) g (↑n : ℤ) = HPow.hPow (β := ℤ) (f ≫ g) (↑n : ℤ)

Tactic:
simp [comp_pow]

Premises used: CategoryTheory.MonObj.comp_pow
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G X Y : C
inst_2 : GrpObj G
f : X ⟶ Y
g : Y ⟶ G
n : ℕ
⊢ f ≫ g ^ Int.negSucc n = (f ≫ g) ^ Int.negSucc n

Tactic:
simp [comp_pow, comp_inv]

Premises used: CategoryTheory.MonObj.comp_pow, CategoryTheory.GrpObj.comp_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
⊢ Eq.{v + 1} (α := G ⟶ G) (@inv _ _ inst_1 _ _) (𝟙 G)⁻¹

Tactic:
simp [Hom.inv_def]

Premises used: CategoryTheory.Hom.inv_def
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ G) (η ≫ @inv _ _ inst_1 _ _) η

Tactic:
simp [GrpObj.inv_eq_inv, GrpObj.comp_inv, one_eq_one]

Premises used: CategoryTheory.GrpObj.inv_eq_inv, CategoryTheory.GrpObj.comp_inv, CategoryTheory.MonObj.one_eq_one
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : CartesianMonoidalCategory.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_4 : F.Monoidal
X G : C
f : X ⟶ G
inst_5 : GrpObj G
rw : F.map f⁻¹ * F.map f = 1
rw₁ : F.map (f⁻¹ * f) = 1
rw₂ : Eq (α := F.obj X ⟶ F.obj G) (F.map 1) 1
rw₃ rw₄ : Eq.{v_1 + 1} (α := F.obj X ⟶ F.obj G) 1 1
⊢ F.map f⁻¹ = (F.map f)⁻¹

Tactic:
rw [eq_inv_iff_mul_eq_one, ← Functor.map_mul, inv_mul_cancel, Functor.map_one]

Premises used: CategoryTheory.Functor.map_mul, inv_mul_cancel, eq_inv_iff_mul_eq_one, CategoryTheory.Functor.map_one
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X G : C
inst_2 : GrpObj G
f₁ f₂ : X ⟶ G
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift f₁ f₂) (conj G) = f₁ * f₂ * f₁⁻¹

Tactic:
simp [conj, comp_mul, comp_inv]

Premises used: CategoryTheory.MonObj.comp_mul, CategoryTheory.GrpObj.comp_inv, CategoryTheory.GrpObj.conj
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
X G : C
inst_2 : GrpObj G
f₁ f₂ : X ⟶ G
⊢ CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) G G) (lift f₁ f₂) (commutator G) = f₁ * f₂ * f₁⁻¹ * f₂⁻¹

Tactic:
simp [commutator, comp_mul, comp_inv]

Premises used: CategoryTheory.GrpObj.commutator, CategoryTheory.MonObj.comp_mul, CategoryTheory.GrpObj.comp_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
⊢ η ▷ G ≫ commutator G =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst))
      (toUnit (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) G)) η

Tactic:
simp [commutator, comp_mul, comp_inv, one_eq_one]

Premises used: CategoryTheory.GrpObj.commutator, CategoryTheory.MonObj.comp_mul, CategoryTheory.GrpObj.comp_inv, CategoryTheory.MonObj.one_eq_one
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
G : C
inst_2 : GrpObj G
⊢ G ◁ η ≫ commutator G =
    CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst))
      (toUnit (tensorObj.{v, u} (𝒞 := inst) G (tensorUnit.{v, u} C (𝒞 := inst)))) η

Tactic:
simp [commutator, comp_mul, comp_inv, one_eq_one]

Premises used: CategoryTheory.GrpObj.commutator, CategoryTheory.MonObj.comp_mul, CategoryTheory.GrpObj.comp_inv, CategoryTheory.MonObj.one_eq_one
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
inst_5 : BraidedCategory.{v, u} C
inst_6 : IsCommMonObj.{v, u} G
⊢ Eq.{v + 1} (α := tensorUnit.{v, u} C (𝒞 := inst) ⟶ G) (η ≫ @GrpObj.inv _ _ inst_1 _ _) η

Tactic:
simp [one_eq_one, ← Hom.inv_def]

Premises used: CategoryTheory.Hom.inv_def, CategoryTheory.MonObj.one_eq_one