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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
⊢ Iso.hom (λ_ (G.obj X)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      ((𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⊗ₘ i.inv.app X) ≫ (LaxMonoidal.ε F ⊗ₘ 𝟙 (F.obj X)))
      (LaxMonoidal.μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X)) ≫ i.hom.app X)

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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
simp :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ G.obj X)
    (Iso.hom (ρ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (i.inv.app X ⊗ₘ LaxMonoidal.ε F)
      (LaxMonoidal.μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ G.map (Iso.hom (ρ_ X))))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ G.obj X)
    (Iso.hom (ρ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (G.obj X ◁ Iso.hom (εIso F ≪≫ i.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (Iso.hom
          ((i.symm.app X ⊗ᵢ i.symm.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≪≫
            μIso F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≪≫
              i.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        G.map (Iso.hom (ρ_ X))))

Tactic:
simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← id_tensorHom, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Category.id_comp,
      Iso.hom_inv_id_app, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.Monoidal.εIso_hom, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorIso_hom, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Iso.app_hom, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.Iso.trans_hom, 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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
rw :
  Iso.hom (ρ_ (G.obj X)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      ((i.inv.app X ⊗ₘ 𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≫ (𝟙 (F.obj X) ⊗ₘ LaxMonoidal.ε F))
      (LaxMonoidal.μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X)) ≫ i.hom.app X)
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶ G.obj X)
    (Iso.hom (ρ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (i.inv.app X ⊗ₘ LaxMonoidal.ε F)
      (LaxMonoidal.μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ G.map (Iso.hom (ρ_ X))))

Tactic:
rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, 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
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
⊢ Iso.hom (ρ_ (G.obj X)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      ((i.inv.app X ⊗ₘ 𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ≫ (𝟙 (F.obj X) ⊗ₘ LaxMonoidal.ε F))
      (LaxMonoidal.μ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.map (Iso.hom (ρ_ X)) ≫ i.hom.app X)

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
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
i : F ≅ G
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε G)
    (LaxMonoidal.ε F ≫ i.hom.app (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
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
i : F ≅ G
⊢ Eq (α := G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η G)
    (i.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ OplaxMonoidal.η 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
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
i : F ≅ G
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ G X Y)
    ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ LaxMonoidal.μ F X Y ≫ i.hom.app (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
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
i : F ≅ G
X Y : C
⊢ Eq (α := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y))
    (OplaxMonoidal.δ G X Y)
    (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ OplaxMonoidal.δ F X Y ≫ (i.hom.app X ⊗ₘ i.hom.app Y))

Tactic:
coreMonoidalTransport_μIso_inv _ _ _

Premises used: CategoryTheory.Functor.Monoidal.coreMonoidalTransport_μIso_inv
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    ((F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
⊢ (tensorObj F F').map f ≫ (α.app Y ⊗ₘ β.app Y) = (α.app X ⊗ₘ β.app X) ≫ (tensorObj G G').map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (F.map f ≫ α.app Y ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
rw₁ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (α.app X ≫ G.map f ⊗ₘ F'.map f ≫ β.app Y) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
rw₂ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    (α.app X ≫ G.map f ⊗ₘ β.app X ≫ G'.map f) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
rw₃ rw₄ :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (F'.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj Y) (G'.obj Y))
    ((F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y)) ((α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f))

Tactic:
rw [tensorHom_comp_tensorHom, α.naturality, β.naturality, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F_1 G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F_1 ⟶ G
β_1 : F' ⟶ G'
F : Functor.{v₁, v₂, u₁, u₂} C D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
simp : (tensorObj F F').map f ≫ (𝟙 (F.obj Y) ⊗ₘ β.app Y) = (𝟙 (F.obj X) ⊗ₘ β.app X) ≫ (tensorObj F G').map f
⊢ (tensorObj F F').map f ≫ F.obj Y ◁ β.app Y = F.obj X ◁ β.app X ≫ (tensorObj F G').map f

Tactic:
simp only [← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F_1 G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F_1 ⟶ G
β_1 : F' ⟶ G'
F : Functor.{v₁, v₂, u₁, u₂} C D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (𝟙 (F.obj Y) ⊗ₘ β.app Y) = (𝟙 (F.obj X) ⊗ₘ β.app X) ≫ (tensorObj F G').map f

Tactic:
apply (tensorHom (𝟙 F) β).naturality

Premises used: CategoryTheory.Monoidal.FunctorCategory.tensorHom, CategoryTheory.CategoryStruct.id, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F'_1 G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F'_1 ⟶ G'
F' : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
simp : (tensorObj F F').map f ≫ (α.app Y ⊗ₘ 𝟙 (F'.obj Y)) = (α.app X ⊗ₘ 𝟙 (F'.obj X)) ≫ (tensorObj G F').map f
⊢ (tensorObj F F').map f ≫ α.app Y ▷ F'.obj Y = α.app X ▷ F'.obj X ≫ (tensorObj G F').map f

Tactic:
simp only [← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F'_1 G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F'_1 ⟶ G'
F' : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (α.app Y ⊗ₘ 𝟙 (F'.obj Y)) = (α.app X ⊗ₘ 𝟙 (F'.obj X)) ≫ (tensorObj G F').map f

Tactic:
apply (tensorHom α (𝟙 F')).naturality

Premises used: CategoryTheory.Monoidal.FunctorCategory.tensorHom, CategoryTheory.CategoryStruct.id, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X : C
⊢ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X =
    tensorUnit.{v₂, u₂} D (𝒞 := inst_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom.{v₂, u₂} (V := D)
      (Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
      (Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y))
    (Functor.map ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) f)
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G).obj X =
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G).map f = F.map f ⊗ₘ G.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' G' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : F' ⟶ G'
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F F').obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G G').obj X)
    (NatTrans.app (α ⊗ₘ β) X) (α.app X ⊗ₘ β.app X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F F' G' : Functor.{v₁, v₂, u₁, u₂} C D
β : F' ⟶ G'
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F F').obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G').obj X)
    (NatTrans.app (F ◁ β) X) (F.obj X ◁ β.app X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G F' : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F F').obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G F').obj X)
    (NatTrans.app (α ▷ F') X) (α.app X ▷ F'.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) F).obj
        X ⟶
      F.obj X)
    (NatTrans.app (Iso.hom (λ_ F)) X) (Iso.hom (λ_ (F.obj X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    F.obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) F).obj
        X)
    (NatTrans.app (Iso.inv (λ_ F)) X) (Iso.inv (λ_ (F.obj X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
            ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category))).obj
        X ⟶
      F.obj X)
    (NatTrans.app (Iso.hom (ρ_ F)) X) (Iso.hom (ρ_ (F.obj X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    F.obj X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
            ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category))).obj
        X)
    (NatTrans.app (Iso.inv (ρ_ F)) X) (Iso.inv (ρ_ (F.obj X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H)).obj
        X)
    (NatTrans.app (Iso.hom (α_ F G H)) X) (Iso.hom (α_ (F.obj X) (G.obj X) (H.obj X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H)).obj
        X ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H).obj
        X)
    (NatTrans.app (Iso.inv (α_ F G H)) X) (Iso.inv (α_ (F.obj X) (G.obj X) (H.obj X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X₁ Y₁ X₂ Y₂ : Functor.{v₁, v₂, u₁, u₂} C D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
w :
  ∀ (x : C),
    Eq (α :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) X₁ X₂).obj x ⟶
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj x)
      (NatTrans.app (f ⊗ₘ g) x) (NatTrans.app (f ▷ X₂ ≫ Y₁ ◁ g) x)
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) X₁ X₂ ⟶
      MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) Y₁ Y₂)
    (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X₁ Y₁ X₂ Y₂ : Functor.{v₁, v₂, u₁, u₂} C D
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
x : C
⊢ Eq (α :=
    (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) X₁ X₂).obj x ⟶
      (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) Y₁ Y₂).obj x)
    (NatTrans.app (f ⊗ₘ g) x) (NatTrans.app (f ▷ X₂ ≫ Y₁ ◁ g) x)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H K : Functor.{v₁, v₂, u₁, u₂} C D
w :
  ∀ (X : C),
    NatTrans.app
        (Iso.hom (α_ F G H) ▷ K ≫
          Iso.hom (α_ F (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) K) ≫ F ◁ Iso.hom (α_ G H K))
        X =
      (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H K) ≫
            Iso.hom (α_ F G (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H K))).app
        X
⊢ Iso.hom (α_ F G H) ▷ K ≫
      Iso.hom (α_ F (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) K) ≫ F ◁ Iso.hom (α_ G H K) =
    Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H K) ≫
      Iso.hom (α_ F G (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H K))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
F G H K : Functor.{v₁, v₂, u₁, u₂} C D
X : C
w :
  Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X))
        (K.obj X) ⟶
      MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X)
        (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X)
          (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
    (Iso.hom (α_ (F.obj X) (G.obj X) (H.obj X)) ▷ K.obj X ≫
      Iso.hom (α_ (F.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (G.obj X) (H.obj X)) (K.obj X)) ≫
        F.obj X ◁ Iso.hom (α_ (G.obj X) (H.obj X) (K.obj X)))
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj X) (G.obj X)) (H.obj X) (K.obj X)) ≫
      Iso.hom (α_ (F.obj X) (G.obj X) (MonoidalCategoryStruct.tensorObj.{v₂, u₂} (𝒞 := inst_1) (H.obj X) (K.obj X))))
⊢ NatTrans.app
      (Iso.hom (α_ F G H) ▷ K ≫
        Iso.hom (α_ F (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) G H) K) ≫ F ◁ Iso.hom (α_ G H K))
      X =
    (Iso.hom (α_ (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) F G) H K) ≫
          Iso.hom (α_ F G (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category) H K))).app
      X

Tactic:
dsimp