<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>((((PreservesCoequalizer.iso (tensorRight P.X) (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X P.X).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)) ⋯) ▷ Q.X ≫ (PreservesCoequalizer.iso (tensorRight Q.X) (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)).inv) ≫ coequalizer.desc ((α_ M.X (TensorBimod.X N P) Q.X).hom ≫ M.X ◁ coequalizer.π (TensorBimod.actRight N P ▷ Q.X) ((α_ (TensorBimod.X N P) Y.X Q.X).hom ≫ TensorBimod.X N P ◁ Q.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)) ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) (M.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) ⋯ ⋯) = coequalizer.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) X.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ▷ Q.X ≫ ((PreservesCoequalizer.iso (tensorRight Q.X) (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) X.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ (TensorBimod.X M N) P.X Q.X).hom ≫ TensorBimod.X M N ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (TensorBimod.actRight M N ▷ TensorBimod.X P Q) ((α_ (TensorBimod.X M N) X.X (TensorBimod.X P Q)).hom ≫ TensorBimod.X M N ◁ TensorBimod.actLeft P Q)) ⋯) ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight (TensorBimod.X P Q)) (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X (TensorBimod.X P Q)).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))) ⋯) ⋯