-- 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 (α := 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))
have h : Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
  (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))
    (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)) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) 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: slice_lhs 1 3 => rw [π_tensor_id_preserves_coequalizer_inv_desc]