C : Type u
inst✝ : Category C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ IsLimit.lift (ℬ X₂ 𝒯.cone.pt).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f) (BinaryFan.snd (ℬ X₁ 𝒯.cone.pt).cone ≫ 𝟙 𝒯.cone.pt)) ≫
      BinaryFan.fst (ℬ X₂ 𝒯.cone.pt).cone =
    BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f
C : Type u
inst✝ : Category C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ f (𝟙 𝒯.cone.pt) ≫ (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom =
    (BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom ≫ f
dsimp [tensorHom]
no goals
C : Type u
inst✝ : Category C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ IsLimit.lift (ℬ X₂ 𝒯.cone.pt).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f) (BinaryFan.snd (ℬ X₁ 𝒯.cone.pt).cone ≫ 𝟙 𝒯.cone.pt)) ≫
      BinaryFan.fst (ℬ X₂ 𝒯.cone.pt).cone =
    BinaryFan.fst (ℬ X₁ 𝒯.cone.pt).cone ≫ f
simp