-- 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)
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) L.X) U.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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) L.X U.X) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ◁ L.actRight ≫
          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) L.X) U.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 :=
        tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
            L.X)
          U.X)
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ▷ U.X)
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst)
            (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))))
            U.X)
          (CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (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))
                U.X)
              (Iso.inv
                  (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X)
                    (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ▷
                U.X)
              (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)))))
                  ⋯ ▷
                U.X) :
            tensorObj.{v₁, u₁} (𝒞 := inst)
                (tensorObj.{v₁, u₁} (𝒞 := inst)
                  (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) L.X)
                U.X ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (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))))
                U.X)
          (TensorBimod.actRight P (Q.tensorBimod L) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (TensorBimod.X P (Q.tensorBimod L)) U.X ⟶
              TensorBimod.X P (Q.tensorBimod L))) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) L.X) U.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) L.X) U.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 (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) L.X U.X) ≫
        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)
            (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ◁ L.actRight ≫
              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) L.X) U.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 :=
        tensorObj.{v₁, u₁} (𝒞 := inst)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
            L.X)
          U.X)
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ▷ U.X)
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst)
            (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))))
            U.X)
          (CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (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))
                U.X)
              (Iso.inv
                  (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X)
                    (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ▷
                U.X)
              (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)))))
                  ⋯ ▷
                U.X) :
            tensorObj.{v₁, u₁} (𝒞 := inst)
                (tensorObj.{v₁, u₁} (𝒞 := inst)
                  (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) L.X)
                U.X ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (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))))
                U.X)
          (TensorBimod.actRight P (Q.tensorBimod L) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (TensorBimod.X P (Q.tensorBimod L)) U.X ⟶
              TensorBimod.X P (Q.tensorBimod L))) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) L.X) U.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