-- 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
      (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
      (CategoryStruct.comp (Y :=
        TensorBimod.X M
          ({ X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }.tensorBimod
            N))
        (CategoryStruct.comp (Y :=
            coequalizer (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) Y.X) N.X)
              (M.actRight ▷ Y.X ▷ N.X) ((Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X))
            (Iso.inv
              (PreservesCoequalizer.iso (tensorRight N.X) (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)))
            (coequalizer.desc
              (Iso.hom (α_ M.X Y.X N.X) ≫
                CategoryStruct.comp (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                    (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
                  (M.X ◁ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) Y.X N.X) ⟶
                      tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                        (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
                  (coequalizer.π
                      (M.actRight ▷
                        TensorBimod.X
                          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                            right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                          N)
                      (Iso.hom
                          (α_ M.X Y.X
                            (TensorBimod.X
                              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ,
                                actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                              N)) ≫
                        M.X ◁
                          TensorBimod.actLeft
                            { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ,
                              actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }
                            N) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                        (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)) ⟶
                      coequalizer (X :=
                        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X)
                          (TensorBimod.X
                            { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ,
                              actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                            N))
                        (M.actRight ▷
                          TensorBimod.X
                            { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ,
                              actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                            N)
                        (Iso.hom
                            (α_ M.X Y.X
                              (TensorBimod.X
                                { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ,
                                  actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                                N)) ≫
                          M.X ◁
                            TensorBimod.actLeft
                              { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ,
                                actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }
                              N)))
              ⋯) :
          tensorObj.{v₁, u₁} (𝒞 := inst)
              (TensorBimod.X M
                { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y })
              N.X ⟶
            TensorBimod.X M
              ({ X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }.tensorBimod
                N))
        (colimMap
            (parallelPairHom
              (M.actRight ▷
                TensorBimod.X
                  { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                  N)
              (Iso.hom
                  (α_ M.X Y.X
                    (TensorBimod.X
                      { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                        right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                      N)) ≫
                M.X ◁
                  TensorBimod.actLeft
                    { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                      right_assoc := ⋯, middle_assoc := ⋯ }
                    N)
              (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)
              (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ LeftUnitorBimod.hom N) (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯) :
          colimit
              (parallelPair (X :=
                tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X)
                  (TensorBimod.X
                    { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                      right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                    N))
                (M.actRight ▷
                  TensorBimod.X
                    { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                      right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                    N)
                (Iso.hom
                    (α_ M.X Y.X
                      (TensorBimod.X
                        { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                          right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                        N)) ≫
                  M.X ◁
                    TensorBimod.actLeft
                      { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                        right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y }
                      N)) ⟶
            colimit (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
      (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
      (coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one))
⊢ Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight N.X) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X (regular Y).X) ⟶
      TensorBimod.X M N)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight N.X)
        (coequalizer (M.actRight ▷ (regular Y).X) (Iso.hom (α_ M.X Y.X (regular Y).X) ≫ M.X ◁ (regular Y).actLeft)))
      (CategoryTheory.Functor.map (tensorRight N.X)
        (coequalizer.π (M.actRight ▷ (regular Y).X) (Iso.hom (α_ M.X Y.X (regular Y).X) ≫ M.X ◁ (regular Y).actLeft)))
      (CategoryStruct.comp (Y := TensorBimod.X M ((regular Y).tensorBimod N))
        (CategoryStruct.comp (Y :=
            coequalizer (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) Y.X) N.X)
              (M.actRight ▷ Y.X ▷ N.X) ((Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X))
            (Iso.inv
              (PreservesCoequalizer.iso (tensorRight N.X) (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)))
            (coequalizer.desc
              (Iso.hom (α_ M.X Y.X N.X) ≫
                CategoryStruct.comp (Y :=
                  tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                    (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
                  (M.X ◁ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) Y.X N.X) ⟶
                      tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                        (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
                  (coequalizer.π (M.actRight ▷ TensorBimod.X (regular Y) N)
                      (Iso.hom (α_ M.X Y.X (TensorBimod.X (regular Y) N)) ≫ M.X ◁ TensorBimod.actLeft (regular Y) N) :
                    tensorObj.{v₁, u₁} (𝒞 := inst) M.X
                        (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)) ⟶
                      coequalizer (X :=
                        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X)
                          (TensorBimod.X (regular Y) N))
                        (M.actRight ▷ TensorBimod.X (regular Y) N)
                        (Iso.hom (α_ M.X Y.X (TensorBimod.X (regular Y) N)) ≫ M.X ◁ TensorBimod.actLeft (regular Y) N)))
              ⋯) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (TensorBimod.X M (regular Y)) N.X ⟶
            TensorBimod.X M ((regular Y).tensorBimod N))
        (colimMap
            (parallelPairHom (M.actRight ▷ TensorBimod.X (regular Y) N)
              (Iso.hom (α_ M.X Y.X (TensorBimod.X (regular Y) N)) ≫ M.X ◁ TensorBimod.actLeft (regular Y) N)
              (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)
              (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ LeftUnitorBimod.hom N) (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯) :
          colimit
              (parallelPair (X :=
                tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) (TensorBimod.X (regular Y) N))
                (M.actRight ▷ TensorBimod.X (regular Y) N)
                (Iso.hom (α_ M.X Y.X (TensorBimod.X (regular Y) N)) ≫ M.X ◁ TensorBimod.actLeft (regular Y) N)) ⟶
            colimit (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)))))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight N.X)
        (coequalizer (M.actRight ▷ (regular Y).X) (Iso.hom (α_ M.X Y.X (regular Y).X) ≫ M.X ◁ (regular Y).actLeft)))
      (CategoryTheory.Functor.map (tensorRight N.X)
        (coequalizer.π (M.actRight ▷ (regular Y).X) (Iso.hom (α_ M.X Y.X (regular Y).X) ≫ M.X ◁ (regular Y).actLeft)))
      (coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one))

Tactic:
dsimp [regular]

Premises used: Bimod.regular