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 : Bimod X Y
N : Bimod Y Z
h :
  coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (whiskerRight (𝟙 M) N) =
    coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (𝟙 (M.tensorBimod N))
⊢ Hom.hom (whiskerRight (𝟙 M) N) = Hom.hom (𝟙 (M.tensorBimod N))

Tactic:
apply Limits.coequalizer.hom_ext

Premises used: CategoryTheory.Limits.coequalizer.hom_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
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 : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (whiskerRight (𝟙 M) N) =
    coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (𝟙 (M.tensorBimod N))

Tactic:
simp [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)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
h :
  Eq (α := (M.tensorBimod N).X ⟶ (M.tensorBimod Q).X) (Hom.hom (M.whiskerLeft (f ≫ g)))
    (Hom.hom (M.whiskerLeft f ≫ M.whiskerLeft g))
⊢ Eq (α := M.tensorBimod N ⟶ M.tensorBimod Q) (M.whiskerLeft (f ≫ g)) (M.whiskerLeft f ≫ M.whiskerLeft g)

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

Tactic:
apply Limits.coequalizer.hom_ext

Premises used: CategoryTheory.Limits.coequalizer.hom_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
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 P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X ⟶ (M.tensorBimod Q).X)
    (coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫ Hom.hom (M.whiskerLeft (f ≫ g)))
    (coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫
      Hom.hom (M.whiskerLeft f ≫ M.whiskerLeft g))

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)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
dsimp :
  Eq (α :=
    { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ : Bimod X X }.tensorBimod
        M ⟶
      { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ : Bimod X X }.tensorBimod
        N)
    ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ }.whiskerLeft
      f)
    (Iso.hom
        (isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯) ≫
      f ≫
        Iso.inv
          (isoOfIso
            { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ :
              TensorBimod.X
                  { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
                  N ≅
                N.X }
            ⋯ ⋯))
⊢ Eq (α := (regular X).tensorBimod M ⟶ (regular X).tensorBimod N) ((regular X).whiskerLeft f)
    (Iso.hom M.leftUnitorBimod ≫ f ≫ Iso.inv N.leftUnitorBimod)

Tactic:
dsimp [tensorHom, regular, leftUnitorBimod]

Premises used: Bimod.regular, Bimod.leftUnitorBimod, CategoryTheory.MonoidalCategoryStruct.tensorHom
-- 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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
h :
  Eq (α :=
    ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
              middle_assoc := ⋯ : Bimod X X }.tensorBimod
          M).X ⟶
      ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
              middle_assoc := ⋯ : Bimod X X }.tensorBimod
          N).X)
    (Hom.hom
      ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ }.whiskerLeft
        f))
    (Hom.hom
      (Iso.hom
          (isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯) ≫
        f ≫
          Iso.inv
            (isoOfIso
              { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ :
                TensorBimod.X
                    { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                      right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
                    N ≅
                  N.X }
              ⋯ ⋯)))
⊢ Eq (α :=
    { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ : Bimod X X }.tensorBimod
        M ⟶
      { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
            middle_assoc := ⋯ : Bimod X X }.tensorBimod
        N)
    ({ X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ }.whiskerLeft
      f)
    (Iso.hom
        (isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯) ≫
      f ≫
        Iso.inv
          (isoOfIso
            { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ :
              TensorBimod.X
                  { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
                  N ≅
                N.X }
            ⋯ ⋯))

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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
rw :
  X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one
| CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
    (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
    (colimMap
      (parallelPairHom (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft) (μ ▷ N.X)
        (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft) (tensorObj.{v₁, u₁} (𝒞 := inst) X.X X.X ◁ f.hom) (X.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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
        colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    (CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.desc M.actLeft ⋯ ≫ f.hom ≫ LeftUnitorBimod.inv N) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        TensorBimod.X
          { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
          N)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
        colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one :
      (parallelPair (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft)).obj WalkingParallelPair.one ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    (CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft) :
          tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶ coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (LeftUnitorBimod.hom M ≫ f.hom ≫ LeftUnitorBimod.inv N :
          TensorBimod.X
              { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
              M ⟶
            TensorBimod.X
              { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
              N) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        TensorBimod.X
          { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
          N)

Tactic:
dsimp [LeftUnitorBimod.hom]

Premises used: Bimod.LeftUnitorBimod.hom
-- 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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
a : M.actLeft
| CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
    (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft)) (coequalizer.desc M.actLeft ⋯)

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)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
        colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    ((M.actLeft ≫ f.hom) ≫ LeftUnitorBimod.inv N :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        TensorBimod.X
          { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
          N)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
        colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    (CategoryStruct.comp (Y := coequalizer (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.π (μ ▷ M.X) (Iso.hom (α_ X.X X.X M.X) ≫ X.X ◁ M.actLeft))
        (coequalizer.desc M.actLeft ⋯ ≫ f.hom ≫ LeftUnitorBimod.inv N) :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        TensorBimod.X
          { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
          N)

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)
X Y : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    ((M.actLeft ≫ f.hom) ≫
      Iso.inv (λ_ N.X) ≫ η ▷ N.X ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
        colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        colimit (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)))
    ((M.actLeft ≫ f.hom) ≫ LeftUnitorBimod.inv N :
      tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
        TensorBimod.X
          { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod X X }
          N)

Tactic:
dsimp [LeftUnitorBimod.inv]

Premises used: Bimod.LeftUnitorBimod.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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
a : X.X ◁ f.hom ≫ N.actLeft
| M.actLeft ≫ f.hom

Tactic:
rw [Hom.left_act_hom]

Premises used: 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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    ((((X.X ◁ f.hom ≫ N.actLeft) ≫ Iso.inv (λ_ N.X)) ≫ η ▷ N.X) ≫
      coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    ((M.actLeft ≫ f.hom) ≫
      Iso.inv (λ_ N.X) ≫ η ▷ N.X ≫ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))

Tactic:
slice_rhs 1 2 => rw [Hom.left_act_hom]

Premises used: 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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
a : Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft
| N.actLeft ≫ Iso.inv (λ_ N.X)

Tactic:
rw [leftUnitor_inv_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      ((Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft) ≫
          η ▷ N.X) ≫
        coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    ((((X.X ◁ f.hom ≫ N.actLeft) ≫ Iso.inv (λ_ N.X)) ≫ η ▷ N.X) ≫
      coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))

Tactic:
slice_rhs 2 3 => rw [leftUnitor_inv_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
a : η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫ X.X ◁ N.actLeft
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft ≫ η ▷ 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
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 : Mon.{v₁, u₁} C
M N : Bimod X Y
f : M ⟶ N
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫
        (η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X ≫ X.X ◁ N.actLeft) ≫
          coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) X.X M.X ⟶
      TensorBimod.X
        { X := X.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod X X }
        N)
    (X.X ◁ f.hom ≫
      colimit.ι (parallelPair (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one)
    (X.X ◁ f.hom ≫
      ((Iso.inv (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) X.X N.X)) ≫ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ N.actLeft) ≫
          η ▷ N.X) ≫
        coequalizer.π (μ ▷ N.X) (Iso.hom (α_ X.X X.X N.X) ≫ X.X ◁ N.actLeft))

Tactic:
slice_rhs 3 4 => rw [whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange