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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X M Q)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (M.actRight ▷ Q.X)
            (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ g.hom) (M.X ◁ g.hom)
            ⋯ ⋯))
        (colimMap
          (parallelPairHom (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯))))
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ (N.tensorBimod Q).X)
    (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) ≫
      Hom.hom (M.whiskerLeft g ≫ whiskerRight f Q))
    (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) ≫
      Hom.hom (whiskerRight f P ≫ N.whiskerLeft g))

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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
a :
  M.X ◁ g.hom ≫
    colimit.ι (parallelPair (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft)) WalkingParallelPair.one
| CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
    (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
    (colimMap
      (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (M.actRight ▷ Q.X)
        (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ g.hom) (M.X ◁ g.hom) ⋯
        ⋯))

Tactic:
rw [ι_colimMap, parallelPairHom_app_one]

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.parallelPairHom_app_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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
a :
  f.hom ▷ Q.X ≫
    colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one
| CategoryStruct.comp (Y := TensorBimod.X M Q)
    (colimit.ι (parallelPair (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft)) WalkingParallelPair.one)
    (colimMap
      (parallelPairHom (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
        (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯))

Tactic:
rw [ι_colimMap, parallelPairHom_app_one]

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.parallelPairHom_app_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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    (M.X ◁ g.hom ≫
      f.hom ▷ Q.X ≫
        colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft))
          WalkingParallelPair.one)
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    (CategoryStruct.comp (Y := TensorBimod.X M Q)
      (M.X ◁ g.hom ≫
        colimit.ι (parallelPair (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft))
          WalkingParallelPair.one)
      (colimMap
        (parallelPairHom (M.actRight ▷ Q.X) (Iso.hom (α_ M.X Y.X Q.X) ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
          (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯)))
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))

Tactic:
slice_lhs 2 3 => rw [ι_colimMap, parallelPairHom_app_one]

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.parallelPairHom_app_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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
a : f.hom ▷ P.X ≫ N.X ◁ g.hom
| M.X ◁ g.hom ≫ f.hom ▷ Q.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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    ((f.hom ▷ P.X ≫ N.X ◁ g.hom) ≫
      colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one)
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    (M.X ◁ g.hom ≫
      f.hom ▷ Q.X ≫
        colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft))
          WalkingParallelPair.one)
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))

Tactic:
slice_lhs 1 2 => 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
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 N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X P.X ⟶ TensorBimod.X N Q)
    ((f.hom ▷ P.X ≫ N.X ◁ g.hom) ≫
      colimit.ι (parallelPair (N.actRight ▷ Q.X) (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft)) WalkingParallelPair.one)
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (coequalizer.π (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft))
      (CategoryStruct.comp (Y := TensorBimod.X N P)
        (colimMap
          (parallelPairHom (M.actRight ▷ P.X) (Iso.hom (α_ M.X Y.X P.X) ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯))
        (colimMap
          (parallelPairHom (N.actRight ▷ P.X) (Iso.hom (α_ N.X Y.X P.X) ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            (Iso.hom (α_ N.X Y.X Q.X) ≫ N.X ◁ Q.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) N.X Y.X ◁ g.hom) (N.X ◁ g.hom)
            ⋯ ⋯))))

Tactic:
simp
-- 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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
dsimp :
  whiskerRight
        (Iso.hom
          (isoOfIso
            { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ :
              TensorBimod.X (M.tensorBimod N) P ≅ TensorBimod.X M (N.tensorBimod P) }
            ⋯ ⋯))
        Q ≫
      Iso.hom
          (isoOfIso
            { hom := AssociatorBimod.hom M (N.tensorBimod P) Q, inv := AssociatorBimod.inv M (N.tensorBimod P) Q,
              hom_inv_id := ⋯, inv_hom_id := ⋯ :
              TensorBimod.X (M.tensorBimod (N.tensorBimod P)) Q ≅ TensorBimod.X M ((N.tensorBimod P).tensorBimod Q) }
            ⋯ ⋯) ≫
        M.whiskerLeft
          (Iso.hom
            (isoOfIso
              { hom := AssociatorBimod.hom N P Q, inv := AssociatorBimod.inv N P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ :
                TensorBimod.X (N.tensorBimod P) Q ≅ TensorBimod.X N (P.tensorBimod Q) }
              ⋯ ⋯)) =
    Iso.hom
        (isoOfIso
          { hom := AssociatorBimod.hom (M.tensorBimod N) P Q, inv := AssociatorBimod.inv (M.tensorBimod N) P Q,
            hom_inv_id := ⋯, inv_hom_id := ⋯ :
            TensorBimod.X ((M.tensorBimod N).tensorBimod P) Q ≅ TensorBimod.X (M.tensorBimod N) (P.tensorBimod Q) }
          ⋯ ⋯) ≫
      Iso.hom
        (isoOfIso
          { hom := AssociatorBimod.hom M N (P.tensorBimod Q), inv := AssociatorBimod.inv M N (P.tensorBimod Q),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }
          ⋯ ⋯)
⊢ whiskerRight (Iso.hom (M.associatorBimod N P)) Q ≫
      Iso.hom (M.associatorBimod (N.tensorBimod P) Q) ≫ M.whiskerLeft (Iso.hom (N.associatorBimod P Q)) =
    Iso.hom ((M.tensorBimod N).associatorBimod P Q) ≫ Iso.hom (M.associatorBimod N (P.tensorBimod Q))

Tactic:
dsimp [associatorBimod]

Premises used: Bimod.associatorBimod
-- 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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a :
  coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X ≫
    colimit.ι
      (parallelPair (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X) ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.actLeft))
      WalkingParallelPair.one
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (colimMap
      (parallelPairHom (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft)
        (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X) ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.actLeft)
        (coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Y.X ▷ Q.X)
        (coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X) ⋯ ⋯))

Tactic:
rw [ι_colimMap, parallelPairHom_app_one]

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.parallelPairHom_app_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
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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a : AssociatorBimod.homAux M (N.tensorBimod P) Q
| CategoryStruct.comp (Y := TensorBimod.X (M.tensorBimod (N.tensorBimod P)) Q)
    (colimit.ι
      (parallelPair (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X) ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.actLeft))
      WalkingParallelPair.one)
    (coequalizer.desc (AssociatorBimod.homAux M (N.tensorBimod P) Q) ⋯)

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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a : AssociatorBimod.homAux (M.tensorBimod N) P Q
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
      (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
    (coequalizer.desc (AssociatorBimod.homAux (M.tensorBimod N) P Q) ⋯)

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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
h :
  coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X ≫
      AssociatorBimod.homAux M (N.tensorBimod P) Q ≫
        colimMap
          (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q)
            (Iso.hom (α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)) ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)
            (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q))
            (Iso.hom (α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))) ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))
            (tensorObj.{v₁, u₁} (𝒞 := inst) M.X W.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯)
            (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) ⋯ ⋯) =
    AssociatorBimod.homAux (M.tensorBimod N) P Q ≫ coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) ⋯
⊢ coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X ≫
      AssociatorBimod.homAux M (N.tensorBimod P) Q ≫
        colimMap
          (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q)
            (Iso.hom (α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)) ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)
            (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q))
            (Iso.hom (α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))) ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))
            (tensorObj.{v₁, u₁} (𝒞 := inst) M.X W.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯)
            (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) ⋯ ⋯) =
    CategoryStruct.comp (Y :=
      coequalizer (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
      (coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X)
        (Iso.hom (α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X) ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft))
      (coequalizer.desc (AssociatorBimod.homAux (M.tensorBimod N) P Q) ⋯ ≫
        coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) ⋯)

Tactic:
slice_rhs 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
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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a :
  Iso.hom (α_ M.X (tensorObj.{v₁, u₁} (𝒞 := inst) N.X P.X) Q.X) ≫
    M.X ◁ coequalizer.π (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft) ▷ Q.X
| (M.X ◁ coequalizer.π (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft)) ▷ Q.X ≫
    Iso.hom (α_ M.X (coequalizer (N.actRight ▷ P.X) (Iso.hom (α_ N.X X.X P.X) ≫ N.X ◁ P.actLeft)) Q.X)

Tactic:
rw [associator_naturality_middle]

Premises used: CategoryTheory.MonoidalCategory.associator_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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
slice_lhs 2 3 => rw [associator_naturality_middle]

Premises used: CategoryTheory.MonoidalCategory.associator_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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a :
  Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X) P.X Q.X) ≫
    coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X
| coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷ P.X ▷ Q.X ≫
    Iso.hom (α_ (coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft)) P.X Q.X)

Tactic:
rw [associator_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_left
-- 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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a :
  tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X ◁
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)
| coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ▷
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
    coequalizer (M.actRight ▷ N.X) (Iso.hom (α_ M.X W.X N.X) ≫ M.X ◁ N.actLeft) ◁
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange