-- 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
⊢ 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))
have 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 := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
              right_assoc := sorry, middle_assoc := sorry : 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 := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                          right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                        N)
                    (Iso.hom
                        (α_ M.X Y.X
                          (TensorBimod.X
                            { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ,
                              actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                            N)) ≫
                      M.X ◁
                        TensorBimod.actLeft
                          { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                            right_assoc := sorry, middle_assoc := sorry }
                          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 := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                            right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                          N))
                      (M.actRight ▷
                        TensorBimod.X
                          { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                            right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                          N)
                      (Iso.hom
                          (α_ M.X Y.X
                            (TensorBimod.X
                              { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ,
                                actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                              N)) ≫
                        M.X ◁
                          TensorBimod.actLeft
                            { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ,
                              actRight_one := sorry, right_assoc := sorry, middle_assoc := sorry }
                            N)))
            sorry) :
        tensorObj.{v₁, u₁} (𝒞 := inst)
            (TensorBimod.X M
              { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                right_assoc := sorry, middle_assoc := sorry : Bimod Y Y })
            N.X ⟶
          TensorBimod.X M
            ({ X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                  right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }.tensorBimod
              N))
      (colimMap
          (parallelPairHom
            (M.actRight ▷
              TensorBimod.X
                { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                  right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                N)
            (Iso.hom
                (α_ M.X Y.X
                  (TensorBimod.X
                    { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                      right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                    N)) ≫
              M.X ◁
                TensorBimod.actLeft
                  { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                    right_assoc := sorry, middle_assoc := sorry }
                  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) sorry sorry) :
        colimit
            (parallelPair (X :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X)
                (TensorBimod.X
                  { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                    right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                  N))
              (M.actRight ▷
                TensorBimod.X
                  { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                    right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                  N)
              (Iso.hom
                  (α_ M.X Y.X
                    (TensorBimod.X
                      { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                        right_assoc := sorry, middle_assoc := sorry : Bimod Y Y }
                      N)) ≫
                M.X ◁
                  TensorBimod.actLeft
                    { X := Y.X, actLeft := μ, one_actLeft := sorry, left_assoc := sorry, actRight := μ, actRight_one := sorry,
                      right_assoc := sorry, middle_assoc := sorry : 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 sorry ▷ 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]