Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ ∀ (j : Discrete WalkingPair),
    (↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
                (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
              ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
          (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
            ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
                ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                  (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
        (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).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 j

Tactic:
rintro ⟨_ | _⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
              (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
      (ℬ W (ℬ X (ℬ Y Z).cone.pt).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.left }

case right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
W X Y Z : C
⊢ (↑(BinaryFan.IsLimit.lift' (ℬ (ℬ W (ℬ X Y).cone.pt).cone.pt Z).isLimit
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.left } ≫
              (BinaryFan.associatorOfLimitCone ℬ W X Y).hom)
            ((ℬ (ℬ (ℬ W X).cone.pt Y).cone.pt Z).cone.π.app { as := WalkingPair.right } ≫ 𝟙 Z)) ≫
        (BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ W (ℬ X (ℬ Y Z).cone.pt).cone.pt).isLimit
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.left } ≫ 𝟙 W)
              ((ℬ W (ℬ (tensorObj ℬ X Y) Z).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                (BinaryFan.associatorOfLimitCone ℬ X Y Z).hom))) ≫
      (ℬ W (ℬ X (ℬ Y Z).cone.pt).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 }