-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
theorem pentagon (W X Y Z : C) :
    tensorHom ℬ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom (𝟙 Z) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          tensorHom ℬ (𝟙 W) (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom =
      (BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
        (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom

Proof state:
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (((ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit.lift
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit.lift
              (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right } =
    (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }

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

Result:
case mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    ((((ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit.lift
                (BinaryFan.mk
                  (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫
                    (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                  (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
              (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
                (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit.lift
                  (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                    (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                      (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
          (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app j =
      ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
              (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
          (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ Y Z).cone.π.app j

Proof state:
case mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (((ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit.lift
            (BinaryFan.mk
              (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit.lift
              (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.left } =
    (((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.left }

Tactic:
simp

Result:
no goals

Proof state:
case mk.right.mk.right.mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ((((ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit.lift
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit.lift
                (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                  (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.right } =
    ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.right }

Tactic:
simp

Result:
no goals

Proof state:
case mk.right.mk.right.mk.left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ((((ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit.lift
              (BinaryFan.mk
                (BinaryFan.fst (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
                (BinaryFan.snd (ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone ≫ 𝟙 Z)) ≫
            (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
              (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit.lift
                (BinaryFan.mk (BinaryFan.fst (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫ 𝟙 W)
                  (BinaryFan.snd (ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone ≫
                    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.left } =
    ((((BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom ≫
            (BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom) ≫
          (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
        (ℬ X (ℬ Y Z).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y Z).cone.π.app { as := WalkingPair.left }

Tactic:
simp

Result:
no goals