[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ tensorHom ℬ f g ≫ (BinaryFan.braiding (ℬ Y Y').isLimit (ℬ Y' Y).isLimit).hom =
    (BinaryFan.braiding (ℬ X X').isLimit (ℬ X' X).isLimit).hom ≫ tensorHom ℬ g f
[PROOFSTEP]
dsimp [tensorHom, Limits.BinaryFan.braiding]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ IsLimit.lift (ℬ Y Y').isLimit (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
      (IsLimit.conePointUniqueUpToIso (ℬ Y Y').isLimit (IsLimit.swapBinaryFan (ℬ Y' Y).isLimit)).hom =
    (IsLimit.conePointUniqueUpToIso (ℬ X X').isLimit (IsLimit.swapBinaryFan (ℬ X' X).isLimit)).hom ≫
      IsLimit.lift (ℬ Y' Y).isLimit (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))
[PROOFSTEP]
apply (ℬ _ _).isLimit.hom_ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ ∀ (j : Discrete WalkingPair),
    (IsLimit.lift (ℬ Y Y').isLimit (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
          (IsLimit.conePointUniqueUpToIso (ℬ Y Y').isLimit (IsLimit.swapBinaryFan (ℬ Y' Y).isLimit)).hom) ≫
        NatTrans.app (ℬ Y' Y).cone.π j =
      ((IsLimit.conePointUniqueUpToIso (ℬ X X').isLimit (IsLimit.swapBinaryFan (ℬ X' X).isLimit)).hom ≫
          IsLimit.lift (ℬ Y' Y).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
        NatTrans.app (ℬ Y' Y).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (IsLimit.lift (ℬ Y Y').isLimit (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
        (IsLimit.conePointUniqueUpToIso (ℬ Y Y').isLimit (IsLimit.swapBinaryFan (ℬ Y' Y).isLimit)).hom) ≫
      NatTrans.app (ℬ Y' Y).cone.π { as := WalkingPair.left } =
    ((IsLimit.conePointUniqueUpToIso (ℬ X X').isLimit (IsLimit.swapBinaryFan (ℬ X' X).isLimit)).hom ≫
        IsLimit.lift (ℬ Y' Y).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
      NatTrans.app (ℬ Y' Y).cone.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (IsLimit.lift (ℬ Y Y').isLimit (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
        IsLimit.lift (ℬ Y' Y).isLimit (BinaryFan.swap (ℬ Y Y').cone)) ≫
      BinaryFan.fst (ℬ Y' Y).cone =
    (IsLimit.lift (ℬ X' X).isLimit (BinaryFan.swap (ℬ X X').cone) ≫
        IsLimit.lift (ℬ Y' Y).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
      BinaryFan.fst (ℬ Y' Y).cone
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (IsLimit.lift (ℬ Y Y').isLimit (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
        (IsLimit.conePointUniqueUpToIso (ℬ Y Y').isLimit (IsLimit.swapBinaryFan (ℬ Y' Y).isLimit)).hom) ≫
      NatTrans.app (ℬ Y' Y).cone.π { as := WalkingPair.right } =
    ((IsLimit.conePointUniqueUpToIso (ℬ X X').isLimit (IsLimit.swapBinaryFan (ℬ X' X).isLimit)).hom ≫
        IsLimit.lift (ℬ Y' Y).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
      NatTrans.app (ℬ Y' Y).cone.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (IsLimit.lift (ℬ Y Y').isLimit (BinaryFan.mk (BinaryFan.fst (ℬ X X').cone ≫ f) (BinaryFan.snd (ℬ X X').cone ≫ g)) ≫
        IsLimit.lift (ℬ Y' Y).isLimit (BinaryFan.swap (ℬ Y Y').cone)) ≫
      BinaryFan.snd (ℬ Y' Y).cone =
    (IsLimit.lift (ℬ X' X).isLimit (BinaryFan.swap (ℬ X X').cone) ≫
        IsLimit.lift (ℬ Y' Y).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X' X).cone ≫ g) (BinaryFan.snd (ℬ X' X).cone ≫ f))) ≫
      BinaryFan.snd (ℬ Y' Y).cone
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
      (BinaryFan.braiding (ℬ X (tensorObj ℬ Y Z)).isLimit (ℬ (tensorObj ℬ Y Z) X).isLimit).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom =
    tensorHom ℬ (BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (𝟙 Z) ≫
      (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
        tensorHom ℬ (𝟙 Y) (BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom
[PROOFSTEP]
dsimp [tensorHom, Limits.BinaryFan.braiding]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
      (IsLimit.conePointUniqueUpToIso (ℬ X (tensorObj ℬ Y Z)).isLimit
            (IsLimit.swapBinaryFan (ℬ (tensorObj ℬ Y Z) X).isLimit)).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom =
    IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
        (BinaryFan.mk
          (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫
            (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom)
          (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
      (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
        IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
            (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
              (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom))
[PROOFSTEP]
apply (ℬ _ _).isLimit.hom_ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    ((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
          (IsLimit.conePointUniqueUpToIso (ℬ X (tensorObj ℬ Y Z)).isLimit
                (IsLimit.swapBinaryFan (ℬ (tensorObj ℬ Y Z) X).isLimit)).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
        NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π j =
      (IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom)
              (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
            IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
                (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom))) ≫
        NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
        (IsLimit.conePointUniqueUpToIso (ℬ X (tensorObj ℬ Y Z)).isLimit
              (IsLimit.swapBinaryFan (ℬ (tensorObj ℬ Y Z) X).isLimit)).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
      NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.left } =
    (IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫
              (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom)
            (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
          IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
              (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom))) ≫
      NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
        IsLimit.lift (ℬ (tensorObj ℬ Y Z) X).isLimit (BinaryFan.swap (ℬ X (tensorObj ℬ Y Z)).cone) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
      BinaryFan.fst (ℬ Y (ℬ Z X).cone.pt).cone =
    (IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫ IsLimit.lift (ℬ Y X).isLimit (BinaryFan.swap (ℬ X Y).cone))
            (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
          IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
              (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                IsLimit.lift (ℬ Z X).isLimit (BinaryFan.swap (ℬ X Z).cone)))) ≫
      BinaryFan.fst (ℬ Y (ℬ Z X).cone.pt).cone
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
        (IsLimit.conePointUniqueUpToIso (ℬ X (tensorObj ℬ Y Z)).isLimit
              (IsLimit.swapBinaryFan (ℬ (tensorObj ℬ Y Z) X).isLimit)).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
      NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right } =
    (IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫
              (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom)
            (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
          IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
              (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom))) ≫
      NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right }
[PROOFSTEP]
apply (ℬ _ _).isLimit.hom_ext
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
            (IsLimit.conePointUniqueUpToIso (ℬ X (tensorObj ℬ Y Z)).isLimit
                  (IsLimit.swapBinaryFan (ℬ (tensorObj ℬ Y Z) X).isLimit)).hom ≫
              (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
          NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ Z X).cone.π j =
      ((IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom)
                (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
              IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
                (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
                  (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                    (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom))) ≫
          NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right }) ≫
        NatTrans.app (ℬ Z X).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
          (IsLimit.conePointUniqueUpToIso (ℬ X (tensorObj ℬ Y Z)).isLimit
                (IsLimit.swapBinaryFan (ℬ (tensorObj ℬ Y Z) X).isLimit)).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
        NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.left } =
    ((IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom)
              (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
            IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
                (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom))) ≫
        NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
          IsLimit.lift (ℬ (tensorObj ℬ Y Z) X).isLimit (BinaryFan.swap (ℬ X (tensorObj ℬ Y Z)).cone) ≫
            (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
        BinaryFan.snd (ℬ Y (ℬ Z X).cone.pt).cone) ≫
      BinaryFan.fst (ℬ Z X).cone =
    ((IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫ IsLimit.lift (ℬ Y X).isLimit (BinaryFan.swap (ℬ X Y).cone))
              (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
            IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
                (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                  IsLimit.lift (ℬ Z X).isLimit (BinaryFan.swap (ℬ X Z).cone)))) ≫
        BinaryFan.snd (ℬ Y (ℬ Z X).cone.pt).cone) ≫
      BinaryFan.fst (ℬ Z X).cone
[PROOFSTEP]
simp
[GOAL]
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
          (IsLimit.conePointUniqueUpToIso (ℬ X (tensorObj ℬ Y Z)).isLimit
                (IsLimit.swapBinaryFan (ℬ (tensorObj ℬ Y Z) X).isLimit)).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
        NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.right } =
    ((IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom)
              (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
            IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
                (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom))) ≫
        NatTrans.app (ℬ Y (ℬ Z X).cone.pt).cone.π { as := WalkingPair.right }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (((BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
          IsLimit.lift (ℬ (tensorObj ℬ Y Z) X).isLimit (BinaryFan.swap (ℬ X (tensorObj ℬ Y Z)).cone) ≫
            (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) ≫
        BinaryFan.snd (ℬ Y (ℬ Z X).cone.pt).cone) ≫
      BinaryFan.snd (ℬ Z X).cone =
    ((IsLimit.lift (ℬ (ℬ Y X).cone.pt Z).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Y).cone.pt Z).cone ≫ IsLimit.lift (ℬ Y X).isLimit (BinaryFan.swap (ℬ X Y).cone))
              (BinaryFan.snd (ℬ (ℬ X Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
            IsLimit.lift (ℬ Y (ℬ Z X).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ Y (ℬ X Z).cone.pt).cone ≫ 𝟙 Y)
                (BinaryFan.snd (ℬ Y (ℬ X Z).cone.pt).cone ≫
                  IsLimit.lift (ℬ Z X).isLimit (BinaryFan.swap (ℬ X Z).cone)))) ≫
        BinaryFan.snd (ℬ Y (ℬ Z X).cone.pt).cone) ≫
      BinaryFan.snd (ℬ Z X).cone
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
      (BinaryFan.braiding (ℬ (tensorObj ℬ X Y) Z).isLimit (ℬ Z (tensorObj ℬ X Y)).isLimit).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv =
    tensorHom ℬ (𝟙 X) (BinaryFan.braiding (ℬ Y Z).isLimit (ℬ Z Y).isLimit).hom ≫
      (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
        tensorHom ℬ (BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom (𝟙 Y)
[PROOFSTEP]
dsimp [tensorHom, Limits.BinaryFan.braiding]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
      (IsLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ X Y) Z).isLimit
            (IsLimit.swapBinaryFan (ℬ Z (tensorObj ℬ X Y)).isLimit)).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv =
    IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
          (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫
            (IsLimit.conePointUniqueUpToIso (ℬ Y Z).isLimit (IsLimit.swapBinaryFan (ℬ Z Y).isLimit)).hom)) ≫
      (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
        IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
          (BinaryFan.mk
            (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫
              (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom)
            (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))
[PROOFSTEP]
apply (ℬ _ _).isLimit.hom_ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    ((BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
          (IsLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ X Y) Z).isLimit
                (IsLimit.swapBinaryFan (ℬ Z (tensorObj ℬ X Y)).isLimit)).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) ≫
        NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π j =
      (IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
              (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ Y Z).isLimit (IsLimit.swapBinaryFan (ℬ Z Y).isLimit)).hom)) ≫
          (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
            IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom)
                (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
        NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
        (IsLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ X Y) Z).isLimit
              (IsLimit.swapBinaryFan (ℬ Z (tensorObj ℬ X Y)).isLimit)).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) ≫
      NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left } =
    (IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
            (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫
              (IsLimit.conePointUniqueUpToIso (ℬ Y Z).isLimit (IsLimit.swapBinaryFan (ℬ Z Y).isLimit)).hom)) ≫
        (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
          IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom)
              (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
      NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left }
[PROOFSTEP]
apply (ℬ _ _).isLimit.hom_ext
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (((BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
            (IsLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ X Y) Z).isLimit
                  (IsLimit.swapBinaryFan (ℬ Z (tensorObj ℬ X Y)).isLimit)).hom ≫
              (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) ≫
          NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left }) ≫
        NatTrans.app (ℬ Z X).cone.π j =
      ((IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
              (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
                (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ Y Z).isLimit (IsLimit.swapBinaryFan (ℬ Z Y).isLimit)).hom)) ≫
            (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
              IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
                (BinaryFan.mk
                  (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫
                    (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom)
                  (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
          NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left }) ≫
        NatTrans.app (ℬ Z X).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (((BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
          (IsLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ X Y) Z).isLimit
                (IsLimit.swapBinaryFan (ℬ Z (tensorObj ℬ X Y)).isLimit)).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) ≫
        NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.left } =
    ((IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
              (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ Y Z).isLimit (IsLimit.swapBinaryFan (ℬ Z Y).isLimit)).hom)) ≫
          (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
            IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom)
                (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
        NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp [BinaryFan.associatorOfLimitCone, BinaryFan.associator, Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.left.mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ((IsLimit.lift (ℬ (ℬ X Y).cone.pt Z).isLimit (BinaryFan.assocInv (ℬ X Y).isLimit (ℬ X (ℬ Y Z).cone.pt).cone) ≫
          IsLimit.lift (ℬ Z (tensorObj ℬ X Y)).isLimit (BinaryFan.swap (ℬ (tensorObj ℬ X Y) Z).cone) ≫
            IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
              (BinaryFan.assocInv (ℬ Z X).isLimit (ℬ Z (ℬ X Y).cone.pt).cone)) ≫
        BinaryFan.fst (ℬ (ℬ Z X).cone.pt Y).cone) ≫
      BinaryFan.fst (ℬ Z X).cone =
    ((IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
              (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫ IsLimit.lift (ℬ Z Y).isLimit (BinaryFan.swap (ℬ Y Z).cone))) ≫
          IsLimit.lift (ℬ (ℬ X Z).cone.pt Y).isLimit (BinaryFan.assocInv (ℬ X Z).isLimit (ℬ X (ℬ Z Y).cone.pt).cone) ≫
            IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫ IsLimit.lift (ℬ Z X).isLimit (BinaryFan.swap (ℬ X Z).cone))
                (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
        BinaryFan.fst (ℬ (ℬ Z X).cone.pt Y).cone) ≫
      BinaryFan.fst (ℬ Z X).cone
[PROOFSTEP]
simp
[GOAL]
case mk.left.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (((BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
          (IsLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ X Y) Z).isLimit
                (IsLimit.swapBinaryFan (ℬ Z (tensorObj ℬ X Y)).isLimit)).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) ≫
        NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.right } =
    ((IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
              (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ Y Z).isLimit (IsLimit.swapBinaryFan (ℬ Z Y).isLimit)).hom)) ≫
          (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
            IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫
                  (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom)
                (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
        NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.left }) ≫
      NatTrans.app (ℬ Z X).cone.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp [BinaryFan.associatorOfLimitCone, BinaryFan.associator, Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.left.mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ((IsLimit.lift (ℬ (ℬ X Y).cone.pt Z).isLimit (BinaryFan.assocInv (ℬ X Y).isLimit (ℬ X (ℬ Y Z).cone.pt).cone) ≫
          IsLimit.lift (ℬ Z (tensorObj ℬ X Y)).isLimit (BinaryFan.swap (ℬ (tensorObj ℬ X Y) Z).cone) ≫
            IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
              (BinaryFan.assocInv (ℬ Z X).isLimit (ℬ Z (ℬ X Y).cone.pt).cone)) ≫
        BinaryFan.fst (ℬ (ℬ Z X).cone.pt Y).cone) ≫
      BinaryFan.snd (ℬ Z X).cone =
    ((IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
            (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
              (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫ IsLimit.lift (ℬ Z Y).isLimit (BinaryFan.swap (ℬ Y Z).cone))) ≫
          IsLimit.lift (ℬ (ℬ X Z).cone.pt Y).isLimit (BinaryFan.assocInv (ℬ X Z).isLimit (ℬ X (ℬ Z Y).cone.pt).cone) ≫
            IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫ IsLimit.lift (ℬ Z X).isLimit (BinaryFan.swap (ℬ X Z).cone))
                (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
        BinaryFan.fst (ℬ (ℬ Z X).cone.pt Y).cone) ≫
      BinaryFan.snd (ℬ Z X).cone
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ ((BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫
        (IsLimit.conePointUniqueUpToIso (ℬ (tensorObj ℬ X Y) Z).isLimit
              (IsLimit.swapBinaryFan (ℬ Z (tensorObj ℬ X Y)).isLimit)).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) ≫
      NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.right } =
    (IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
            (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫
              (IsLimit.conePointUniqueUpToIso (ℬ Y Z).isLimit (IsLimit.swapBinaryFan (ℬ Z Y).isLimit)).hom)) ≫
        (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫
          IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫
                (IsLimit.conePointUniqueUpToIso (ℬ X Z).isLimit (IsLimit.swapBinaryFan (ℬ Z X).isLimit)).hom)
              (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
      NatTrans.app (ℬ (ℬ Z X).cone.pt Y).cone.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp [BinaryFan.associatorOfLimitCone, BinaryFan.associator, Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y Z : C
⊢ (IsLimit.lift (ℬ (ℬ X Y).cone.pt Z).isLimit (BinaryFan.assocInv (ℬ X Y).isLimit (ℬ X (ℬ Y Z).cone.pt).cone) ≫
        IsLimit.lift (ℬ Z (tensorObj ℬ X Y)).isLimit (BinaryFan.swap (ℬ (tensorObj ℬ X Y) Z).cone) ≫
          IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit (BinaryFan.assocInv (ℬ Z X).isLimit (ℬ Z (ℬ X Y).cone.pt).cone)) ≫
      BinaryFan.snd (ℬ (ℬ Z X).cone.pt Y).cone =
    (IsLimit.lift (ℬ X (ℬ Z Y).cone.pt).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X)
            (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫ IsLimit.lift (ℬ Z Y).isLimit (BinaryFan.swap (ℬ Y Z).cone))) ≫
        IsLimit.lift (ℬ (ℬ X Z).cone.pt Y).isLimit (BinaryFan.assocInv (ℬ X Z).isLimit (ℬ X (ℬ Z Y).cone.pt).cone) ≫
          IsLimit.lift (ℬ (ℬ Z X).cone.pt Y).isLimit
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫ IsLimit.lift (ℬ Z X).isLimit (BinaryFan.swap (ℬ X Z).cone))
              (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫
      BinaryFan.snd (ℬ (ℬ Z X).cone.pt Y).cone
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom ≫ (BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom =
    𝟙 (tensorObj ℬ X Y)
[PROOFSTEP]
dsimp [tensorHom, Limits.BinaryFan.braiding]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
      (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom =
    𝟙 (tensorObj ℬ X Y)
[PROOFSTEP]
apply (ℬ _ _).isLimit.hom_ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ∀ (j : Discrete WalkingPair),
    ((IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
          (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom) ≫
        NatTrans.app (ℬ X Y).cone.π j =
      𝟙 (tensorObj ℬ X Y) ≫ NatTrans.app (ℬ X Y).cone.π j
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
        (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom) ≫
      NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.left } =
    𝟙 (tensorObj ℬ X Y) ≫ NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.left }
[PROOFSTEP]
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (IsLimit.lift (ℬ Y X).isLimit (BinaryFan.swap (ℬ X Y).cone) ≫
        IsLimit.lift (ℬ X Y).isLimit (BinaryFan.swap (ℬ Y X).cone)) ≫
      BinaryFan.fst (ℬ X Y).cone =
    𝟙 (tensorObj ℬ X Y) ≫ BinaryFan.fst (ℬ X Y).cone
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ ((IsLimit.conePointUniqueUpToIso (ℬ X Y).isLimit (IsLimit.swapBinaryFan (ℬ Y X).isLimit)).hom ≫
        (IsLimit.conePointUniqueUpToIso (ℬ Y X).isLimit (IsLimit.swapBinaryFan (ℬ X Y).isLimit)).hom) ≫
      NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.right } =
    𝟙 (tensorObj ℬ X Y) ≫ NatTrans.app (ℬ X Y).cone.π { as := WalkingPair.right }
[PROOFSTEP]
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
[GOAL]
case mk.right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X Y : C
⊢ (IsLimit.lift (ℬ Y X).isLimit (BinaryFan.swap (ℬ X Y).cone) ≫
        IsLimit.lift (ℬ X Y).isLimit (BinaryFan.swap (ℬ Y X).cone)) ≫
      BinaryFan.snd (ℬ X Y).cone =
    𝟙 (tensorObj ℬ X Y) ≫ BinaryFan.snd (ℬ X Y).cone
[PROOFSTEP]
simp


[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
⊢ ∀ {W X Y Z : D} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
intros W X Y Z f r g
[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
f : W ⟶ X
r : R
g : Y ⟶ Z
⊢ f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
f : W ⟶ X
r : R
g : Y ⟶ Z
⊢ F.map (f ⊗ r • g) = F.map (r • (f ⊗ g))
[PROOFSTEP]
simp only [F.toFunctor.map_smul r (f ⊗ g), F.toFunctor.map_smul r g, F.map_tensor, MonoidalLinear.tensor_smul,
  Linear.smul_comp, Linear.comp_smul]
[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
⊢ ∀ {W X Y Z : D} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
intros W X Y Z r f g
[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
r : R
f : W ⟶ X
g : Y ⟶ Z
⊢ r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
r : R
f : W ⟶ X
g : Y ⟶ Z
⊢ F.map (r • f ⊗ g) = F.map (r • (f ⊗ g))
[PROOFSTEP]
simp only [F.toFunctor.map_smul r (f ⊗ g), F.toFunctor.map_smul r f, F.map_tensor, MonoidalLinear.smul_tensor,
  Linear.smul_comp, Linear.comp_smul]