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
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₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
h₁ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1)
    (CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
        (μ (F.prod G) x x_1) (δ (F.prod G) x x_1)).1
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))).1
h₂ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).2)
    (CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
        (μ (F.prod G) x x_1) (δ (F.prod G) x x_1)).2
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))).2
⊢ CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
      (μ (F.prod G) x x_1) (δ (F.prod G) x x_1) =
    𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((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₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).1)
    (CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
        (μ (F.prod G) x x_1) (δ (F.prod G) x x_1)).1
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))).1

Tactic:
apply Monoidal.μ_δ

Premises used: 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₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1)).2)
    (CategoryStruct.comp (Y := (F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))
        (μ (F.prod G) x x_1) (δ (F.prod G) x x_1)).2
    (𝟙 (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))).2

Tactic:
apply Monoidal.μ_δ

Premises used: 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₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
h₁ :
  Eq (α :=
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1 ⟶
      ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
        (δ (F.prod G) x x_1) (μ (F.prod G) x x_1)).1
    (𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))).1
h₂ :
  Eq (α :=
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).2 ⟶
      ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).2)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
        (δ (F.prod G) x x_1) (μ (F.prod G) x x_1)).2
    (𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))).2
⊢ CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
      (δ (F.prod G) x x_1) (μ (F.prod G) x x_1) =
    𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x 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₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
⊢ Eq (α :=
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1 ⟶
      ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).1)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
        (δ (F.prod G) x x_1) (μ (F.prod G) x x_1)).1
    (𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))).1

Tactic:
apply Monoidal.δ_μ

Premises used: 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₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.Monoidal
inst_9 : G.Monoidal
x x_1 : C × E
⊢ Eq (α :=
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).2 ⟶
      ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1)).2)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj x) ((F.prod G).obj x_1))
        (δ (F.prod G) x x_1) (μ (F.prod G) x x_1)).2
    (𝟙 ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) x x_1))).2

Tactic:
apply Monoidal.δ_μ

Premises used: CategoryTheory.Functor.Monoidal.δ_μ
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C) ⟶
      obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (diag C)) (𝟙 (tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C))
    (η (diag C)) (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
⊢ μ (diag C) X Y =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y))
    (δ (diag C) X Y) (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))

Tactic:
rfl

Premises used: 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.LaxMonoidal
inst_7 : G.LaxMonoidal
change :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      F.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)
    ((ε (F.prod G)).1 ≫ F.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)) (ε F)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' G)).1 (ε F)

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.LaxMonoidal
inst_7 : G.LaxMonoidal
rw :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      F.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)
    (ε (F.prod G)).1 (ε F)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      F.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)
    ((ε (F.prod G)).1 ≫ F.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)) (ε F)

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

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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.LaxMonoidal
inst_7 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      F.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).1)
    (ε (F.prod G)).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.LaxMonoidal
inst_7 : G.LaxMonoidal
change :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      G.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)
    ((ε (F.prod G)).2 ≫ G.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)) (ε G)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).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.LaxMonoidal
inst_7 : G.LaxMonoidal
rw :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      G.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)
    (ε (F.prod G)).2 (ε G)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      G.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)
    ((ε (F.prod G)).2 ≫ G.map (𝟙 tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)) (ε G)

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

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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.LaxMonoidal
inst_7 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      G.obj tensorUnit.{v₁, u₁} (C × C) (𝒞 := uniformProd C C).2)
    (ε (F.prod G)).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.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
change :
  Eq (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1)
    ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 ≫
      F.map
        (𝟙
          (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1))
    (μ F X Y)
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).1 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X 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.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
rw :
  Eq (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) 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 (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1)
    ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).1 ≫
      F.map
        (𝟙
          (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (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.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
⊢ Eq (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) 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:
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.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
change :
  Eq (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2)
    ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 ≫
      G.map
        (𝟙
          (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
              (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2))
    (μ G X Y)
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj X) ((F.prod' G).obj Y)).2 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X 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.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
rw :
  Eq (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) 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 (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2)
    ((μ (F.prod G) (obj.{v₁, v₁, u₁, u₁} (diag C) X) (obj.{v₁, v₁, u₁, u₁} (diag C) Y)).2 ≫
      G.map
        (𝟙
          (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (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.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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.LaxMonoidal
inst_7 : G.LaxMonoidal
X Y : C
⊢ Eq (α :=
    (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.obj
        (tensorObj.{v₁, u₁} (𝒞 := uniformProd C C) (obj.{v₁, v₁, u₁, u₁} (diag C) X)
            (obj.{v₁, v₁, u₁, u₁} (diag C) 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:
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 (α :=
    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.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) ≫ (η (F.prod G)).1) (η F)
⊢ Eq (α :=
    ((F.prod' G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 ⟶
      (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1)
    (η (F.prod' G)).1 (η F)

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
rw :
  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)
⊢ 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.map (𝟙 (obj.{v₁, v₁, u₁, u₁} (diag C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) ≫ (η (F.prod G)).1) (η F)

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

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp