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

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

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

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

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

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

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 (α :=
    M.tensorBimod
        { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod Y Y } ⟶
      N.tensorBimod
        { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ })
    (whiskerRight f
      { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
        middle_assoc := ⋯ })
    (Iso.hom
        (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯) ≫
      f ≫
        Iso.inv
          (isoOfIso
            { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ :
              TensorBimod.X N
                  { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
                    right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y } ≅
                N.X }
            ⋯ ⋯))
⊢ Eq (α := M.tensorBimod (regular Y) ⟶ N.tensorBimod (regular Y)) (whiskerRight f (regular Y))
    (Iso.hom M.rightUnitorBimod ≫ f ≫ Iso.inv N.rightUnitorBimod)

Tactic:
dsimp [tensorHom, regular, rightUnitorBimod]

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

Tactic:
dsimp [RightUnitorBimod.hom]

Premises used: Bimod.RightUnitorBimod.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.actRight
| CategoryStruct.comp (Y := coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ))
    (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) (coequalizer.desc M.actRight ⋯)

Tactic:
rw [coequalizer.π_desc]

Premises used: CategoryTheory.Limits.coequalizer.π_desc
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
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) M.X Y.X ⟶
      TensorBimod.X N
        { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod Y Y })
    (f.hom ▷ Y.X ≫
        colimit.ι (parallelPair (N.actRight ▷ Y.X) (Iso.hom (α_ N.X Y.X Y.X) ≫ N.X ◁ μ)) WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ⟶
        colimit (parallelPair (N.actRight ▷ Y.X) (Iso.hom (α_ N.X Y.X Y.X) ≫ N.X ◁ μ)))
    ((M.actRight ≫ f.hom) ≫ RightUnitorBimod.inv N :
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ⟶
        TensorBimod.X N
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y })
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ⟶
      TensorBimod.X N
        { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ : Bimod Y Y })
    (f.hom ▷ Y.X ≫
        colimit.ι (parallelPair (N.actRight ▷ Y.X) (Iso.hom (α_ N.X Y.X Y.X) ≫ N.X ◁ μ)) WalkingParallelPair.one :
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ⟶
        colimit (parallelPair (N.actRight ▷ Y.X) (Iso.hom (α_ N.X Y.X Y.X) ≫ N.X ◁ μ)))
    (CategoryStruct.comp (Y := coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ))
        (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ))
        (coequalizer.desc M.actRight ⋯ ≫ f.hom ≫ RightUnitorBimod.inv N) :
      tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X ⟶
        TensorBimod.X N
          { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯,
            right_assoc := ⋯, middle_assoc := ⋯ : Bimod Y Y })

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

Tactic:
dsimp [RightUnitorBimod.inv]

Premises used: Bimod.RightUnitorBimod.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
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 : f.hom ▷ Y.X ≫ N.actRight
| M.actRight ≫ f.hom

Tactic:
rw [Hom.right_act_hom]

Premises used: Bimod.Hom.right_act_hom