-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Bimod (goal)
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)
W X Y Z : Mon.{v₁, u₁} C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
      coequalizer (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
          (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
          (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
        (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
        (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
            M'.X ◁ TensorBimod.actLeft N P :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))))
    (f.hom ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) ≫
        colimit.ι
          (parallelPair (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
                tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
                M'.X ◁ TensorBimod.actLeft N P :
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
                tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))))
          WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
        colimit
          (parallelPair (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
                tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
                M'.X ◁ TensorBimod.actLeft N P :
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
                tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                  (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))))
    (CategoryStruct.comp (Y :=
        coequalizer (TensorBimod.actRight M' N ▷ P.X)
          (Iso.hom (α_ (coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft)) Y.X P.X) ≫
            coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) ◁ P.actLeft))
        (AssociatorBimod.invAux M N P ≫
            colimMap
              (parallelPairHom (TensorBimod.actRight M N ▷ P.X)
                (Iso.hom (α_ (coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft)) Y.X P.X) ≫
                  coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) ◁ P.actLeft)
                (TensorBimod.actRight M' N ▷ P.X)
                (Iso.hom (α_ (coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft)) Y.X P.X) ≫
                  coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) ◁ P.actLeft)
                (colimMap
                      (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft)
                        (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X)
                        (f.hom ▷ N.X) ⋯ ⋯) ▷
                    Y.X ▷
                  P.X)
                (colimMap
                    (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X)
                      (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷
                  P.X)
                ⋯ ⋯) :
          tensorObj.{v₁, u₁} (𝒞 := inst) M.X
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
            coequalizer (TensorBimod.actRight M' N ▷ P.X)
              (Iso.hom (α_ (coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft)) Y.X P.X) ≫
                coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) ◁ P.actLeft))
        (AssociatorBimod.hom M' N P : ((M'.tensorBimod N).tensorBimod P).X ⟶ (M'.tensorBimod (N.tensorBimod P)).X) :
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
              M'.X ◁ TensorBimod.actLeft N P :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
    coequalizer (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
        (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
      (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) M'.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
      (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
      (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
          M'.X ◁ TensorBimod.actLeft N P :
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))))
  (f.hom ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) ≫
      colimit.ι
        (parallelPair (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
              M'.X ◁ TensorBimod.actLeft N P :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))))
        WalkingParallelPair.one :
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
      colimit
        (parallelPair (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
          (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
              M'.X ◁ TensorBimod.actLeft N P :
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
                (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))))
  (CategoryStruct.comp (Y :=
      coequalizer (TensorBimod.actRight M' N ▷ P.X)
        (Iso.hom (α_ (coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft)) Y.X P.X) ≫
          coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) ◁ P.actLeft))
      (CategoryStruct.comp (Y :=
            coequalizer (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X) P.X))
              (M.X ◁ N.actRight ▷ P.X) (M.X ◁ (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (Iso.inv
              (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P.X)
                (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
            (coequalizer.desc
              (Iso.inv (α_ M.X N.X P.X) ≫
                coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) ▷ P.X ≫
                  coequalizer.π (TensorBimod.actRight M N ▷ P.X)
                    (Iso.hom (α_ (TensorBimod.X M N) Y.X P.X) ≫ TensorBimod.X M N ◁ P.actLeft))
              sorry) ≫
          colimMap
            (parallelPairHom (TensorBimod.actRight M N ▷ P.X)
              (Iso.hom (α_ (coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft)) Y.X P.X) ≫
                coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) ◁ P.actLeft)
              (TensorBimod.actRight M' N ▷ P.X)
              (Iso.hom (α_ (coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft)) Y.X P.X) ≫
                coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) ◁ P.actLeft)
              (colimMap
                    (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X)
                      (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) sorry sorry) ▷
                  Y.X ▷
                P.X)
              (colimMap
                  (parallelPairHom (M.actRight ▷ N.X) (Iso.hom (α_ M.X X.X N.X) ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X)
                    (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) sorry sorry) ▷
                P.X)
              sorry sorry) :
        tensorObj.{v₁, u₁} (𝒞 := inst) M.X
            (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
          coequalizer (TensorBimod.actRight M' N ▷ P.X)
            (Iso.hom (α_ (coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft)) Y.X P.X) ≫
              coequalizer (M'.actRight ▷ N.X) (Iso.hom (α_ M'.X X.X N.X) ≫ M'.X ◁ N.actLeft) ◁ P.actLeft))
      (coequalizer.desc (AssociatorBimod.homAux M' N P) sorry :
        coequalizer (TensorBimod.actRight M' N ▷ P.X)
            (Iso.hom (α_ (TensorBimod.X M' N) Y.X P.X) ≫ TensorBimod.X M' N ◁ P.actLeft) ⟶
          TensorBimod.X M' (N.tensorBimod P)) :
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
      coequalizer (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
          (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
        (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
          (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
        (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)))
        (Iso.hom (α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))) ≫
            M'.X ◁ TensorBimod.actLeft N P :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M'.X X.X)
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M'.X
              (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft))))
Tactic: dsimp [AssociatorBimod.invAux, AssociatorBimod.hom]