-- 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)
W X Y Z : C
⊢ Eq (α :=
    tensorObj ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z ⟶
      Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt)))
          (CategoryStruct.comp (Y :=
            Cone.pt (F := pair W (Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt))))
              (LimitCone.cone (ℬ W (Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt))))))
            (CategoryStruct.comp (Y :=
              tensorObj ℬ (Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt))) Z)
              (IsLimit.lift
                  (LimitCone.isLimit
                    (ℬ (Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt))) Z))
                  (BinaryFan.mk (P :=
                    Cone.pt (F := pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                      (LimitCone.cone
                        (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)))
                    (NatTrans.app
                          (Cone.π
                            (LimitCone.cone
                              (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)))
                          { as := WalkingPair.left } ≫
                        (BinaryFan.associatorOfLimitCone ℬ W X Y).hom :
                      Cone.pt (F :=
                          pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                          (LimitCone.cone
                            (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)) ⟶
                        Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt)))
                    (CategoryStruct.comp (Y := Z)
                        (NatTrans.app
                            (Cone.π
                              (LimitCone.cone
                                (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)))
                            { as := WalkingPair.right } :
                          Functor.obj.{0, v, 0, u}
                              (Functor.obj (Functor.const (Discrete WalkingPair))
                                (Cone.pt (F :=
                                  pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                                  (LimitCone.cone
                                    (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y)))
                                      Z))))
                              { as := WalkingPair.right : Discrete WalkingPair } ⟶
                            Functor.obj.{0, v, 0, u}
                              (pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                              { as := WalkingPair.right : Discrete WalkingPair })
                        (𝟙 Z) :
                      Cone.pt (F :=
                          pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                          (LimitCone.cone
                            (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)) ⟶
                        Z)) :
                Cone.pt (F := pair (Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt))) Z)
                    (BinaryFan.mk (P :=
                      Cone.pt (F :=
                        pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                        (LimitCone.cone
                          (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)))
                      (NatTrans.app
                            (Cone.π
                              (LimitCone.cone
                                (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)))
                            { as := WalkingPair.left : Discrete WalkingPair } ≫
                          (BinaryFan.associatorOfLimitCone ℬ W X Y).hom :
                        Cone.pt (F :=
                            pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                            (LimitCone.cone
                              (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)) ⟶
                          Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt)))
                      (CategoryStruct.comp (Y := Z)
                          (NatTrans.app
                              (Cone.π
                                (LimitCone.cone
                                  (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)))
                              { as := WalkingPair.right : Discrete WalkingPair } :
                            Functor.obj.{0, v, 0, u}
                                (Functor.obj (Functor.const (Discrete WalkingPair))
                                  (Cone.pt (F :=
                                    pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y)))
                                      Z)
                                    (LimitCone.cone
                                      (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y)))
                                        Z))))
                                { as := WalkingPair.right : Discrete WalkingPair } ⟶
                              Functor.obj.{0, v, 0, u}
                                (pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                                { as := WalkingPair.right : Discrete WalkingPair })
                          (𝟙 Z) :
                        Cone.pt (F :=
                            pair (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)
                            (LimitCone.cone
                              (ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z)) ⟶
                          Z)) ⟶
                  Cone.pt (F := pair (Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt))) Z)
                    (LimitCone.cone
                      (ℬ (Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt))) Z)))
              (Iso.hom (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z) ≫
                  IsLimit.lift
                    (LimitCone.isLimit
                      (ℬ W (Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt)))))
                    (BinaryFan.mk (P :=
                      Cone.pt (F :=
                        pair W (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))
                        (LimitCone.cone
                          (ℬ W (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))))
                      (CategoryStruct.comp (Y := W)
                          (NatTrans.app
                              (Cone.π
                                (LimitCone.cone
                                  (ℬ W
                                    (Cone.pt (F := pair (tensorObj ℬ X Y) Z)
                                      (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))))
                              { as := WalkingPair.left } :
                            Functor.obj.{0, v, 0, u}
                                (Functor.obj (Functor.const (Discrete WalkingPair))
                                  (Cone.pt (F :=
                                    pair W
                                      (Cone.pt (F := pair (tensorObj ℬ X Y) Z)
                                        (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))
                                    (LimitCone.cone
                                      (ℬ W
                                        (Cone.pt (F := pair (tensorObj ℬ X Y) Z)
                                          (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z)))))))
                                { as := WalkingPair.left : Discrete WalkingPair } ⟶
                              Functor.obj.{0, v, 0, u}
                                (pair W
                                  (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))
                                { as := WalkingPair.left : Discrete WalkingPair })
                          (𝟙 W) :
                        Cone.pt (F :=
                            pair W (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))
                            (LimitCone.cone
                              (ℬ W
                                (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))) ⟶
                          W)
                      (NatTrans.app
                            (Cone.π
                              (LimitCone.cone
                                (ℬ W
                                  (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))))
                            { as := WalkingPair.right } ≫
                          (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom :
                        Cone.pt (F :=
                            pair W (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))
                            (LimitCone.cone
                              (ℬ W
                                (Cone.pt (F := pair (tensorObj ℬ X Y) Z) (LimitCone.cone (ℬ (tensorObj ℬ X Y) Z))))) ⟶
                          Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt)))) :
                tensorObj ℬ (Cone.pt (F := pair W (ℬ X Y).cone.pt) (LimitCone.cone (ℬ W (ℬ X Y).cone.pt))) Z ⟶
                  tensorObj ℬ W (Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt)))))
            (NatTrans.app
              (Cone.π
                (LimitCone.cone (ℬ W (Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt))))))
              { as := WalkingPair.right }))
          (NatTrans.app (Cone.π (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt))) { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app { as := WalkingPair.left : Discrete WalkingPair } :
      tensorObj ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z ⟶
        Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y := Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt)))
          ((Iso.hom (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z) ≫
                Iso.hom (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z))) ≫
              NatTrans.app
                (Cone.π
                  (LimitCone.cone (ℬ W (Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt))))))
                { as := WalkingPair.right } :
            tensorObj ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z ⟶
              Functor.obj.{0, v, 0, u}
                (pair W (Cone.pt (F := pair X (ℬ Y Z).cone.pt) (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt))))
                { as := WalkingPair.right : Discrete WalkingPair })
          (NatTrans.app (Cone.π (LimitCone.cone (ℬ X (ℬ Y Z).cone.pt))) { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app { as := WalkingPair.left : Discrete WalkingPair } :
      tensorObj ℬ (Cone.pt (F := pair (ℬ W X).cone.pt Y) (LimitCone.cone (ℬ (ℬ W X).cone.pt Y))) Z ⟶
        Functor.obj.{0, v, 0, u} (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
simp