-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X) L.X ⟶
      coequalizer (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
            P.X ◁ TensorBimod.actLeft Q L :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))
    (Iso.hom (α_ P.X Q.X T.X) ▷ L.X ≫
        (P.X ◁ Q.actRight) ▷ L.X ≫
          Iso.hom (α_ P.X Q.X L.X) ≫
            CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
              (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X) ⟶
                  tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                    (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
              (coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))
                  (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                    P.X ◁ TensorBimod.actLeft Q L) :
                tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                    (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                  coequalizer (X :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                      (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                    (Y :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                      (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                    (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                    (Iso.hom
                          (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                        P.X ◁ TensorBimod.actLeft Q L :
                      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X) L.X ⟶
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
              P.X ◁ TensorBimod.actLeft Q L :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))
    (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ T.X ▷ L.X ≫
        (Iso.hom (α_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) T.X L.X) ≫
            coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) ≫
          CategoryStruct.comp (Y :=
            coequalizer (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X) L.X)
              (P.actRight ▷ Q.X ▷ L.X) ((Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X))
            (Iso.inv
              (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X)
                (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
            (coequalizer.desc
              (Iso.hom (α_ P.X Q.X L.X) ≫
                CategoryStruct.comp (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                    (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                  (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X) ⟶
                      tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                        (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                  (coequalizer.π
                      (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))
                      (Iso.hom
                          (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                        P.X ◁ TensorBimod.actLeft Q L) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                        (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                      coequalizer (X :=
                        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                        (Y :=
                        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                        (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                        (Iso.hom
                              (α_ P.X S.X
                                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                            P.X ◁ TensorBimod.actLeft Q L :
                          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))))
              ⋯) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X) L.X ⟶
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
              P.X ◁ TensorBimod.actLeft Q L :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X) L.X ⟶
      coequalizer (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
            P.X ◁ TensorBimod.actLeft Q L :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))
    (CategoryStruct.comp (Y :=
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X)
            L.X)
          (P.actRight ▷ Q.X ▷ L.X) ((Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
            L.X)
          (Iso.hom (α_ P.X Q.X T.X) ▷ L.X ≫
            (P.X ◁ Q.actRight) ▷ L.X ≫
              coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X)
          (Iso.inv
            (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X)
              (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))))
        (coequalizer.desc
          (Iso.hom (α_ P.X Q.X L.X) ≫
            CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
              (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X) ⟶
                  tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                    (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
              (coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))
                  (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                    P.X ◁ TensorBimod.actLeft Q L) :
                tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                    (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                  coequalizer (X :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                      (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                    (Y :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                      (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                    (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                    (Iso.hom
                          (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                        P.X ◁ TensorBimod.actLeft Q L :
                      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))))
          ⋯) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X) L.X ⟶
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
              P.X ◁ TensorBimod.actLeft Q L :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))
    (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ T.X ▷ L.X ≫
        (Iso.hom (α_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) T.X L.X) ≫
            coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) ≫
          CategoryStruct.comp (Y :=
            coequalizer (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X) L.X)
              (P.actRight ▷ Q.X ▷ L.X) ((Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X))
            (Iso.inv
              (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X)
                (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
            (coequalizer.desc
              (Iso.hom (α_ P.X Q.X L.X) ≫
                CategoryStruct.comp (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                    (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                  (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X) ⟶
                      tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                        (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                  (coequalizer.π
                      (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))
                      (Iso.hom
                          (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                        P.X ◁ TensorBimod.actLeft Q L) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                        (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                      coequalizer (X :=
                        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                        (Y :=
                        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                        (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
                          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
                        (Iso.hom
                              (α_ P.X S.X
                                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
                            P.X ◁ TensorBimod.actLeft Q L :
                          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
                            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))))
              ⋯) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X) L.X ⟶
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ≫
              P.X ◁ TensorBimod.actLeft Q L :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) P.X
                (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))

Tactic:
slice_lhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]

Premises used: π_tensor_id_preserves_coequalizer_inv_desc