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

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
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)
slice_lhs :
  CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
          R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
⊢ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      η ▷ coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.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
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)
a :
  Iso.inv (α_ R.X P.X Q.X) ≫
    P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) :
    tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))

Tactic:
rw [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
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)
slice_lhs :
  η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
      Iso.inv (α_ R.X P.X Q.X) ≫
        P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
          R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
      (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))

Tactic:
slice_lhs 2 3 => rw [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
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)
a : Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫ η ▷ P.X ▷ Q.X
| η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫ Iso.inv (α_ R.X P.X Q.X)

Tactic:
rw [associator_inv_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
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)
slice_lhs :
  ((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫ η ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
⊢ η ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫
      Iso.inv (α_ R.X P.X Q.X) ≫
        P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))

Tactic:
slice_lhs 1 2 => rw [associator_inv_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
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)
a : Iso.hom (λ_ P.X) ▷ Q.X
| η ▷ P.X ▷ Q.X ≫ P.actLeft ▷ Q.X

Tactic:
rw [← comp_whiskerRight, one_actLeft]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, Bimod.one_actLeft
-- 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)
slice_lhs :
  Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫
      Iso.hom (λ_ P.X) ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
⊢ ((Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫ η ▷ P.X ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))

Tactic:
slice_lhs 2 3 => rw [← comp_whiskerRight, one_actLeft]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, Bimod.one_actLeft
-- 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)
rw :
  Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
| tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))

Tactic:
rw [leftUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_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
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)
slice_rhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫
      Iso.hom (λ_ P.X) ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
⊢ Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫
      Iso.hom (λ_ P.X) ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) =
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (λ_ (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))

Tactic:
slice_rhs 1 2 => rw [leftUnitor_naturality]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_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
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)
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) P.X Q.X) ≫
      Iso.hom (λ_ P.X) ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (λ_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))

Tactic:
monoidal
-- 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)
⊢ μ ▷ X P Q ≫ actLeft P Q = Iso.hom (α_ R.X R.X (X P Q)) ≫ R.X ◁ actLeft P Q ≫ actLeft P Q

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
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)
refine :
  Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X))
        (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      X P Q)
    (CategoryTheory.Functor.map (tensorLeft (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X))
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
      μ ▷ X P Q ≫ actLeft P Q)
    (CategoryTheory.Functor.map (tensorLeft (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X))
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
      Iso.hom (α_ R.X R.X (X P Q)) ≫ R.X ◁ actLeft P Q ≫ actLeft P Q)
⊢ μ ▷ X P Q ≫ actLeft P Q = Iso.hom (α_ R.X R.X (X P Q)) ≫ R.X ◁ actLeft P Q ≫ actLeft P Q

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

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
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)
a : Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫ μ ▷ P.X ▷ Q.X
| μ ▷ tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ≫ Iso.inv (α_ R.X P.X Q.X)

Tactic:
rw [associator_inv_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
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)
a : Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X
| μ ▷ P.X ▷ Q.X ≫ P.actLeft ▷ Q.X

Tactic:
rw [← comp_whiskerRight, left_assoc, comp_whiskerRight, comp_whiskerRight]

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

Tactic:
rw [associator_naturality_right]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_right
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
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)
a :
  R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
    R.X ◁ P.actLeft ▷ Q.X ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X
        (tensorObj.{v₁, u₁} (𝒞 := inst) R.X
          (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))))
      (R.X ◁ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
        tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) R.X
              (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))))
      (R.X ◁ actLeft P Q :
        tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (tensorObj.{v₁, u₁} (𝒞 := inst) R.X
              (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))) ⟶
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))) :
    tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) R.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))

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

Premises used: Bimod.TensorBimod.whiskerLeft_π_actLeft, CategoryTheory.MonoidalCategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
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)
slice_rhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
      (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
      R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
        R.X ◁ P.actLeft ▷ Q.X ≫
          Iso.inv (α_ R.X P.X Q.X) ≫
            P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
        (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
          coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
        coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) R.X
            (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
          (R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
              R.X ◁ P.actLeft ▷ Q.X ≫
                R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) :
            tensorObj.{v₁, u₁} (𝒞 := inst) R.X
                (tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ⟶
              tensorObj.{v₁, u₁} (𝒞 := inst) R.X
                (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)))
          (actLeft P Q : tensorObj.{v₁, u₁} (𝒞 := inst) R.X (X P Q) ⟶ X P Q) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
        coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))

Tactic:
slice_rhs 4 5 => rw [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
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)
a : Iso.inv (α_ R.X (tensorObj.{v₁, u₁} (𝒞 := inst) R.X P.X) Q.X) ≫ (R.X ◁ P.actLeft) ▷ Q.X
| R.X ◁ P.actLeft ▷ Q.X ≫ Iso.inv (α_ R.X P.X Q.X)

Tactic:
rw [associator_inv_naturality_middle]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_middle
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
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)
slice_rhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
      (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
      R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
        ((Iso.inv (α_ R.X (tensorObj.{v₁, u₁} (𝒞 := inst) R.X P.X) Q.X) ≫ (R.X ◁ P.actLeft) ▷ Q.X) ≫ P.actLeft ▷ Q.X) ≫
          coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) R.X R.X) P.X Q.X) ≫
      (Iso.hom (α_ R.X R.X P.X) ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (Iso.hom (α_ R.X R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
      R.X ◁ Iso.inv (α_ R.X P.X Q.X) ≫
        R.X ◁ P.actLeft ▷ Q.X ≫
          Iso.inv (α_ R.X P.X Q.X) ≫
            P.actLeft ▷ Q.X ≫ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))

Tactic:
slice_rhs 3 4 => rw [associator_inv_naturality_middle]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality_middle