-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
ℬ : (X Y : C) → LimitCone.{0, 0, v, u} (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
right :
  ∀ (j : Discrete WalkingPair),
    Eq (α := tensorObj ℬ (tensorObj ℬ X₁ X₂) X₃ ⟶ Functor.obj.{0, v, 0, u} (pair Y₂ Y₃) j)
      (CategoryStruct.comp (Y := Cone.pt (F := pair Y₁ (ℬ Y₂ Y₃).cone.pt) (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt)))
            (IsLimit.lift (LimitCone.isLimit (ℬ (tensorObj ℬ Y₁ Y₂) Y₃))
                (BinaryFan.mk (P :=
                  Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃)))
                  (CategoryStruct.comp (Y := tensorObj ℬ X₁ X₂)
                      (NatTrans.app (Cone.π (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃))) { as := WalkingPair.left } :
                        Functor.obj.{0, v, 0, u}
                            (Functor.obj (Functor.const (Discrete WalkingPair))
                              (Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃))))
                            { as := WalkingPair.left : Discrete WalkingPair } ⟶
                          Functor.obj.{0, v, 0, u} (pair (tensorObj ℬ X₁ X₂) X₃)
                            { as := WalkingPair.left : Discrete WalkingPair })
                      ((ℬ Y₁ Y₂).isLimit.lift
                        (BinaryFan.mk (P := (ℬ X₁ X₂).cone.pt)
                          ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁ : (ℬ X₁ X₂).cone.pt ⟶ Y₁)
                          ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂ : (ℬ X₁ X₂).cone.pt ⟶ Y₂))) :
                    Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃)) ⟶
                      tensorObj ℬ Y₁ Y₂)
                  (NatTrans.app (Cone.π (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃))) { as := WalkingPair.right } ≫ f₃ :
                    Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃)) ⟶ Y₃)) ≫
              (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom)
            (NatTrans.app (Cone.π (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt))) { as := WalkingPair.right }) ≫
          (ℬ Y₂ Y₃).cone.π.app j :
        tensorObj ℬ (tensorObj ℬ X₁ X₂) X₃ ⟶ Functor.obj.{0, v, 0, u} (pair Y₂ Y₃) j)
      (CategoryStruct.comp (Y := Cone.pt (F := pair Y₁ (ℬ Y₂ Y₃).cone.pt) (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt)))
            ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
              IsLimit.lift (LimitCone.isLimit (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)))
                (BinaryFan.mk (P := Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt)))
                  (NatTrans.app (Cone.π (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt))) { as := WalkingPair.left } ≫ f₁ :
                    Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt)) ⟶ Y₁)
                  (CategoryStruct.comp (Y := (ℬ X₂ X₃).cone.pt)
                      (NatTrans.app (Cone.π (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt))) { as := WalkingPair.right } :
                        Functor.obj.{0, v, 0, u}
                            (Functor.obj (Functor.const (Discrete WalkingPair))
                              (Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt))))
                            { as := WalkingPair.right : Discrete WalkingPair } ⟶
                          Functor.obj.{0, v, 0, u} (pair X₁ (ℬ X₂ X₃).cone.pt)
                            { as := WalkingPair.right : Discrete WalkingPair })
                      ((ℬ Y₂ Y₃).isLimit.lift
                        (BinaryFan.mk (P := (ℬ X₂ X₃).cone.pt)
                          ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂ : (ℬ X₂ X₃).cone.pt ⟶ Y₂)
                          ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃ : (ℬ X₂ X₃).cone.pt ⟶ Y₃))) :
                    Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt)) ⟶
                      tensorObj ℬ Y₂ Y₃)))
            (NatTrans.app (Cone.π (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt))) { as := WalkingPair.right }) ≫
          (ℬ Y₂ Y₃).cone.π.app j :
        tensorObj ℬ (tensorObj ℬ X₁ X₂) X₃ ⟶ Functor.obj.{0, v, 0, u} (pair Y₂ Y₃) j)
⊢ Eq (α :=
    tensorObj ℬ (tensorObj ℬ X₁ X₂) X₃ ⟶
      Functor.obj.{0, v, 0, u} (pair Y₁ (ℬ Y₂ Y₃).cone.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := Cone.pt (F := pair Y₁ (ℬ Y₂ Y₃).cone.pt) (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt)))
        (IsLimit.lift (LimitCone.isLimit (ℬ (tensorObj ℬ Y₁ Y₂) Y₃))
            (BinaryFan.mk (P := Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃)))
              (CategoryStruct.comp (Y := tensorObj ℬ X₁ X₂)
                  (NatTrans.app (Cone.π (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃))) { as := WalkingPair.left } :
                    Functor.obj.{0, v, 0, u}
                        (Functor.obj (Functor.const (Discrete WalkingPair))
                          (Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃))))
                        { as := WalkingPair.left : Discrete WalkingPair } ⟶
                      Functor.obj.{0, v, 0, u} (pair (tensorObj ℬ X₁ X₂) X₃)
                        { as := WalkingPair.left : Discrete WalkingPair })
                  ((ℬ Y₁ Y₂).isLimit.lift
                    (BinaryFan.mk (P := (ℬ X₁ X₂).cone.pt)
                      ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁ : (ℬ X₁ X₂).cone.pt ⟶ Y₁)
                      ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂ : (ℬ X₁ X₂).cone.pt ⟶ Y₂))) :
                Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃)) ⟶
                  tensorObj ℬ Y₁ Y₂)
              (NatTrans.app (Cone.π (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃))) { as := WalkingPair.right } ≫ f₃ :
                Cone.pt (F := pair (tensorObj ℬ X₁ X₂) X₃) (LimitCone.cone (ℬ (tensorObj ℬ X₁ X₂) X₃)) ⟶ Y₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom)
        (NatTrans.app (Cone.π (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt))) { as := WalkingPair.right }) :
      tensorObj ℬ (tensorObj ℬ X₁ X₂) X₃ ⟶
        Functor.obj.{0, v, 0, u} (pair Y₁ (ℬ Y₂ Y₃).cone.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y := Cone.pt (F := pair Y₁ (ℬ Y₂ Y₃).cone.pt) (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt)))
        ((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          IsLimit.lift (LimitCone.isLimit (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)))
            (BinaryFan.mk (P := Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt)))
              (NatTrans.app (Cone.π (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt))) { as := WalkingPair.left } ≫ f₁ :
                Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt)) ⟶ Y₁)
              (CategoryStruct.comp (Y := (ℬ X₂ X₃).cone.pt)
                  (NatTrans.app (Cone.π (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt))) { as := WalkingPair.right } :
                    Functor.obj.{0, v, 0, u}
                        (Functor.obj (Functor.const (Discrete WalkingPair))
                          (Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt))))
                        { as := WalkingPair.right : Discrete WalkingPair } ⟶
                      Functor.obj.{0, v, 0, u} (pair X₁ (ℬ X₂ X₃).cone.pt)
                        { as := WalkingPair.right : Discrete WalkingPair })
                  ((ℬ Y₂ Y₃).isLimit.lift
                    (BinaryFan.mk (P := (ℬ X₂ X₃).cone.pt)
                      ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂ : (ℬ X₂ X₃).cone.pt ⟶ Y₂)
                      ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃ : (ℬ X₂ X₃).cone.pt ⟶ Y₃))) :
                Cone.pt (F := pair X₁ (ℬ X₂ X₃).cone.pt) (LimitCone.cone (ℬ X₁ (ℬ X₂ X₃).cone.pt)) ⟶
                  tensorObj ℬ Y₂ Y₃)))
        (NatTrans.app (Cone.π (LimitCone.cone (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt))) { as := WalkingPair.right }) :
      tensorObj ℬ (tensorObj ℬ X₁ X₂) X₃ ⟶
        Functor.obj.{0, v, 0, u} (pair Y₁ (ℬ Y₂ Y₃).cone.pt) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
apply (ℬ _ _).isLimit.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.LimitCone.isLimit