awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : C
inst_2 : GrpObj A
s :
  PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ
m : s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ Iso.hom (α_ A A A) ≫ A ◁ μ = s.snd
⊢ m ≫ snd (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)
      ((fun
            (s :
              PullbackCone.{v₁, u₁} (C := C) (X := tensorObj.{v₁, u₁} (𝒞 := inst) A A) (Y :=
                tensorObj.{v₁, u₁} (𝒞 := inst) A A) μ μ) ↦
          (lift
              (lift (s.snd ≫ fst A A)
                (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A)
                  (lift (s.snd ≫ fst A A ≫ @inv _ _ inst_1 _ _) (s.fst ≫ fst A A)) μ))
              (s.fst ≫ snd A A) :
            s.pt ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A))
        s)
      (snd (tensorObj.{v₁, u₁} (𝒞 := inst) A A) A)

Tactic:
simpa using hm₁ =≫ snd _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.snd
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
this :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f)
⊢ @inv _ _ inst_1 _ _ ≫ f = f ≫ @inv _ _ inst_1 _ _

Tactic:
simpa using (this =≫ fst _ _) =≫ snd _ _

Premises used: CategoryTheory.eq_whisker, CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.SemiCartesianMonoidalCategory.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
suffices :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f)
⊢ @inv _ _ inst_1 _ _ ≫ f = f ≫ @inv _ _ inst_1 _ _

Tactic:
suffices lift (lift f (ι ≫ f)) f =
      lift (lift f (f ≫ ι)) f by simpa using (this =≫ fst _ _) =≫ snd _ _
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
h₀ :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
h₁ :
  Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
    (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f)

Tactic:
apply (isPullback B).hom_ext

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.GrpObj.isPullback
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
h₀ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
      (fst B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
      (fst B B)
h₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
      (snd B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
      (snd B B)
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))

Tactic:
apply CartesianMonoidalCategory.hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
h₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B)
h₂ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (snd B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (snd B B)
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
    (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)

Tactic:
apply CartesianMonoidalCategory.hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
      (fst B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
      (fst B B)

Tactic:
simp [lift_inv_comp_right, lift_inv_comp_left]

Premises used: CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.GrpObj.lift_inv_comp_right
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f) (μ ▷ B))
      (snd B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) B B) B)
        (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f) (μ ▷ B))
      (snd B B)

Tactic:
simp [lift_inv_comp_right, lift_inv_comp_left]

Premises used: CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.GrpObj.lift_inv_comp_right
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B)

Tactic:
simp [lift_inv_comp_right, lift_inv_comp_left]

Premises used: CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.GrpObj.lift_inv_comp_right
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (snd B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (snd B B)

Tactic:
simp [lift_inv_comp_right, lift_inv_comp_left]

Premises used: CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.GrpObj.lift_inv_comp_right
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
this : Eq.{v₁ + 1} (α := X ⟶ X) (@inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)
mk :
  ∀ [toMonObj : MonObj X] (inv : X ⟶ X)
    (left_inv :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift inv (𝟙 X)) μ =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
    (right_inv :
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (𝟙 X) inv) μ =
        CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
    (e : Eq.{v₁ + 1} (α := MonObj X) GrpObj.toMonObj GrpObj.toMonObj)
    (this : Eq.{v₁ + 1} (α := X ⟶ X) (@GrpObj.inv _ _ inst_1 _ _) (@GrpObj.inv _ _ inst_1 _ _)),
    { toMonObj := toMonObj, inv := inv, left_inv := left_inv, right_inv := right_inv : GrpObj X } = h₂
⊢ h₁ = h₂

Tactic:
cases h₁
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₂ : GrpObj X
toMonObj : MonObj X
inv : X ⟶ X
left_inv :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift inv (𝟙 X)) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η
right_inv :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (𝟙 X) inv) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η
e : Eq.{v₁ + 1} (α := MonObj X) GrpObj.toMonObj GrpObj.toMonObj
this : Eq.{v₁ + 1} (α := X ⟶ X) (@GrpObj.inv _ _ inst_1 _ _) (@GrpObj.inv _ _ inst_1 _ _)
⊢ { toMonObj := toMonObj, inv := inv, left_inv := left_inv, right_inv := right_inv : GrpObj X } = h₂

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
suffices : Eq.{v₁ + 1} (α := X ⟶ X) (@inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)
⊢ h₁ = h₂

Tactic:
suffices h₁.inv = h₂.inv by cases h₁; congr!
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
apply :
  Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
⊢ Eq.{v₁ + 1} (α := X ⟶ X) (@inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)

Tactic:
apply lift_left_mul_ext (𝟙 _)

Premises used: CategoryTheory.GrpObj.lift_left_mul_ext, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
rw :
  Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)

Tactic:
rw [left_inv]

Premises used: CategoryTheory.GrpObj.left_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)

Tactic:
@left_inv _ _ _ _ h₁

Premises used: CategoryTheory.GrpObj.left_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
h : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
h₃ : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)

Tactic:
convert! @left_inv _ _ _ _ h₁ using 2

Premises used: CategoryTheory.GrpObj.left_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ

Tactic:
congr(($e.symm).mul)

Premises used: congrArg, id, Eq.symm, CategoryTheory.MonObj.mul
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η

Tactic:
congr(($e.symm).one)

Premises used: congrArg, id, CategoryTheory.MonObj.one, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ

Tactic:
exacts [congr(($e.symm).mul), congr(($e.symm).one)]
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
H : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ h₁ = h₂

Tactic:
GrpObj.toMonObj_injective H

Premises used: CategoryTheory.GrpObj.toMonObj_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
h₁ :
  ∀ (g : Functor.obj (Functor.obj yoneda G) X),
    Eq (α := Functor.obj (Functor.obj yoneda G) Y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj yoneda G) f ≫
            (fun (X : Cᵒᵖ) ↦
                (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                  Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
              Y))
        g)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((fun (X : Cᵒᵖ) ↦
                (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                  Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
              X ≫
            Functor.map (Functor.obj yoneda G) f))
        g)
⊢ Eq (α := Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) Y)
    (Functor.map (Functor.obj yoneda G) f ≫
      (fun (X : Cᵒᵖ) ↦
          (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
            Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
        Y)
    ((fun (X : Cᵒᵖ) ↦
          (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
            Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
        X ≫
      Functor.map (Functor.obj yoneda G) f)

Tactic:
ext g
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : Functor.obj (Functor.obj yoneda G) X
h₁ : f.unop ≫ @Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * f.unop ≫ g = 1
⊢ Eq (α := Functor.obj (Functor.obj yoneda G) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj yoneda G) f ≫
          (fun (X : Cᵒᵖ) ↦
              (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
            Y))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Cᵒᵖ) ↦
              (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
            X ≫
          Functor.map (Functor.obj yoneda G) f))
      g)

Tactic:
simp only [yoneda_obj_obj, yoneda_obj_map, TypeCat.Fun.toFun_apply, comp_apply,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, invOf_eq_iff_left]

Premises used: TypeCat.Fun.coe_mk, CategoryTheory.yoneda_obj_obj, CategoryTheory.yoneda_obj_map, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, invOf_eq_iff_left, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : Functor.obj (Functor.obj yoneda G) X
h₁ : f.unop ≫ (@Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * g) = 1
h₂ : Eq (α := Opposite.unop Y ⟶ G) (f.unop ≫ 1) 1
h₃ h₄ : Eq.{v₁ + 1} (α := Opposite.unop Y ⟶ G) 1 1
⊢ f.unop ≫ @Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * f.unop ≫ g = 1

Tactic:
rw [← comp_mul, invOf_mul_self, comp_one]

Premises used: CategoryTheory.MonObj.comp_one, invOf_mul_self, CategoryTheory.MonObj.comp_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
⊢ Eq.{v₁ + 1} (α := G ⟶ G)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) G G)
      (lift
        (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
          {
            app := fun (X : Cᵒᵖ) ↦
              ↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _,
            naturality := ⋯ })
        (𝟙 G))
      μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit G) η)

Tactic:
simp [Yoneda.fullyFaithful_preimage, ← Hom.mul_def, Hom.one_def]

Premises used: CategoryTheory.Hom.mul_def, CategoryTheory.Hom.one_def, CategoryTheory.Yoneda.fullyFaithful_preimage
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
⊢ Eq.{v₁ + 1} (α := G ⟶ G)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) G G)
      (lift (𝟙 G)
        (Functor.FullyFaithful.preimage Yoneda.fullyFaithful
          {
            app := fun (X : Cᵒᵖ) ↦
              ↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _,
            naturality := ⋯ }))
      μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit G) η)

Tactic:
simp [Yoneda.fullyFaithful_preimage, ← Hom.mul_def, Hom.one_def]

Premises used: CategoryTheory.Hom.mul_def, CategoryTheory.Hom.one_def, CategoryTheory.Yoneda.fullyFaithful_preimage
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
⊢ Functor.Full (C := Grp.{v₁, u₁} C) (forget₂Mon C)

Tactic:
InducedCategory.full _

Premises used: CategoryTheory.Grp.forget₂Mon, CategoryTheory.InducedCategory, CategoryTheory.InducedCategory.full
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
⊢ Functor.Faithful (C := Grp.{v₁, u₁} C) (forget₂Mon C)

Tactic:
InducedCategory.faithful _

Premises used: CategoryTheory.InducedCategory.faithful, CategoryTheory.Grp.forget₂Mon, CategoryTheory.InducedCategory
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : Grp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (Functor.obj (forget₂Mon C) A).X) η η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A : Grp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget₂Mon C) A).X (Functor.obj (forget₂Mon C) A).X ⟶
      (Functor.obj (forget₂Mon C) A).X)
    μ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : Grp.{v₁, u₁} C
f : A ⟶ B
⊢ Hom.hom (Functor.map (forget₂Mon C) f) = f.hom.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
⊢ Eq (α := Grp.{v₁, u₁} C ⥤ C) (forget₂Mon C ⋙ Mon.forget C) (forget C)

Tactic:
rfl

Premises used: CategoryTheory.Grp.forget, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G H : Grp.{v₁, u₁} C
f : G ⟶ H
inst_2 : IsIso f
⊢ IsIso f.hom.hom

Tactic:
inferInstanceAs <| IsIso <| (forget C).map f

Premises used: _private.0.CategoryTheory.Grp.instIsIsoHomHomMon._proof_1
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G H : Grp.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := G.toMon ⟶ H.toMon) (InducedCategory.Hom.hom 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Grp
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ X.{v₁, u₁} ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) = tensorUnit.{v₁, u₁} C (𝒞 := inst)

Tactic:
rfl

Premises used: rfl