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