awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
⊢ Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)))
        (pullback.fst f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (pullback.fst f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X A B R S Y Z : C
f : R ⟶ X
g : S ⟶ X
inst_2 : MonObj (mk f)
⊢ Eq (α :=
    Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
        (pullback.snd f (𝟙 X)) ⟶
      R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (CategoryStruct.comp (Y := Limits.pullback (X := Limits.pullback f f) (pullback.fst f f ≫ f) (𝟙 X))
          (Hom.left (LaxMonoidal.μ (pullback (𝟙 X)) (mk f) (mk f))) (pullback.fst (pullback.fst f f ≫ f) (𝟙 X)))
        (pullback.snd f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)
    (CategoryStruct.comp (Y := Limits.pullback f f)
        (Hom.left (homMk (pullback.fst f (𝟙 X)) ⋯ ⊗ₘ homMk (pullback.fst f (𝟙 X)) ⋯)) (pullback.snd f f) :
      Limits.pullback (X := Limits.pullback f (𝟙 X)) (Y := Limits.pullback f (𝟙 X)) (pullback.snd f (𝟙 X))
          (pullback.snd f (𝟙 X)) ⟶
        R)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := Opposite.unop Y ⟶ R) (f.unop ≫ 1) 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := Opposite.unop Y ⟶ R) (f.unop ≫ 0) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : RingObj R
X Y : Cᵒᵖ
f : X ⟶ Y
x : Opposite.unop X ⟶ R
⊢ (ConcreteCategory.hom (FC := fun (R S : RingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := RingCat.carrier) (X :=
          RingCat.of (Opposite.unop X ⟶ R)) (Y := RingCat.of (Opposite.unop Y ⟶ R))
          (Functor.map (yonedaRingObj R) f : Functor.obj (yonedaRingObj R) X ⟶ Functor.obj (yonedaRingObj R) Y) :
        (a : Opposite.unop X ⟶ R) → Opposite.unop Y ⟶ R)
      x =
    f.unop ≫ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X_1 Y : RingObjCat.{v, u} C
f : X_1 ⟶ Y
X : Cᵒᵖ
⊢ Eq (α := Opposite.unop X ⟶ Y.X) (1 ≫ f.hom) 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X_1 Y : RingObjCat.{v, u} C
f : X_1 ⟶ Y
X : Cᵒᵖ
⊢ Eq (α := Opposite.unop X ⟶ Y.X) (0 ≫ f.hom) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R : C
inst_3 : CommRingObj R
X Y : Cᵒᵖ
f : X ⟶ Y
x : Opposite.unop X ⟶ R
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
          CommRingCat.carrier) (X := CommRingCat.of (Opposite.unop X ⟶ R)) (Y := CommRingCat.of (Opposite.unop Y ⟶ R))
          (Functor.map (yonedaCommRingObj R) f :
            Functor.obj (yonedaCommRingObj R) X ⟶ Functor.obj (yonedaCommRingObj R) Y) :
        (a : Opposite.unop X ⟶ R) → Opposite.unop Y ⟶ R)
      x =
    f.unop ≫ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X_1 Y : CommRingObjCat.{v, u} C
f : X_1 ⟶ Y
X : Cᵒᵖ
⊢ Eq (α := Opposite.unop X ⟶ Y.X) (1 ≫ f.hom) 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X_1 Y : CommRingObjCat.{v, u} C
f : X_1 ⟶ Y
X : Cᵒᵖ
⊢ Eq (α := Opposite.unop X ⟶ Y.X) (0 ≫ f.hom) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
R₁ R₂ : CommRingObjCat.{v, u} C
f : R₁ ⟶ R₂
X : C
x : X ⟶ R₁.X
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
          CommRingCat.carrier) (X := CommRingCat.of (X ⟶ R₁.X)) (Y := CommRingCat.of (X ⟶ R₂.X))
          (NatTrans.app (Functor.map yonedaCommRing f) (Opposite.op X) :
            Functor.obj (yonedaCommRingObj R₁.X) (Opposite.op X) ⟶
              Functor.obj (yonedaCommRingObj R₂.X) (Opposite.op X)) :
        (a : X ⟶ R₁.X) → X ⟶ R₂.X)
      x =
    x ≫ f.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Mon.{v, u} C
X : Cᵒᵖ
dsimp : Small.{w, v} (unop X ⟶ M.X)
⊢ Small.{w, v} (↑((Functor.obj yonedaMon M).obj X) : Type v)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Mon.{v, u} C
X : Cᵒᵖ
⊢ Small.{w, v} (unop X ⟶ M.X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Grp.{v, u} C
X : Cᵒᵖ
dsimp : Small.{w, v} (unop X ⟶ M.X)
⊢ Small.{w, v} (↑((Functor.obj yonedaGrp M).obj X) : Type v)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Grp.{v, u} C
X : Cᵒᵖ
⊢ Small.{w, v} (unop X ⟶ M.X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Mon.{v, u} C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ M.X
⊢ Eq (α := (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj Y') : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            ((Functor.obj shrinkYonedaMon.{w, v, u} M).map g) :
          (a : (↑((shrinkYonedaMon.{w, v, u}.obj M).obj Y) : Type w)) →
            (↑((shrinkYonedaMon.{w, v, u}.obj M).obj Y') : Type w))
        ((MulEquiv.symm shrinkYonedaMonObjObjEquiv :
              (a : unop Y ⟶ M.X) → (↑((shrinkYonedaMon.{w, v, u}.obj M).obj Y) : Type w))
            f :
          (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj Y) : Type w)) :
      (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj Y') : Type w))
    ((MulEquiv.symm shrinkYonedaMonObjObjEquiv :
          (a : unop Y' ⟶ M.X) → (↑((shrinkYonedaMon.{w, v, u}.obj M).obj Y') : Type w))
        (g.unop ≫ f) :
      (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj Y') : Type w))

Tactic:
simp [shrinkYonedaMon, shrinkYonedaMonObjObjEquiv]

Premises used: CategoryTheory.shrinkYonedaMonObjObjEquiv, CategoryTheory.shrinkYonedaMon
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Mon.{v, u} C
Y Y' : C
g : Y' ⟶ Y
f : Y ⟶ M.X
⊢ Eq.{w + 1} (α := (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj (op Y')) : Type w))
    ((MulEquiv.symm shrinkYonedaMonObjObjEquiv :
          (a : unop (op Y') ⟶ M.X) → (↑((shrinkYonedaMon.{w, v, u}.obj M).obj (op Y')) : Type w))
        (g ≫ f) :
      (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj (op Y')) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            ((Functor.obj shrinkYonedaMon.{w, v, u} M).map g.op) :
          (a : (↑((shrinkYonedaMon.{w, v, u}.obj M).obj (op Y)) : Type w)) →
            (↑((shrinkYonedaMon.{w, v, u}.obj M).obj (op Y')) : Type w))
        ((MulEquiv.symm shrinkYonedaMonObjObjEquiv :
              (a : unop (op Y) ⟶ M.X) → (↑((shrinkYonedaMon.{w, v, u}.obj M).obj (op Y)) : Type w))
            f :
          (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj (op Y)) : Type w)) :
      (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj (op Y')) : Type w))

Tactic:
(shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm g.op f).symm

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M M' : Mon.{v, u} C
Y : Cᵒᵖ
f : unop Y ⟶ M.X
g : M ⟶ M'
⊢ Eq (α := (↑((Functor.obj shrinkYonedaMon.{w, v, u} M').obj Y) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (X := (Functor.obj shrinkYonedaMon.{w, v, u} M).obj Y)
            (NatTrans.app (Functor.map shrinkYonedaMon.{w, v, u} g) Y) :
          (a : (↑((shrinkYonedaMon.{w, v, u}.obj M).obj Y) : Type w)) →
            (↑((shrinkYonedaMon.{w, v, u}.obj M').obj Y) : Type w))
        ((MulEquiv.symm shrinkYonedaMonObjObjEquiv :
              (a : unop Y ⟶ M.X) → (↑((shrinkYonedaMon.{w, v, u}.obj M).obj Y) : Type w))
            f :
          (↑((Functor.obj shrinkYonedaMon.{w, v, u} M).obj Y) : Type w)) :
      (↑((Functor.obj shrinkYonedaMon.{w, v, u} M').obj Y) : Type w))
    ((MulEquiv.symm shrinkYonedaMonObjObjEquiv :
          (a : unop Y ⟶ M'.X) → (↑((shrinkYonedaMon.{w, v, u}.obj M').obj Y) : Type w))
        (f ≫ g.hom) :
      (↑((Functor.obj shrinkYonedaMon.{w, v, u} M').obj Y) : Type w))

Tactic:
simp [shrinkYonedaMon, shrinkYonedaMonObjObjEquiv]

Premises used: CategoryTheory.shrinkYonedaMonObjObjEquiv, CategoryTheory.shrinkYonedaMon
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Grp.{v, u} C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ M.X
⊢ Eq (α := (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj Y') : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
            ((Functor.obj shrinkYonedaGrp.{w, v, u} M).map g) :
          (a : (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj Y) : Type w)) →
            (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj Y') : Type w))
        ((MulEquiv.symm shrinkYonedaGrpObjObjEquiv :
              (a : unop Y ⟶ M.X) → (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj Y) : Type w))
            f :
          (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj Y) : Type w)) :
      (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj Y') : Type w))
    ((MulEquiv.symm shrinkYonedaGrpObjObjEquiv :
          (a : unop Y' ⟶ M.X) → (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj Y') : Type w))
        (g.unop ≫ f) :
      (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj Y') : Type w))

Tactic:
simp [shrinkYonedaGrp, shrinkYonedaGrpObjObjEquiv]

Premises used: CategoryTheory.shrinkYonedaGrp, CategoryTheory.shrinkYonedaGrpObjObjEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M : Grp.{v, u} C
Y Y' : C
g : Y' ⟶ Y
f : Y ⟶ M.X
⊢ Eq.{w + 1} (α := (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj (op Y')) : Type w))
    ((MulEquiv.symm shrinkYonedaGrpObjObjEquiv :
          (a : unop (op Y') ⟶ M.X) → (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj (op Y')) : Type w))
        (g ≫ f) :
      (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj (op Y')) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
            ((Functor.obj shrinkYonedaGrp.{w, v, u} M).map g.op) :
          (a : (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj (op Y)) : Type w)) →
            (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj (op Y')) : Type w))
        ((MulEquiv.symm shrinkYonedaGrpObjObjEquiv :
              (a : unop (op Y) ⟶ M.X) → (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj (op Y)) : Type w))
            f :
          (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj (op Y)) : Type w)) :
      (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj (op Y')) : Type w))

Tactic:
(shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm g.op f).symm

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
M M' : Grp.{v, u} C
Y : Cᵒᵖ
f : unop Y ⟶ M.X
g : M ⟶ M'
⊢ Eq (α := (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M').obj Y) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
            (X := (Functor.obj shrinkYonedaGrp.{w, v, u} M).obj Y)
            (NatTrans.app (Functor.map shrinkYonedaGrp.{w, v, u} g) Y) :
          (a : (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj Y) : Type w)) →
            (↑((shrinkYonedaGrp.{w, v, u}.obj M').obj Y) : Type w))
        ((MulEquiv.symm shrinkYonedaGrpObjObjEquiv :
              (a : unop Y ⟶ M.X) → (↑((shrinkYonedaGrp.{w, v, u}.obj M).obj Y) : Type w))
            f :
          (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M).obj Y) : Type w)) :
      (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M').obj Y) : Type w))
    ((MulEquiv.symm shrinkYonedaGrpObjObjEquiv :
          (a : unop Y ⟶ M'.X) → (↑((shrinkYonedaGrp.{w, v, u}.obj M').obj Y) : Type w))
        (f ≫ g.hom.hom) :
      (↑((Functor.obj shrinkYonedaGrp.{w, v, u} M').obj Y) : Type w))

Tactic:
simp [shrinkYonedaGrp, shrinkYonedaGrpObjObjEquiv]

Premises used: CategoryTheory.shrinkYonedaGrp, CategoryTheory.shrinkYonedaGrpObjObjEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategoryStruct.{v, u} C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X₁ X₂)
id_tensorHom :
  ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y₁ ⟶ tensorObj.{v, u} (𝒞 := inst) X Y₂) (𝟙 X ⊗ₘ f) (X ◁ f)
tensorHom_id :
  ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y ⟶ tensorObj.{v, u} (𝒞 := inst) X₂ Y) (f ⊗ₘ 𝟙 Y) (f ▷ Y)
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ X₂ ⟶ tensorObj.{v, u} (𝒞 := inst) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
      (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Eq (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X₁ X₂) X₃ ⟶
        tensorObj.{v, u} (𝒞 := inst) Y₁ (tensorObj.{v, u} (𝒞 := inst) Y₂ Y₃))
      (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ hom (α_ Y₁ Y₂ Y₃)) (hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
leftUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ f) ≫ hom (λ_ Y) = hom (λ_ X) ≫ f
rightUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ Y) = hom (ρ_ X) ≫ f
pentagon :
  ∀ (W X Y Z : C),
    (hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ (𝟙 W ⊗ₘ hom (α_ X Y Z)) =
      hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))
triangle :
  ∀ (X Y : C),
    Eq.{v + 1} (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) Y ⟶
        tensorObj.{v, u} (𝒞 := inst) X Y)
      (hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ (𝟙 X ⊗ₘ hom (λ_ Y))) (hom (ρ_ X) ⊗ₘ 𝟙 Y)
X₁ Y₁ X₂ Y₂ : C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ X₂ ⟶ tensorObj.{v, u} (𝒞 := inst) Y₁ Y₂) (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ g)

Tactic:
simp [← id_tensorHom, ← tensorHom_id, tensorHom_comp_tensorHom]
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategoryStruct.{v, u} C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X₁ X₂)
id_tensorHom :
  ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y₁ ⟶ tensorObj.{v, u} (𝒞 := inst) X Y₂) (𝟙 X ⊗ₘ f) (X ◁ f)
tensorHom_id :
  ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y ⟶ tensorObj.{v, u} (𝒞 := inst) X₂ Y) (f ⊗ₘ 𝟙 Y) (f ▷ Y)
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ X₂ ⟶ tensorObj.{v, u} (𝒞 := inst) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
      (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Eq (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X₁ X₂) X₃ ⟶
        tensorObj.{v, u} (𝒞 := inst) Y₁ (tensorObj.{v, u} (𝒞 := inst) Y₂ Y₃))
      (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ hom (α_ Y₁ Y₂ Y₃)) (hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
leftUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ f) ≫ hom (λ_ Y) = hom (λ_ X) ≫ f
rightUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ Y) = hom (ρ_ X) ≫ f
pentagon :
  ∀ (W X Y Z : C),
    (hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ (𝟙 W ⊗ₘ hom (α_ X Y Z)) =
      hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))
triangle :
  ∀ (X Y : C),
    Eq.{v + 1} (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) Y ⟶
        tensorObj.{v, u} (𝒞 := inst) X Y)
      (hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ (𝟙 X ⊗ₘ hom (λ_ Y))) (hom (ρ_ X) ⊗ₘ 𝟙 Y)
X Y : C
⊢ X ◁ 𝟙 Y = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)

Tactic:
simp [← id_tensorHom, ← id_tensorHom_id]
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategoryStruct.{v, u} C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X₁ X₂)
id_tensorHom :
  ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y₁ ⟶ tensorObj.{v, u} (𝒞 := inst) X Y₂) (𝟙 X ⊗ₘ f) (X ◁ f)
tensorHom_id :
  ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y ⟶ tensorObj.{v, u} (𝒞 := inst) X₂ Y) (f ⊗ₘ 𝟙 Y) (f ▷ Y)
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ X₂ ⟶ tensorObj.{v, u} (𝒞 := inst) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
      (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Eq (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X₁ X₂) X₃ ⟶
        tensorObj.{v, u} (𝒞 := inst) Y₁ (tensorObj.{v, u} (𝒞 := inst) Y₂ Y₃))
      (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ hom (α_ Y₁ Y₂ Y₃)) (hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
leftUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ f) ≫ hom (λ_ Y) = hom (λ_ X) ≫ f
rightUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ Y) = hom (ρ_ X) ≫ f
pentagon :
  ∀ (W X Y Z : C),
    (hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ (𝟙 W ⊗ₘ hom (α_ X Y Z)) =
      hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))
triangle :
  ∀ (X Y : C),
    Eq.{v + 1} (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) Y ⟶
        tensorObj.{v, u} (𝒞 := inst) X Y)
      (hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ (𝟙 X ⊗ₘ hom (λ_ Y))) (hom (ρ_ X) ⊗ₘ 𝟙 Y)
X Y : C
⊢ 𝟙 X ▷ Y = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)

Tactic:
simp [← tensorHom_id, id_tensorHom_id]
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategoryStruct.{v, u} C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X₁ X₂)
id_tensorHom :
  ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y₁ ⟶ tensorObj.{v, u} (𝒞 := inst) X Y₂) (𝟙 X ⊗ₘ f) (X ◁ f)
tensorHom_id :
  ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y ⟶ tensorObj.{v, u} (𝒞 := inst) X₂ Y) (f ⊗ₘ 𝟙 Y) (f ▷ Y)
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ X₂ ⟶ tensorObj.{v, u} (𝒞 := inst) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
      (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Eq (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X₁ X₂) X₃ ⟶
        tensorObj.{v, u} (𝒞 := inst) Y₁ (tensorObj.{v, u} (𝒞 := inst) Y₂ Y₃))
      (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ hom (α_ Y₁ Y₂ Y₃)) (hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
leftUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ f) ≫ hom (λ_ Y) = hom (λ_ X) ≫ f
rightUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ Y) = hom (ρ_ X) ≫ f
pentagon :
  ∀ (W X Y Z : C),
    (hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ (𝟙 W ⊗ₘ hom (α_ X Y Z)) =
      hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))
triangle :
  ∀ (X Y : C),
    Eq.{v + 1} (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) Y ⟶
        tensorObj.{v, u} (𝒞 := inst) X Y)
      (hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ (𝟙 X ⊗ₘ hom (λ_ Y))) (hom (ρ_ X) ⊗ₘ 𝟙 Y)
W X Y Z : C
⊢ hom (α_ W X Y) ▷ Z ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ W ◁ hom (α_ X Y Z) =
    hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))

Tactic:
simp [← id_tensorHom, ← tensorHom_id, pentagon]