C : Type u
inst✝ : Category 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))
C : Type u
inst✝ : Category 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
dsimp [tensorHom, Limits.BinaryFan.braiding]
C : Type u
inst✝ : Category 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) ≫
        (ℬ Y (ℬ Z X).cone.pt).cone.π.app 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))) ≫
        (ℬ Y (ℬ Z X).cone.pt).cone.π.app j
C : Type u
inst✝ : Category 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))
apply (ℬ _ _).isLimit.hom_ext
case mk.left
C : Type u
inst✝ : Category 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) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { 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))) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.left }

case mk.right
C : Type u
inst✝ : Category 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) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { 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))) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.right }
C : Type u
inst✝ : Category 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) ≫
        (ℬ Y (ℬ Z X).cone.pt).cone.π.app 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))) ≫
        (ℬ Y (ℬ Z X).cone.pt).cone.π.app j
rintro ⟨⟨⟩⟩
case mk.left
C : Type u
inst✝ : Category 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
case mk.left
C : Type u
inst✝ : Category 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) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { 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))) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.left }
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
no goals
case mk.left
C : Type u
inst✝ : Category 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
simp
case mk.right
C : Type u
inst✝ : Category 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) ≫
          (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Z X).cone.π.app 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))) ≫
          (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Z X).cone.π.app j
case mk.right
C : Type u
inst✝ : Category 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) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { 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))) ≫
      (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.right }
apply (ℬ _ _).isLimit.hom_ext
case mk.right.mk.right
C : Type u
inst✝ : Category 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
case mk.right.mk.right
C : Type u
inst✝ : Category 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) ≫
        (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Z X).cone.π.app { 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))) ≫
        (ℬ Y (ℬ Z X).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Z X).cone.π.app { as := WalkingPair.right }
dsimp [Limits.IsLimit.conePointUniqueUpToIso]
no goals
case mk.right.mk.right
C : Type u
inst✝ : Category 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
simp