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 : Functor.{v₁, v₂, u₁, u₂} C D
εIso : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ≅ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μIso : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    Iso.inv (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality :
  ∀ (X : C),
    Iso.inv (λ_ (F.obj X)) =
      F.map (Iso.inv (λ_ X)) ≫ Iso.inv (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ εIso.inv ▷ F.obj X
oplax_right_unitality :
  ∀ (X : C),
    Iso.inv (ρ_ (F.obj X)) =
      F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv
X : C
rw :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    (F.obj X ◁ εIso.hom ≫ Iso.hom (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ X))) ≫
      F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv
⊢ Iso.hom (ρ_ (F.obj X)) =
    F.obj X ◁ εIso.hom ≫ Iso.hom (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ X))

Tactic:
rw [← cancel_mono (ρ_ (F.obj X)).inv, Iso.hom_inv_id, oplax_right_unitality]

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.Iso.hom_inv_id, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
εIso : tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ≅ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))
μIso : (X Y : C) → tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ≅ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    Iso.inv (μIso (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
        (μIso X Y).inv ▷ F.obj Z ≫ Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) =
      F.map (Iso.hom (α_ X Y Z)) ≫ Iso.inv (μIso X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality :
  ∀ (X : C),
    Iso.inv (λ_ (F.obj X)) =
      F.map (Iso.inv (λ_ X)) ≫ Iso.inv (μIso (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ εIso.inv ▷ F.obj X
oplax_right_unitality :
  ∀ (X : C),
    Iso.inv (ρ_ (F.obj X)) =
      F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv
X : C
⊢ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    (F.obj X ◁ εIso.hom ≫ Iso.hom (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.map (Iso.hom (ρ_ X))) ≫
      F.map (Iso.inv (ρ_ X)) ≫ Iso.inv (μIso X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ F.obj X ◁ εIso.inv

Tactic:
simp
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
rw :
  (h.μIso X x_1).hom ≫ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 =
    (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
rw₁ : F.map x ▷ F.obj x_1 = (h.μIso X x_1).hom ≫ F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv
rw₂ : F.map x ▷ F.obj x_1 = F.map x ▷ F.obj x_1 ≫ (h.μIso Y x_1).hom ≫ (h.μIso Y x_1).inv
rw₃ : F.map x ▷ F.obj x_1 = F.map x ▷ F.obj x_1 ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))
rw₄ rw₅ :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))
    (F.map x ▷ F.obj x_1) (F.map x ▷ F.obj x_1)
⊢ (h.μIso X x_1).inv ≫ F.map x ▷ F.obj x_1 = F.map (x ▷ x_1) ≫ (h.μIso Y x_1).inv

Tactic:
rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Functor.CoreMonoidal.μIso, CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_left_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
X Y x : C
x_1 : X ⟶ Y
rw : (h.μIso x X).hom ≫ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
rw₁ : F.obj x ◁ F.map x_1 = (h.μIso x X).hom ≫ F.map (x ◁ x_1) ≫ (h.μIso x Y).inv
rw₂ : F.obj x ◁ F.map x_1 = F.obj x ◁ F.map x_1 ≫ (h.μIso x Y).hom ≫ (h.μIso x Y).inv
rw₃ : F.obj x ◁ F.map x_1 = F.obj x ◁ F.map x_1 ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
rw₄ rw₅ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
    (F.obj x ◁ F.map x_1) (F.obj x ◁ F.map x_1)
⊢ (h.μIso x X).inv ≫ F.obj x ◁ F.map x_1 = F.map (x ◁ x_1) ≫ (h.μIso x Y).inv

Tactic:
rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_right_assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Functor.CoreMonoidal.μIso, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.CoreMonoidal.μIso_hom_natural_right_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
inst_7 : F.OplaxMonoidal
inst_8 : IsIso (X := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F)
inst_9 :
  ∀ (X Y : C),
    IsIso (X := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (δ F X Y)
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Iso.hom (Iso.symm (asIso (δ F X Y))) ▷ F.obj Z ≫
      Iso.hom (Iso.symm (asIso (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))) ≫ F.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
      F.obj X ◁ Iso.hom (Iso.symm (asIso (δ F Y Z))) ≫
        Iso.hom (Iso.symm (asIso (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))))

Tactic:
simp [← cancel_epi (δ F X Y ▷ F.obj Z), ← cancel_epi (δ F (X ⊗ Y) Z)]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.cancel_epi, CategoryTheory.Functor.obj
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
inst_7 : F.OplaxMonoidal
inst_8 : IsIso (X := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F)
inst_9 :
  ∀ (X Y : C),
    IsIso (X := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (δ F X Y)
X : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj X) ⟶ F.obj X)
    (Iso.hom (λ_ (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (Iso.hom (Iso.symm (asIso (η F))) ▷ F.obj X)
      (Iso.hom (Iso.symm (asIso (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))) ≫ F.map (Iso.hom (λ_ X))))

Tactic:
simp [← cancel_epi (λ_ (F.obj X)).inv]

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
h : F.CoreMonoidal
inst_7 : F.OplaxMonoidal
inst_8 : IsIso (X := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F)
inst_9 :
  ∀ (X Y : C),
    IsIso (X := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
      (δ F X Y)
X : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ F.obj X)
    (Iso.hom (ρ_ (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.obj X ◁ Iso.hom (Iso.symm (asIso (η F))))
      (Iso.hom (Iso.symm (asIso (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))) ≫ F.map (Iso.hom (ρ_ X))))

Tactic:
simp [← cancel_epi (ρ_ (F.obj X)).inv]

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- 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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₃, v₁', u₃, u₁'} E C'
inst_7 : MonoidalCategory.{v₁', u₁'} C'
inst_8 : F.LaxMonoidal
inst_9 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1 ⟶
      ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).1)
    (ε (F.prod G)).1 (ε F)

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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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.LaxMonoidal
inst_9 : G.LaxMonoidal
⊢ Eq (α :=
    (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').2 ⟶
      ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).2)
    (ε (F.prod G)).2 (ε G)

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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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.LaxMonoidal
inst_9 : G.LaxMonoidal
X Y : C × E
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj X) ((F.prod G).obj Y)).1 ⟶
      ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) X Y)).1)
    (μ (F.prod G) X Y).1 (μ F X.1 Y.1)

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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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.LaxMonoidal
inst_9 : G.LaxMonoidal
X Y : C × E
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj X) ((F.prod G).obj Y)).2 ⟶
      ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) X Y)).2)
    (μ (F.prod G) X Y).2 (μ G X.2 Y.2)

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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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.OplaxMonoidal
inst_9 : G.OplaxMonoidal
⊢ Eq (α :=
    ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).1 ⟶
      (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1)
    (η (F.prod G)).1 (η F)

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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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.OplaxMonoidal
inst_9 : G.OplaxMonoidal
⊢ Eq (α :=
    ((F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E))).2 ⟶
      (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').2)
    (η (F.prod G)).2 (η G)

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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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.OplaxMonoidal
inst_9 : G.OplaxMonoidal
X Y : C × E
⊢ Eq (α :=
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) X Y)).1 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj X) ((F.prod G).obj Y)).1)
    (δ (F.prod G) X Y).1 (δ F X.1 Y.1)

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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
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.OplaxMonoidal
inst_9 : G.OplaxMonoidal
X Y : C × E
⊢ Eq (α :=
    ((F.prod G).obj (tensorObj (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E) X Y)).2 ⟶
      (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C') ((F.prod G).obj X) ((F.prod G).obj Y)).2)
    (δ (F.prod G) X Y).2 (δ G X.2 Y.2)

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
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
h₁ :
  Eq (α :=
    Quiver.Hom.{v₂, u₂} (V := D) (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1
      (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').1)
    (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
        (ε (F.prod G)) (η (F.prod G))).1
    (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))).1
h₂ :
  Eq (α :=
    Quiver.Hom.{v₁', u₁'} (V := C') (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').2
      (𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C').2)
    (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
        (ε (F.prod G)) (η (F.prod G))).2
    (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))).2
⊢ Eq (α :=
    Quiver.Hom (V := D × C') ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C'))
      ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')))
    (CategoryStruct.comp (Y := (F.prod G).obj ((𝟙_ (C × E)) (𝒞 := CategoryTheory.prod'.{v₁, v₃, u₁, u₃} C E)))
      (ε (F.prod G)) (η (F.prod G)))
    (𝟙 ((𝟙_ (D × C')) (𝒞 := CategoryTheory.prod'.{v₂, v₁', u₂, u₁'} D C')))

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

Tactic:
apply Monoidal.η_ε

Premises used: CategoryTheory.Functor.Monoidal.η_ε