Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (tensorRight S.X).map
        (coequalizer.π
          (P.actRight ▷
            { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.X)
          ((α_ P.X S.X
                { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
            P.X ◁
              { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫
      ((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
          colimMap
            (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X) (P.actRight ▷ S.X)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
              ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ μ ≫ (α_ P.X S.X S.X).inv)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ⋯ ⋯)) ≫
        coequalizer.desc P.actRight ⋯ =
    (tensorRight S.X).map
        (coequalizer.π
          (P.actRight ▷
            { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ }.X)
          ((α_ P.X S.X
                { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫
            P.X ◁
              { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                  right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫
      coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X ≫
      ((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)).inv ≫
          colimMap
            (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X) (P.actRight ▷ S.X)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ)
              ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ μ ≫ (α_ P.X S.X S.X).inv)
              ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ⋯ ⋯)) ≫
        coequalizer.desc P.actRight ⋯ =
    coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ▷ S.X ≫
      coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight