-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
theorem hexagon_forward (X Y Z : C) :
    (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom ≫
        (Limits.BinaryFan.braiding (ℬ X (tensorObj ℬ Y Z)).isLimit
              (ℬ (tensorObj ℬ Y Z) X).isLimit).hom ≫
          (BinaryFan.associatorOfLimitCone ℬ Y Z X).hom =
      tensorHom ℬ (Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (𝟙 Z) ≫
        (BinaryFan.associatorOfLimitCone ℬ Y X Z).hom ≫
          tensorHom ℬ (𝟙 Y) (Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom

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

Tactic:
rintro ⟨⟨⟩⟩

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

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