awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
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)
slice_rhs :
  (Iso.hom (α_ R.X P.X S.X) ≫ R.X ◁ P.actRight) ≫ P.actLeft = Iso.hom (α_ R.X P.X S.X) ≫ R.X ◁ P.actRight ≫ P.actLeft
⊢ (Iso.hom (α_ R.X P.X S.X) ≫ R.X ◁ P.actRight) ≫ P.actLeft = P.actLeft ▷ S.X ≫ P.actRight

Tactic:
slice_rhs 1 2 => rw [middle_assoc]

Premises used: Bimod.middle_assoc
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
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)
⊢ (Iso.hom (α_ R.X P.X S.X) ≫ R.X ◁ P.actRight) ≫ P.actLeft = Iso.hom (α_ R.X P.X S.X) ≫ R.X ◁ P.actRight ≫ P.actLeft

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S : Mon.{v₁, u₁} C
P : Bimod R S
dsimp : P.actRight ▷ S.X ≫ P.actRight = (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫ P.actRight
⊢ P.actRight ▷ (regular S).X ≫ P.actRight =
    (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft) ≫ P.actRight

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
inst_2 : HasCoequalizers.{v₁, u₁} C
R S : Mon.{v₁, u₁} C
P : Bimod R S
rw : P.actRight ▷ S.X ≫ P.actRight = Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ ≫ P.actRight
rw₁ :
  P.actRight ▷ S.X ≫ P.actRight = Iso.hom (α_ P.X S.X S.X) ≫ Iso.inv (α_ P.X S.X S.X) ≫ P.actRight ▷ S.X ≫ P.actRight
rw₂ rw₃ : P.actRight ▷ S.X ≫ P.actRight = P.actRight ▷ S.X ≫ P.actRight
⊢ P.actRight ▷ S.X ≫ P.actRight = (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫ P.actRight

Tactic:
rw [Category.assoc, right_assoc, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, Bimod.right_assoc, CategoryTheory.Iso.hom_inv_id_assoc
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
dsimp :
  coequalizer.desc P.actRight ⋯ ≫
      Iso.inv (ρ_ P.X) ≫
        P.X ◁ η ≫
          coequalizer.π (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft) =
    𝟙 (coequalizer (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))
⊢ hom P ≫ inv P = 𝟙 (TensorBimod.X P (regular S))

Tactic:
dsimp only [hom, inv, TensorBimod.X]

Premises used: Bimod.RightUnitorBimod.hom, Bimod.RightUnitorBimod.inv, Bimod.TensorBimod.X
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  CategoryStruct.comp (Y :=
      coequalizer (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))
      (coequalizer.π (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))
      (coequalizer.desc P.actRight ⋯ ≫
        Iso.inv (ρ_ P.X) ≫
          P.X ◁ η ≫
            coequalizer.π (P.actRight ▷ (regular S).X)
              (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft)) =
    coequalizer.π (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft) ≫
      𝟙 (coequalizer (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))
⊢ coequalizer.desc P.actRight ⋯ ≫
      Iso.inv (ρ_ P.X) ≫
        P.X ◁ η ≫
          coequalizer.π (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft) =
    𝟙 (coequalizer (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))

Tactic:
ext
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  CategoryStruct.comp (Y := coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
      (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
      (coequalizer.desc P.actRight ⋯ ≫
        Iso.inv (ρ_ P.X) ≫ P.X ◁ η ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ CategoryStruct.comp (Y :=
      coequalizer (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))
      (coequalizer.π (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))
      (coequalizer.desc P.actRight ⋯ ≫
        Iso.inv (ρ_ P.X) ≫
          P.X ◁ η ≫
            coequalizer.π (P.actRight ▷ (regular S).X)
              (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft)) =
    coequalizer.π (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft) ≫
      𝟙 (coequalizer (P.actRight ▷ (regular S).X) (Iso.hom (α_ P.X S.X (regular S).X) ≫ P.X ◁ (regular S).actLeft))

Tactic:
dsimp
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
a : P.actRight
| CategoryStruct.comp (Y := coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
    (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) (coequalizer.desc P.actRight ⋯)

Tactic:
rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  ((P.actRight ≫ Iso.inv (ρ_ P.X)) ≫ P.X ◁ η) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ CategoryStruct.comp (Y := coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
      (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
      (coequalizer.desc P.actRight ⋯ ≫
        Iso.inv (ρ_ P.X) ≫ P.X ◁ η ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
slice_lhs 1 2 => rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
a : Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫ P.actRight ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)
| P.actRight ≫ Iso.inv (ρ_ P.X)

Tactic:
rw [rightUnitor_inv_naturality]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  ((Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫ P.actRight ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ P.X ◁ η) ≫
      coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ ((P.actRight ≫ Iso.inv (ρ_ P.X)) ≫ P.X ◁ η) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
slice_lhs 1 2 => rw [rightUnitor_inv_naturality]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
a : tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ η ≫ P.actRight ▷ S.X
| P.actRight ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫ P.X ◁ η

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ η ≫ P.actRight ▷ S.X) ≫
        coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ ((Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫ P.actRight ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ P.X ◁ η) ≫
      coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
slice_lhs 2 3 => rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
a : (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)
| P.actRight ▷ S.X ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)

Tactic:
rw [coequalizer.condition]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ η ≫
        (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ η ≫ P.actRight ▷ S.X) ≫
        coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
slice_lhs 3 4 => rw [coequalizer.condition]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
a : Iso.hom (α_ P.X S.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ P.X ◁ S.X ◁ η
| tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ η ≫ Iso.hom (α_ P.X S.X S.X)

Tactic:
rw [associator_naturality_right]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_right
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      ((Iso.hom (α_ P.X S.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ P.X ◁ S.X ◁ η) ≫ P.X ◁ μ) ≫
        coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ η ≫
        (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
slice_lhs 2 3 => rw [associator_naturality_right]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_right
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
a : P.X ◁ Iso.hom (ρ_ S.X)
| P.X ◁ S.X ◁ η ≫ P.X ◁ μ

Tactic:
rw [← whiskerLeft_comp, MonObj.mul_one]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonObj.mul_one
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      Iso.hom (α_ P.X S.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        P.X ◁ Iso.hom (ρ_ S.X) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      ((Iso.hom (α_ P.X S.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ P.X ◁ S.X ◁ η) ≫ P.X ◁ μ) ≫
        coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
slice_lhs 3 4 => rw [← whiskerLeft_comp, MonObj.mul_one]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonObj.mul_one
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
rw : coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)
| coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
    𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ⟶ coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
    (Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      Iso.hom (α_ P.X S.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        P.X ◁ Iso.hom (ρ_ S.X) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
    (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
⊢ Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      Iso.hom (α_ P.X S.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        P.X ◁ Iso.hom (ρ_ S.X) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) =
    coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ) ≫
      𝟙 (coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
slice_rhs 1 2 => rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ⟶ coequalizer (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
    (Iso.inv (ρ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X)) ≫
      Iso.hom (α_ P.X S.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        P.X ◁ Iso.hom (ρ_ S.X) ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
    (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))

Tactic:
monoidal
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
dsimp :
  CategoryStruct.comp (Y := TensorBimod.X P (regular S))
      (Iso.inv (ρ_ P.X) ≫ P.X ◁ η ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
      (coequalizer.desc P.actRight ⋯) =
    𝟙 P.X
⊢ CategoryStruct.comp (Y := TensorBimod.X P (regular S)) (inv P) (hom P) = 𝟙 P.X

Tactic:
dsimp [hom, inv]

Premises used: Bimod.RightUnitorBimod.hom, Bimod.RightUnitorBimod.inv
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
a : P.actRight
| CategoryStruct.comp (Y := TensorBimod.X P (regular S))
    (coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) (coequalizer.desc P.actRight ⋯)

Tactic:
rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
slice_lhs : Iso.inv (ρ_ P.X) ≫ P.X ◁ η ≫ P.actRight = 𝟙 P.X
⊢ CategoryStruct.comp (Y := TensorBimod.X P (regular S))
      (Iso.inv (ρ_ P.X) ≫ P.X ◁ η ≫ coequalizer.π (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ))
      (coequalizer.desc P.actRight ⋯) =
    𝟙 P.X

Tactic:
slice_lhs 3 4 => rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
rw :
  Eq.{v₁ + 1} (α := P.X ⟶ P.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (Iso.inv (ρ_ P.X)) (Iso.hom (ρ_ P.X)))
    (𝟙 P.X)
rw₁ rw₂ : Eq.{v₁ + 1} (α := P.X ⟶ P.X) (𝟙 P.X) (𝟙 P.X)
⊢ Iso.inv (ρ_ P.X) ≫ P.X ◁ η ≫ P.actRight = 𝟙 P.X

Tactic:
rw [actRight_one, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, Bimod.actRight_one
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
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)
dsimp :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) R.X (TensorBimod.X P (regular S)) ⟶ P.X)
    (TensorBimod.actLeft P (regular S) ≫ hom P) (R.X ◁ hom P ≫ P.actLeft)
⊢ (P.tensorBimod (regular S)).actLeft ≫ hom P = R.X ◁ hom P ≫ P.actLeft

Tactic:
dsimp
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
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)
dsimp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) R.X
        (TensorBimod.X P
          { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod S S }) ⟶
      P.X)
    (CategoryStruct.comp (Y :=
      TensorBimod.X P
        { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod S S })
      (CategoryStruct.comp (Y :=
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) S.X))
          (R.X ◁ P.actRight ▷ S.X) (R.X ◁ (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)))
        (Iso.inv (PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)))
        (colimMap
          (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) (P.actRight ▷ S.X)
            (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)
            (Iso.inv (α_ R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) S.X) ≫
              Iso.inv (α_ R.X P.X S.X) ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X)
            (Iso.inv (α_ R.X P.X S.X) ≫ P.actLeft ▷ S.X) ⋯ ⋯)))
      (coequalizer.desc P.actRight ⋯))
    (R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) R.X (TensorBimod.X P (regular S)) ⟶ P.X)
    (TensorBimod.actLeft P (regular S) ≫ hom P) (R.X ◁ hom P ≫ P.actLeft)

Tactic:
dsimp [hom, TensorBimod.actLeft, regular]

Premises used: Bimod.TensorBimod.actLeft, Bimod.RightUnitorBimod.hom, Bimod.regular
-- 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
R S : Mon.{v₁, u₁} C
P : Bimod R S
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)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) R.X
        (TensorBimod.X P
          { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod S S }) ⟶
      P.X)
    (CategoryStruct.comp (Y :=
      TensorBimod.X P
        { X := S.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod S S })
      (CategoryStruct.comp (Y :=
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) S.X))
          (R.X ◁ P.actRight ▷ S.X) (R.X ◁ (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)))
        (Iso.inv (PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)))
        (colimMap
          (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)) (P.actRight ▷ S.X)
            (Iso.hom (α_ P.X S.X S.X) ≫ P.X ◁ μ)
            (Iso.inv (α_ R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) S.X) ≫
              Iso.inv (α_ R.X P.X S.X) ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X)
            (Iso.inv (α_ R.X P.X S.X) ≫ P.actLeft ▷ S.X) ⋯ ⋯)))
      (coequalizer.desc P.actRight ⋯))
    (R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft)

Tactic:
(cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Functor.map, CategoryTheory.MonoidalCategory.tensorLeft, Bimod.TensorBimod.X, Iff.mp, CategoryTheory.Limits.coequalizer.π, CategoryTheory.cancel_epi