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 (ℬ 𝒯.cone.pt X₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ 𝒯.cone.pt X₁).cone ≫ 𝟙 𝒯.cone.pt) (BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f)) ≫
      BinaryFan.snd (ℬ 𝒯.cone.pt X₂).cone =
    BinaryFan.snd (ℬ 𝒯.cone.pt 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₂ : C
f : X₁ ⟶ X₂
⊢ tensorHom ℬ (𝟙 𝒯.cone.pt) f ≫ (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom =
    (BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).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 (ℬ 𝒯.cone.pt X₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ 𝒯.cone.pt X₁).cone ≫ 𝟙 𝒯.cone.pt) (BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f)) ≫
      BinaryFan.snd (ℬ 𝒯.cone.pt X₂).cone =
    BinaryFan.snd (ℬ 𝒯.cone.pt X₁).cone ≫ f
simp