[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (fun X => NatTrans.app α X ⊗ NatTrans.app β X) Y =
    (fun X => NatTrans.app α X ⊗ NatTrans.app β X) X ≫ (tensorObj G G').map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (F.map f ⊗ F'.map f) ≫ (NatTrans.app α Y ⊗ NatTrans.app β Y) =
    (NatTrans.app α X ⊗ NatTrans.app β X) ≫ (G.map f ⊗ G'.map f)
[PROOFSTEP]
rw [← tensor_comp, α.naturality, β.naturality, tensor_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F✝ G F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (fun X => F.obj X ◁ NatTrans.app β X) Y =
    (fun X => F.obj X ◁ NatTrans.app β X) X ≫ (tensorObj F G').map f
[PROOFSTEP]
simp only [← id_tensorHom]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F✝ G F' G' : C ⥤ D
α : F✝ ⟶ G
β✝ : F' ⟶ G'
F : C ⥤ D
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (𝟙 (F.obj Y) ⊗ NatTrans.app β Y) = (𝟙 (F.obj X) ⊗ NatTrans.app β X) ≫ (tensorObj F G').map f
[PROOFSTEP]
apply (tensorHom (𝟙 F) β).naturality
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (fun X => NatTrans.app α X ▷ F'.obj X) Y =
    (fun X => NatTrans.app α X ▷ F'.obj X) X ≫ (tensorObj G F').map f
[PROOFSTEP]
simp only [← tensorHom_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F'✝ G' : C ⥤ D
α : F ⟶ G
β : F'✝ ⟶ G'
F' : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (NatTrans.app α Y ⊗ 𝟙 (F'.obj Y)) =
    (NatTrans.app α X ⊗ 𝟙 (F'.obj X)) ≫ (tensorObj G F').map f
[PROOFSTEP]
apply (tensorHom α (𝟙 F')).naturality
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C ⥤ D} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) f g =
      (fun {X₁ X₂} α F => FunctorCategory.whiskerRight α F) f X₂ ≫
        (fun F x x_1 α => FunctorCategory.whiskerLeft F α) Y₁ X₂ Y₂ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) f✝ g✝ =
    (fun {X₁ X₂} α F => FunctorCategory.whiskerRight α F) f✝ X₂✝ ≫
      (fun F x x_1 α => FunctorCategory.whiskerLeft F α) Y₁✝ X₂✝ Y₂✝ g✝
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
x✝ : C
⊢ NatTrans.app ((fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) f✝ g✝) x✝ =
    NatTrans.app
      ((fun {X₁ X₂} α F => FunctorCategory.whiskerRight α F) f✝ X₂✝ ≫
        (fun F x x_1 α => FunctorCategory.whiskerLeft F α) Y₁✝ X₂✝ Y₂✝ g✝)
      x✝
[PROOFSTEP]
simp [tensorHom_def]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
⊢ (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β)
        ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G H).hom (𝟙 K) ≫
      ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F
            ((fun F G => FunctorCategory.tensorObj F G) G H) K).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) (𝟙 F)
          ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) G H K).hom =
    ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X))
          ((fun F G => FunctorCategory.tensorObj F G) F G) H K).hom ≫
      ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G
          ((fun F G => FunctorCategory.tensorObj F G) H K)).hom
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ NatTrans.app
      ((fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β)
          ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G H).hom (𝟙 K) ≫
        ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F
              ((fun F G => FunctorCategory.tensorObj F G) G H) K).hom ≫
          (fun {X₁ Y₁ X₂ Y₂} α β => FunctorCategory.tensorHom α β) (𝟙 F)
            ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) G H K).hom)
      X =
    NatTrans.app
      (((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X))
            ((fun F G => FunctorCategory.tensorObj F G) F G) H K).hom ≫
        ((fun F G H => NatIso.ofComponents fun X => α_ (F.obj X) (G.obj X) (H.obj X)) F G
            ((fun F G => FunctorCategory.tensorObj F G) H K)).hom)
      X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ ((α_ (F.obj X) (G.obj X) (H.obj X)).hom ⊗ 𝟙 (K.obj X)) ≫
      (α_ (F.obj X) (G.obj X ⊗ H.obj X) (K.obj X)).hom ≫ (𝟙 (F.obj X) ⊗ (α_ (G.obj X) (H.obj X) (K.obj X)).hom) =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom
[PROOFSTEP]
rw [pentagon]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).hom ≫ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F (G ⊗ H)).hom ≫ (α_ G H F).hom =
    (((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F G).hom ⊗ 𝟙 H) ≫
      (α_ G F H).hom ≫ (𝟙 G ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ NatTrans.app
      ((α_ F G H).hom ≫
        ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F (G ⊗ H)).hom ≫ (α_ G H F).hom)
      X =
    NatTrans.app
      ((((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F G).hom ⊗ 𝟙 H) ≫
        (α_ G F H).hom ≫ (𝟙 G ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom))
      X
[PROOFSTEP]
apply hexagon_forward
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
⊢ (α_ F G H).inv ≫ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) (F ⊗ G) H).hom ≫ (α_ H F G).inv =
    (𝟙 F ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) G H).hom) ≫
      (α_ F H G).inv ≫ (((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom ⊗ 𝟙 G)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ NatTrans.app
      ((α_ F G H).inv ≫
        ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) (F ⊗ G) H).hom ≫ (α_ H F G).inv)
      X =
    NatTrans.app
      ((𝟙 F ⊗ ((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) G H).hom) ≫
        (α_ F H G).inv ≫ (((fun F G => NatIso.ofComponents fun X => β_ (F.obj X) (G.obj X)) F H).hom ⊗ 𝟙 G))
      X
[PROOFSTEP]
apply hexagon_reverse
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
⊢ (β_ F G).hom ≫ (β_ G F).hom = 𝟙 (F ⊗ G)
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
X : C
⊢ NatTrans.app ((β_ F G).hom ≫ (β_ G F).hom) X = NatTrans.app (𝟙 (F ⊗ G)) X
[PROOFSTEP]
apply symmetry
