C : Type u
inst✝ : Category C
X Y : C
𝒯 : LimitCone (Functor.empty C)
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ∀ (j : Discrete WalkingPair),
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app j =
      (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).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₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂
apply IsLimit.hom_ext (ℬ _ _).isLimit
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₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ IsLimit.lift (ℬ Z₁ Z₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁ ≫ g₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂ ≫ g₂)) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone =
    (IsLimit.lift (ℬ Y₁ Y₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)) ≫
        IsLimit.lift (ℬ Z₁ Z₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ Y₁ Y₂).cone ≫ g₁) (BinaryFan.snd (ℬ Y₁ Y₂).cone ≫ g₂))) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).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₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right } =
    (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right }
dsimp [tensorHom]
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₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ IsLimit.lift (ℬ Z₁ Z₂).isLimit
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁ ≫ g₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂ ≫ g₂)) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone =
    (IsLimit.lift (ℬ Y₁ Y₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)) ≫
        IsLimit.lift (ℬ Z₁ Z₂).isLimit
          (BinaryFan.mk (BinaryFan.fst (ℬ Y₁ Y₂).cone ≫ g₁) (BinaryFan.snd (ℬ Y₁ Y₂).cone ≫ g₂))) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone
simp