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
A B : Mon.{v₁, u₁} C
M : Bimod A B
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a :
  P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X ≫
    P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)
| tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁
      coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) ≫
    P.actRight ▷ coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)

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
A B : Mon.{v₁, u₁} C
M : Bimod A B
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a : Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X L.X) ≫ P.actRight ▷ Q.X ▷ L.X
| P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X ≫ Iso.inv (α_ P.X Q.X L.X)

Tactic:
rw [associator_inv_naturality_left]

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

Tactic:
rw [← comp_whiskerRight, coequalizer.condition, comp_whiskerRight, comp_whiskerRight]

Premises used: CategoryTheory.Limits.coequalizer.condition, CategoryTheory.MonoidalCategory.comp_whiskerRight
-- 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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a :
  Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X)) ≫
    P.X ◁ S.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)
| tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁
      coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) ≫
    Iso.hom (α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))

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
A B : Mon.{v₁, u₁} C
M : Bimod A B
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a :
  P.X ◁ Iso.inv (α_ S.X Q.X L.X) ≫
    P.X ◁ Q.actLeft ▷ L.X ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X
        (tensorObj.{v₁, u₁} (𝒞 := inst) S.X
          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))
      (P.X ◁ S.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X)) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) S.X
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))))
      (P.X ◁ TensorBimod.actLeft Q L :
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) S.X
              (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))) :
    tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorObj.{v₁, u₁} (𝒞 := inst) S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X L.X)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))

Tactic:
rw [← whiskerLeft_comp, TensorBimod.whiskerLeft_π_actLeft,
          whiskerLeft_comp, whiskerLeft_comp]

Premises used: Bimod.TensorBimod.whiskerLeft_π_actLeft, CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- 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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a : Iso.inv (α_ P.X (tensorObj.{v₁, u₁} (𝒞 := inst) S.X Q.X) L.X) ≫ (P.X ◁ Q.actLeft) ▷ L.X
| P.X ◁ Q.actLeft ▷ L.X ≫ Iso.inv (α_ P.X Q.X L.X)

Tactic:
rw [associator_inv_naturality_middle]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_middle
-- 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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a :
  CategoryStruct.comp (Y :=
    coequalizer (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) L.X))
      (P.X ◁ Q.actRight ▷ L.X) (P.X ◁ (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
    (Iso.inv
      (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
    (coequalizer.desc
      (Iso.inv (α_ P.X Q.X L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft))
      ⋯)
| (CategoryStruct.comp (Y := TensorBimod.X P (Q.tensorBimod L))
      (coequalizer.π (P.actRight ▷ TensorBimod.X Q L)
          (Iso.hom (α_ P.X S.X (TensorBimod.X Q L)) ≫ P.X ◁ TensorBimod.actLeft Q L) :
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
          coequalizer (X := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) (TensorBimod.X Q L))
            (P.actRight ▷ TensorBimod.X Q L) (Iso.hom (α_ P.X S.X (TensorBimod.X Q L)) ≫ P.X ◁ TensorBimod.actLeft Q L))
      (coequalizer.desc
        (CategoryStruct.comp (Y :=
          coequalizer (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) L.X))
            (P.X ◁ Q.actRight ▷ L.X) (P.X ◁ (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Iso.inv
            (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (coequalizer.desc
            (Iso.inv (α_ P.X Q.X L.X) ≫
              coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
                coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
                  (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft))
            ⋯))
        ⋯) :
    tensorObj.{v₁, u₁} (𝒞 := inst) P.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)) ⟶
      TensorBimod.X (P.tensorBimod Q) L)

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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a :
  Iso.inv (α_ P.X Q.X L.X) ≫
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft)
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) P.X (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
    (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))
    (CategoryStruct.comp (Y :=
      coequalizer (X :=
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) L.X))
        (P.X ◁ Q.actRight ▷ L.X) (P.X ◁ (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
      (Iso.inv
        (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
      (coequalizer.desc
        (Iso.inv (α_ P.X Q.X L.X) ≫
          coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
            coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
              (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft))
        ⋯))

Tactic:
rw [id_tensor_π_preserves_coequalizer_inv_desc]

Premises used: id_tensor_π_preserves_coequalizer_inv_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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
h :
  Iso.hom (α_ P.X Q.X L.X) ≫
      Iso.inv (α_ P.X Q.X L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)
⊢ Iso.hom (α_ P.X Q.X L.X) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) P.X
          (coequalizer (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (P.X ◁ coequalizer.π (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft))
        (CategoryStruct.comp (Y :=
          coequalizer (X :=
            tensorObj.{v₁, u₁} (𝒞 := inst) P.X
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) L.X))
            (P.X ◁ Q.actRight ▷ L.X) (P.X ◁ (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (Iso.inv
            (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
          (coequalizer.desc
            (Iso.inv (α_ P.X Q.X L.X) ≫
              coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
                coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
                  (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft))
            ⋯)) =
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)

Tactic:
slice_lhs 2 4 => rw [id_tensor_π_preserves_coequalizer_inv_desc]

Premises used: id_tensor_π_preserves_coequalizer_inv_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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a : coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X
| Iso.hom (α_ P.X Q.X L.X) ≫
    Iso.inv (α_ P.X Q.X L.X) ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X

Tactic:
rw [Iso.hom_inv_id_assoc]

Premises used: 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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
h :
  coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)
⊢ Iso.hom (α_ P.X Q.X L.X) ≫
      Iso.inv (α_ P.X Q.X L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)

Tactic:
slice_lhs 1 3 => rw [Iso.hom_inv_id_assoc]

Premises used: 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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
h :
  CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) L.X)
      (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X :
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) L.X ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
            L.X)
      (coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
          (Iso.hom (α_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) T.X L.X) ≫
            coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
            L.X ⟶
          coequalizer (TensorBimod.actRight P Q ▷ L.X)
            (Iso.hom (α_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) T.X L.X) ≫
              coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)) =
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙
          (coequalizer ((P.tensorBimod Q).actRight ▷ L.X)
            (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft))
⊢ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
        (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft) =
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
        𝟙 (TensorBimod.X (P.tensorBimod Q) L)

Tactic:
dsimp only [TensorBimod.X]

Premises used: 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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a :
  coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
    (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft)
| coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
      (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
    𝟙
      (coequalizer ((P.tensorBimod Q).actRight ▷ L.X)
        (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft))

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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight L.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer ((P.tensorBimod Q).actRight ▷ L.X)
        (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft))
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
          L.X)
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) L.X ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
              L.X)
        (coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            (Iso.hom (α_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) T.X L.X) ≫
              coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ◁ L.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
              L.X ⟶
            coequalizer (TensorBimod.actRight P Q ▷ L.X)
              (Iso.hom (α_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) T.X L.X) ≫
                coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ◁ L.actLeft)) :
      Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight L.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
        coequalizer ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft))
    (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
        coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft) :
      Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight L.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
        coequalizer ((P.tensorBimod Q).actRight ▷ L.X)
          (Iso.hom (α_ (P.tensorBimod Q).X T.X L.X) ≫ (P.tensorBimod Q).X ◁ L.actLeft))

Tactic:
rfl
-- 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
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)
R S T U : Mon.{v₁, u₁} C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
a :
  CategoryStruct.comp (Y :=
    coequalizer (X :=
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) L.X))
      (P.X ◁ Q.actRight ▷ L.X) (P.X ◁ (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
    (Iso.inv
      (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
    (coequalizer.desc
      (Iso.inv (α_ P.X Q.X L.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
            (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft))
      ⋯)
| CategoryStruct.comp (Y :=
    coequalizer (P.actRight ▷ (Q.tensorBimod L).X)
      (Iso.hom (α_ P.X S.X (Q.tensorBimod L).X) ≫ P.X ◁ (Q.tensorBimod L).actLeft))
    (coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
      (Iso.hom (α_ P.X S.X (Q.tensorBimod L).X) ≫ P.X ◁ (Q.tensorBimod L).actLeft))
    (coequalizer.desc
      (CategoryStruct.comp (Y :=
        coequalizer (X :=
          tensorObj.{v₁, u₁} (𝒞 := inst) P.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) L.X))
          (P.X ◁ Q.actRight ▷ L.X) (P.X ◁ (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (Iso.inv
          (PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) (Iso.hom (α_ Q.X T.X L.X) ≫ Q.X ◁ L.actLeft)))
        (coequalizer.desc
          (Iso.inv (α_ P.X Q.X L.X) ≫
            coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
              coequalizer.π (TensorBimod.actRight P Q ▷ L.X)
                (Iso.hom (α_ (TensorBimod.X P Q) T.X L.X) ≫ TensorBimod.X P Q ◁ L.actLeft))
          ⋯))
      ⋯)

Tactic:
rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc