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

Tactic:
simp
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
rw rw₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N₁.X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₂.X)
    (M.actRight ▷ N₁.X ≫ M.X ◁ f.hom) (M.actRight ▷ N₁.X ≫ M.X ◁ f.hom)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N₁.X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₂.X)
    (M.actRight ▷ N₁.X ≫ M.X ◁ f.hom) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom ≫ M.actRight ▷ N₂.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
A B : Mon.{v₁, u₁} C
M_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
simp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) Y.X N₁.X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₂.X)
    (M.X ◁ N₁.actLeft ≫ M.X ◁ f.hom) (M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.actLeft)
⊢ (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) ≫ M.X ◁ f.hom =
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom ≫ Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft

Tactic:
simp only [Category.assoc, tensor_whiskerLeft, Iso.inv_hom_id_assoc,
            Iso.cancel_iso_hom_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.cancel_iso_hom_left, CategoryTheory.MonoidalCategory.tensor_whiskerLeft
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
rw : M.X ◁ (Y.X ◁ f.hom ≫ N₂.actLeft)
| M.X ◁ N₁.actLeft ≫ M.X ◁ f.hom

Tactic:
rw [← whiskerLeft_comp, Hom.left_act_hom]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, Bimod.Hom.left_act_hom
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) Y.X N₁.X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₂.X)
    (M.X ◁ (Y.X ◁ f.hom ≫ N₂.actLeft)) (M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.actLeft)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) Y.X N₁.X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₂.X)
    (M.X ◁ N₁.actLeft ≫ M.X ◁ f.hom) (M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.actLeft)

Tactic:
slice_lhs 1 2 => rw [← whiskerLeft_comp, Hom.left_act_hom]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, Bimod.Hom.left_act_hom
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (tensorObj.{v₁, u₁} (𝒞 := inst) Y.X N₁.X) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₂.X)
    (M.X ◁ (Y.X ◁ f.hom ≫ N₂.actLeft)) (M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.actLeft)

Tactic:
simp
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
⊢ (M.tensorBimod N₁).actLeft ≫
      colimMap
        (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
          (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom) (M.X ◁ f.hom)
          ⋯ ⋯) =
    X.X ◁
        colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
            (M.X ◁ f.hom) ⋯ ⋯) ≫
      (M.tensorBimod N₂).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
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
refine :
  Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft X.X) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ (M.tensorBimod N₂).X)
    (CategoryTheory.Functor.map (tensorLeft X.X)
        (coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft)) ≫
      (M.tensorBimod N₁).actLeft ≫
        colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
            (M.X ◁ f.hom) ⋯ ⋯))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft X.X)
        (coequalizer (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft)))
      (CategoryTheory.Functor.map (tensorLeft X.X)
        (coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft)))
      (X.X ◁
          colimMap
            (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
              (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
              (M.X ◁ f.hom) ⋯ ⋯) ≫
        (M.tensorBimod N₂).actLeft))
⊢ (M.tensorBimod N₁).actLeft ≫
      colimMap
        (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
          (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom) (M.X ◁ f.hom)
          ⋯ ⋯) =
    X.X ◁
        colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
            (M.X ◁ f.hom) ⋯ ⋯) ≫
      (M.tensorBimod N₂).actLeft

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

Premises used: CategoryTheory.Functor.map, CategoryTheory.MonoidalCategory.tensorLeft, Iff.mp, CategoryTheory.Limits.coequalizer.π, CategoryTheory.cancel_epi
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
a :
  Iso.inv (α_ X.X M.X N₁.X) ≫
    M.actLeft ▷ N₁.X ≫ coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft)
| X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) ≫ TensorBimod.actLeft M N₁

Tactic:
rw [TensorBimod.whiskerLeft_π_actLeft]

Premises used: Bimod.TensorBimod.whiskerLeft_π_actLeft
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
a :
  M.X ◁ f.hom ≫
    colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one
| CategoryStruct.comp (Y := TensorBimod.X M N₁)
    (coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft))
    (colimMap
      (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
        (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom) (M.X ◁ f.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
A B : Mon.{v₁, u₁} C
M_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
slice_lhs :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (Iso.inv (α_ X.X M.X N₁.X) ≫
        M.actLeft ▷ N₁.X ≫
          M.X ◁ f.hom ≫
            colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
              WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X.X
          (coequalizer (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft)))
        (X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft))
        (X.X ◁
            colimMap
              (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
                (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
                (M.X ◁ f.hom) ⋯ ⋯) ≫
          TensorBimod.actLeft M N₂) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (CategoryStruct.comp (Y := TensorBimod.X M N₁)
        (Iso.inv (α_ X.X M.X N₁.X) ≫
          M.actLeft ▷ N₁.X ≫ coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft))
        (colimMap
          (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
            (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
            (M.X ◁ f.hom) ⋯ ⋯)) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X.X
          (coequalizer (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft)))
        (X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft))
        (X.X ◁
            colimMap
              (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
                (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
                (M.X ◁ f.hom) ⋯ ⋯) ≫
          TensorBimod.actLeft M N₂) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)

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

Tactic:
rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one,
      whiskerLeft_comp]

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.MonoidalCategory.whiskerLeft_comp, 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
A B : Mon.{v₁, u₁} C
M_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
slice_rhs :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (Iso.inv (α_ X.X M.X N₁.X) ≫
        M.actLeft ▷ N₁.X ≫
          M.X ◁ f.hom ≫
            colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
              WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    ((X.X ◁ M.X ◁ f.hom ≫
          X.X ◁
            colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
              WalkingParallelPair.one) ≫
        TensorBimod.actLeft M N₂ :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (Iso.inv (α_ X.X M.X N₁.X) ≫
        M.actLeft ▷ N₁.X ≫
          M.X ◁ f.hom ≫
            colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
              WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X.X
          (coequalizer (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft)))
        (X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft))
        (X.X ◁
            colimMap
              (parallelPairHom (M.actRight ▷ N₁.X) (Iso.hom (α_ M.X Y.X N₁.X) ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X)
                (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ◁ f.hom)
                (M.X ◁ f.hom) ⋯ ⋯) ≫
          TensorBimod.actLeft M N₂) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)

Tactic:
slice_rhs 1 2 => rw [← whiskerLeft_comp, ι_colimMap, parallelPairHom_app_one,
      whiskerLeft_comp]

Premises used: CategoryTheory.Limits.ι_colimMap, CategoryTheory.MonoidalCategory.whiskerLeft_comp, 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
A B : Mon.{v₁, u₁} C
M_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
a :
  Iso.inv (α_ X.X M.X N₂.X) ≫
    M.actLeft ▷ N₂.X ≫ coequalizer.π (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft)
| X.X ◁
      colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
        WalkingParallelPair.one ≫
    TensorBimod.actLeft M N₂

Tactic:
rw [TensorBimod.whiskerLeft_π_actLeft]

Premises used: Bimod.TensorBimod.whiskerLeft_π_actLeft
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
slice_rhs :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (Iso.inv (α_ X.X M.X N₁.X) ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one)
    (X.X ◁ M.X ◁ f.hom ≫
      Iso.inv (α_ X.X M.X N₂.X) ≫
        M.actLeft ▷ N₂.X ≫ coequalizer.π (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (Iso.inv (α_ X.X M.X N₁.X) ≫
        M.actLeft ▷ N₁.X ≫
          M.X ◁ f.hom ≫
            colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
              WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    ((X.X ◁ M.X ◁ f.hom ≫
          X.X ◁
            colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
              WalkingParallelPair.one) ≫
        TensorBimod.actLeft M N₂ :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)

Tactic:
slice_rhs 2 3 => rw [TensorBimod.whiskerLeft_π_actLeft]

Premises used: Bimod.TensorBimod.whiskerLeft_π_actLeft
-- 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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
a : Iso.inv (α_ X.X M.X N₁.X) ≫ tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ◁ f.hom
| X.X ◁ M.X ◁ f.hom ≫ Iso.inv (α_ X.X M.X N₂.X)

Tactic:
rw [associator_inv_naturality_right]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
slice_rhs :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (Iso.inv (α_ X.X M.X N₁.X) ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one)
    (((Iso.inv (α_ X.X M.X N₁.X) ≫ tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ◁ f.hom) ≫ M.actLeft ▷ N₂.X) ≫
      coequalizer.π (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X N₁.X) ⟶ TensorBimod.X M N₂)
    (Iso.inv (α_ X.X M.X N₁.X) ≫
      M.actLeft ▷ N₁.X ≫
        M.X ◁ f.hom ≫
          colimit.ι (parallelPair (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))
            WalkingParallelPair.one)
    (X.X ◁ M.X ◁ f.hom ≫
      Iso.inv (α_ X.X M.X N₂.X) ≫
        M.actLeft ▷ N₂.X ≫ coequalizer.π (M.actRight ▷ N₂.X) (Iso.hom (α_ M.X Y.X N₂.X) ≫ M.X ◁ N₂.actLeft))

Tactic:
slice_rhs 1 2 => rw [associator_inv_naturality_right]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_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_1 : 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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N₁ N₂ : Bimod Y Z
f : N₁ ⟶ N₂
a : M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom
| tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ◁ f.hom ≫ M.actLeft ▷ N₂.X

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange