Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ coequalizer.π (TensorBimod.actRight M N ▷ P.X)
        ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫
      colimMap
        (parallelPairHom (TensorBimod.actRight M N ▷ P.X)
          ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft)
          (colimMap
                (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M.actRight ▷ N'.X)
                  ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ((M.X ⊗ X.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
              Y.X ▷
            P.X)
          (colimMap
              (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M.actRight ▷ N'.X)
                ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ((M.X ⊗ X.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
            P.X)
          ⋯ ⋯) =
    coequalizer.π (TensorBimod.actRight M N ▷ P.X)
        ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫
      AssociatorBimod.hom M N P ≫
        colimMap
            (parallelPairHom (M.actRight ▷ TensorBimod.X N P)
              ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ TensorBimod.X N' P)
              ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P)
              ((M.X ⊗ X.X) ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              (M.X ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              ⋯ ⋯) ≫
          AssociatorBimod.inv M N' P

Tactic:
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ colimMap
          (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M.actRight ▷ N'.X)
            ((α_ M.X X.X N'.X).hom ≫ M.X ◁ N'.actLeft) ((M.X ⊗ X.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷
        P.X ≫
      colimit.ι
        (parallelPair (TensorBimod.actRight M N' ▷ P.X)
          ((α_ (TensorBimod.X M N') Y.X P.X).hom ≫ TensorBimod.X M N' ◁ P.actLeft))
        WalkingParallelPair.one =
    coequalizer.π (TensorBimod.actRight M N ▷ P.X)
        ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫
      AssociatorBimod.hom M N P ≫
        colimMap
            (parallelPairHom (M.actRight ▷ TensorBimod.X N P)
              ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ TensorBimod.X N' P)
              ((α_ M.X X.X (TensorBimod.X N' P)).hom ≫ M.X ◁ TensorBimod.actLeft N' P)
              ((M.X ⊗ X.X) ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              (M.X ◁
                colimMap
                  (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N'.actRight ▷ P.X)
                    ((α_ N'.X Y.X P.X).hom ≫ N'.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
              ⋯ ⋯) ≫
          AssociatorBimod.inv M N' P