Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case right.left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                    ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.left } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                    ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.left }

pp: case right.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                    ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.right } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                    ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.right }

Tactic:
<;>

Goal state after:
case right.left
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                    ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.left } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                    ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.left }

case right.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ ((↑(BinaryFan.IsLimit.lift' (ℬ (tensorObj ℬ Y₁ Y₂) Y₃).isLimit
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.left } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ Y₂).isLimit ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.left } ≫ f₁)
                    ((ℬ X₁ X₂).cone.π.app { as := WalkingPair.right } ≫ f₂)))
              ((ℬ (tensorObj ℬ X₁ X₂) X₃).cone.π.app { as := WalkingPair.right } ≫ f₃)) ≫
          (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.right } =
    (((BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫
          ↑(BinaryFan.IsLimit.lift' (ℬ Y₁ (tensorObj ℬ Y₂ Y₃)).isLimit
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.left } ≫ f₁)
              ((ℬ X₁ (ℬ X₂ X₃).cone.pt).cone.π.app { as := WalkingPair.right } ≫
                ↑(BinaryFan.IsLimit.lift' (ℬ Y₂ Y₃).isLimit ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.left } ≫ f₂)
                    ((ℬ X₂ X₃).cone.π.app { as := WalkingPair.right } ≫ f₃))))) ≫
        (ℬ Y₁ (ℬ Y₂ Y₃).cone.pt).cone.π.app { as := WalkingPair.right }) ≫
      (ℬ Y₂ Y₃).cone.π.app { as := WalkingPair.right }