awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
⊢ Eq (α :=
    F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    ((η (F.prod G)).1 :
      ((F.prod G).obj (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C))).1 ⟶
        (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    (η F)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
change :
  Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (G.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) ≫ (η (F.prod G)).2) (η G)
⊢ Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (η (F.prod' G)).2 (η G)

Tactic:
change G.map (𝟙 _) ≫ _ = _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
rw :
  Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    ((η (F.prod G)).2 :
      ((F.prod G).obj (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C))).2 ⟶
        (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (η G)
⊢ Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (G.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) ≫ (η (F.prod G)).2) (η G)

Tactic:
rw [Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
⊢ Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    ((η (F.prod G)).2 :
      ((F.prod G).obj (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C))).2 ⟶
        (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (η G)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
X Y : C
change :
  Eq (α :=
    F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).1)
    (F.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1) ≫
      (δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1)
    (δ F X Y)
⊢ Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).1)
    (δ (F.prod' G) X Y).1 (δ F X Y)

Tactic:
change F.map (𝟙 _) ≫ _ = _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
X Y : C
rw :
  Eq (α :=
    F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).1)
    ((δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 :
      ((F.prod G).obj
            (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y))).1 ⟶
        (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
            ((diag C ⋙ F.prod G).obj Y)).1)
    (δ F X Y)
⊢ Eq (α :=
    F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).1)
    (F.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1) ≫
      (δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1)
    (δ F X Y)

Tactic:
rw [Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
X Y : C
⊢ Eq (α :=
    F.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).1)
    ((δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 :
      ((F.prod G).obj
            (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y))).1 ⟶
        (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
            ((diag C ⋙ F.prod G).obj Y)).1)
    (δ F X Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
X Y : C
change :
  Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).2)
    (G.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2) ≫
      (δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2)
    (δ G X Y)
⊢ Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).2)
    (δ (F.prod' G) X Y).2 (δ G X Y)

Tactic:
change G.map (𝟙 _) ≫ _ = _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
X Y : C
rw :
  Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).2)
    ((δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 :
      ((F.prod G).obj
            (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y))).2 ⟶
        (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
            ((diag C ⋙ F.prod G).obj Y)).2)
    (δ G X Y)
⊢ Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).2)
    (G.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2) ≫
      (δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2)
    (δ G X Y)

Tactic:
rw [Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_6 : F.OplaxMonoidal
inst_7 : G.OplaxMonoidal
X Y : C
⊢ Eq (α :=
    G.obj (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
          ((diag C ⋙ F.prod G).obj Y)).2)
    ((δ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 :
      ((F.prod G).obj
            (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y))).2 ⟶
        (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((diag C ⋙ F.prod G).obj X)
            ((diag C ⋙ F.prod G).obj Y)).2)
    (δ G X Y)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
h₁ :
  Eq (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G))).1
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))).1
h₂ :
  Eq (α :=
    Quiver.Hom.{v₃, u₃} (V := E) (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G))).2
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))).2
⊢ Eq (α :=
    Quiver.Hom (V := D × E) ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))
      ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)))
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G)))
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ Eq (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G))).1
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))).1

Tactic:
simp only [CategoryTheory.prod_comp_fst, prod'_ε_fst, prod'_η_fst, ε_η,
        prodMonoidal_tensorUnit, prod_id]

Premises used: CategoryTheory.Functor.prod'_ε_fst, CategoryTheory.Functor.Monoidal.ε_η, CategoryTheory.prod_id, CategoryTheory.MonoidalCategory.prodMonoidal_tensorUnit, CategoryTheory.prod_comp_fst, CategoryTheory.Functor.prod'_η_fst
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ Eq (α :=
    Quiver.Hom.{v₃, u₃} (V := E) (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F.prod' G)) (η (F.prod' G))).2
    (𝟙 ((𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E))).2

Tactic:
simp only [CategoryTheory.prod_comp_snd, prod'_ε_snd, prod'_η_snd, ε_η,
        prodMonoidal_tensorUnit, prod_id]

Premises used: CategoryTheory.Functor.Monoidal.ε_η, CategoryTheory.prod_id, CategoryTheory.MonoidalCategory.prodMonoidal_tensorUnit, CategoryTheory.Functor.prod'_η_snd, CategoryTheory.Functor.prod'_ε_snd, CategoryTheory.prod_comp_snd
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
h₁ :
  Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶ ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
        (ε (F.prod' G))).1
    (𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))).1
h₂ :
  Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶ ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
        (ε (F.prod' G))).2
    (𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))).2
⊢ CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
      (ε (F.prod' G)) =
    𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶ ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
        (ε (F.prod' G))).1
    (𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))).1

Tactic:
simp only [CategoryTheory.prod_comp_fst, prod'_ε_fst, prod'_η_fst, η_ε,
        prod_id, prod'_obj]

Premises used: CategoryTheory.Functor.prod'_ε_fst, CategoryTheory.prod_id, CategoryTheory.Functor.prod'_obj, CategoryTheory.prod_comp_fst, CategoryTheory.Functor.prod'_η_fst, CategoryTheory.Functor.Monoidal.η_ε
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
⊢ Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 ⟶ ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (CategoryStruct.comp (Y := (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E)) (η (F.prod' G))
        (ε (F.prod' G))).2
    (𝟙 ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))).2

Tactic:
simp only [CategoryTheory.prod_comp_snd, prod'_ε_snd, prod'_η_snd, η_ε,
        prod_id, prod'_obj]

Premises used: CategoryTheory.prod_id, CategoryTheory.Functor.prod'_obj, CategoryTheory.Functor.prod'_η_snd, CategoryTheory.Functor.prod'_ε_snd, CategoryTheory.Functor.Monoidal.η_ε, CategoryTheory.prod_comp_snd
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
h₁ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
        (δ (F.prod' G) x x_1)).1
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))).1
h₂ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).2)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
        (δ (F.prod' G) x x_1)).2
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))).2
⊢ CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
      (δ (F.prod' G) x x_1) =
    𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).1)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
        (δ (F.prod' G) x x_1)).1
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))).1

Tactic:
simp only [CategoryTheory.prod_comp_fst, prod'_μ_fst, prod'_δ_fst, μ_δ,
        prod'_obj, prodMonoidal_tensorObj, prod_id]

Premises used: CategoryTheory.Functor.prod'_μ_fst, CategoryTheory.prod_id, CategoryTheory.Functor.prod'_obj, CategoryTheory.Functor.prod'_δ_fst, CategoryTheory.prod_comp_fst, CategoryTheory.MonoidalCategory.prodMonoidal_tensorObj, CategoryTheory.Functor.Monoidal.μ_δ
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1)).2)
    (CategoryStruct.comp (Y := (F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)) (μ (F.prod' G) x x_1)
        (δ (F.prod' G) x x_1)).2
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))).2

Tactic:
simp only [CategoryTheory.prod_comp_snd, prod'_μ_snd, prod'_δ_snd, μ_δ,
        prod'_obj, prodMonoidal_tensorObj, prod_id]

Premises used: CategoryTheory.Functor.prod'_δ_snd, CategoryTheory.prod_id, CategoryTheory.Functor.prod'_obj, CategoryTheory.Functor.prod'_μ_snd, CategoryTheory.MonoidalCategory.prodMonoidal_tensorObj, CategoryTheory.Functor.Monoidal.μ_δ, CategoryTheory.prod_comp_snd