Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case right.right.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.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 }

pp: case right.right.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 }) ≫
        (ℬ 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:
<;>

Goal state after:
case right.right.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.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 }

case right.right.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 }) ≫
        (ℬ 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 }