-- 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
| 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 :=
      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)))
        ⋯))
have a : (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))
Tactic: rw [π_tensor_id_preserves_coequalizer_inv_desc]