-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ 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)))) =
    Iso.hom (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z) ≫
      Iso.hom (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z))
have apply : ∀ (j : Discrete WalkingPair),
  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))))))
        j) =
    (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)))))) j
Tactic: apply (ℬ _ _).isLimit.hom_ext