-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a :
  (M.X ◁ Iso.hom (α_ N.X P.X Q.X) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) M.X
          (tensorObj.{v₁, u₁} (𝒞 := inst) N.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))))
        (M.X ◁ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) M.X
              (tensorObj.{v₁, u₁} (𝒞 := inst) N.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M.X
              (tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))))
        (M.X ◁
            coequalizer.π (N.actRight ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))
              (Iso.hom (α_ N.X X.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))) ≫
                N.X ◁ TensorBimod.actLeft P Q) :
          tensorObj.{v₁, u₁} (𝒞 := inst) M.X
              (tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M.X
              (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft))) :
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X P.X) Q.X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X
        (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
          (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft)))
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X
        (tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft))
          Q.X))
      (M.X ◁ coequalizer.π (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft) ▷ Q.X)
      (M.X ◁
        CategoryStruct.comp (Y :=
          coequalizer (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X X.X) P.X)
              Q.X)
            (N.actRight ▷ P.X ▷ Q.X) ((Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft) ▷ Q.X))
          (Iso.inv
            (PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X)
              (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft)))
          (coequalizer.desc
            (Iso.hom (α_ N.X P.X Q.X) ≫
              CategoryStruct.comp (Y :=
                tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                  (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)))
                (N.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft) :
                  tensorObj.{v₁, u₁} (𝒞 := inst) N.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
                    tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                      (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)))
                (coequalizer.π
                    (N.actRight ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))
                    (Iso.hom
                        (α_ N.X X.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))) ≫
                      N.X ◁ TensorBimod.actLeft P Q) :
                  tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                      (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)) ⟶
                    coequalizer (X :=
                      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X X.X)
                        (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)))
                      (Y :=
                      tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                        (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)))
                      (N.actRight ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft) :
                        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X X.X)
                            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)) ⟶
                          tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)))
                      (Iso.hom
                            (α_ N.X X.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft))) ≫
                          N.X ◁ TensorBimod.actLeft P Q :
                        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X X.X)
                            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)) ⟶
                          tensorObj.{v₁, u₁} (𝒞 := inst) N.X
                            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)))))
            ⋯)) :
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X P.X) Q.X) ⟶
      (parallelPair (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X W.X)
              (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft)))
            (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) M.X
              (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft)))
            (M.actRight ▷
                coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                  (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft) :
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X W.X)
                  (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                    (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft)) ⟶
                tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                  (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                    (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft)))
            (Iso.hom
                  (α_ M.X W.X
                    (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                      (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft))) ≫
                M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q) :
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X W.X)
                  (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                    (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft)) ⟶
                tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                  (coequalizer (N.actRight ▷ (P.tensorBimod Q).X)
                    (Iso.hom (α_ N.X X.X (P.tensorBimod Q).X) ≫ N.X ◁ (P.tensorBimod Q).actLeft)))).obj
        WalkingParallelPair.one)

Tactic:
rw [← whiskerLeft_comp, π_tensor_id_preserves_coequalizer_inv_desc,
      whiskerLeft_comp, whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, π_tensor_id_preserves_coequalizer_inv_desc