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)
⊢ 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))

Tactic:
monoidal
-- 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 : Bimod A B
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₁} (tensorRight X)
dsimp :
  P.actRight ▷ Q.X ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X
⊢ CategoryTheory.Functor.map (tensorRight T.X) (P.actRight ▷ Q.X) ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X

Tactic:
dsimp
-- 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 : Bimod A B
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₁} (tensorRight X)
a : Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫ P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X
| P.actRight ▷ Q.X ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X)

Tactic:
rw [associator_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
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₁} (tensorRight X)
slice_lhs :
  (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) ≫
      P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X
⊢ P.actRight ▷ Q.X ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X

Tactic:
slice_lhs 1 2 => rw [associator_naturality_left]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_left
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A B : Mon.{v₁, u₁} C
M : Bimod A B
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₁} (tensorRight X)
a : tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ Q.actRight ≫ P.actRight ▷ Q.X
| P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X ≫ P.X ◁ Q.actRight

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 : Bimod A B
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₁} (tensorRight X)
slice_lhs :
  Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ Q.actRight ≫ P.actRight ▷ Q.X =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X
⊢ (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        P.actRight ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X) ≫
      P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X

Tactic:
slice_lhs 2 3 => 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 : Bimod A B
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₁} (tensorRight X)
⊢ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X ◁ Q.actRight ≫ P.actRight ▷ Q.X =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      P.actRight ▷ Q.X

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 : Bimod A B
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₁} (tensorRight X)
dsimp :
  (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft
⊢ CategoryTheory.Functor.map (tensorRight T.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
      Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft

Tactic:
dsimp
-- 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 : Bimod A B
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₁} (tensorRight X)
simp :
  Iso.hom (α_ P.X S.X Q.X) ▷ T.X ≫
      Iso.hom (α_ P.X (tensorObj.{v₁, u₁} (𝒞 := inst) S.X Q.X) T.X) ≫ P.X ◁ Q.actLeft ▷ T.X ≫ P.X ◁ Q.actRight =
    Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫ P.X ◁ S.X ◁ Q.actRight ≫ P.X ◁ Q.actLeft
⊢ (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ Iso.hom (α_ P.X Q.X T.X) ≫ P.X ◁ Q.actRight =
    (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
        Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫
          P.X ◁ S.X ◁ Q.actRight ≫ Iso.inv (α_ P.X S.X Q.X)) ≫
      Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft

Tactic:
simp only [comp_whiskerRight, whisker_assoc, Category.assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whisker_assoc
-- 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 : Bimod A B
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₁} (tensorRight X)
a : P.X ◁ Iso.hom (α_ S.X Q.X T.X) ≫ P.X ◁ (S.X ◁ Q.actRight ≫ Q.actLeft)
| P.X ◁ Q.actLeft ▷ T.X ≫ P.X ◁ Q.actRight

Tactic:
rw [← whiskerLeft_comp, middle_assoc, whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, Bimod.middle_assoc
-- 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 : Bimod A B
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₁} (tensorRight X)
slice_lhs :
  Iso.hom (α_ P.X S.X Q.X) ▷ T.X ≫
      Iso.hom (α_ P.X (tensorObj.{v₁, u₁} (𝒞 := inst) S.X Q.X) T.X) ≫
        P.X ◁ Iso.hom (α_ S.X Q.X T.X) ≫ P.X ◁ (S.X ◁ Q.actRight ≫ Q.actLeft) =
    Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫ P.X ◁ S.X ◁ Q.actRight ≫ P.X ◁ Q.actLeft
⊢ Iso.hom (α_ P.X S.X Q.X) ▷ T.X ≫
      Iso.hom (α_ P.X (tensorObj.{v₁, u₁} (𝒞 := inst) S.X Q.X) T.X) ≫ P.X ◁ Q.actLeft ▷ T.X ≫ P.X ◁ Q.actRight =
    Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫ P.X ◁ S.X ◁ Q.actRight ≫ P.X ◁ Q.actLeft

Tactic:
slice_lhs 3 4 =>
            rw [← whiskerLeft_comp, middle_assoc, whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, Bimod.middle_assoc
-- 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 : Bimod A B
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₁} (tensorRight X)
⊢ Iso.hom (α_ P.X S.X Q.X) ▷ T.X ≫
      Iso.hom (α_ P.X (tensorObj.{v₁, u₁} (𝒞 := inst) S.X Q.X) T.X) ≫
        P.X ◁ Iso.hom (α_ S.X Q.X T.X) ≫ P.X ◁ (S.X ◁ Q.actRight ≫ Q.actLeft) =
    Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) P.X S.X) Q.X T.X) ≫
      Iso.hom (α_ P.X S.X (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X T.X)) ≫ P.X ◁ S.X ◁ Q.actRight ≫ 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
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₁} (tensorRight X)
erw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X ⟶ X P Q)
    ((Iso.hom (α_ P.X 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 (α_ P.X 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))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X ⟶ X P Q)
    (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ actRight P Q)
    (Iso.hom (α_ P.X 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:
erw [map_π_preserves_coequalizer_inv_colimMap (tensorRight _)]

Premises used: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap, CategoryTheory.MonoidalCategory.tensorRight
-- 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₁} (tensorRight X)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) T.X ⟶ X P Q)
    ((Iso.hom (α_ P.X 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 (α_ P.X 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 only [Category.assoc]

Premises used: CategoryTheory.Category.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₁} (tensorRight X)
⊢ X P Q ◁ η ≫ actRight P Q = Iso.hom (ρ_ (X P Q))

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

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Functor.map, CategoryTheory.MonoidalCategory.tensorRight, 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₁} (tensorRight X)
refine :
  Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      X P Q)
    (CategoryTheory.Functor.map (tensorRight (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
      X P Q ◁ η ≫ actRight P Q)
    (CategoryTheory.Functor.map (tensorRight (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft)) ≫
      Iso.hom (ρ_ (X P Q)))
⊢ X P Q ◁ η ≫ actRight P Q = Iso.hom (ρ_ (X P Q))

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

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

Tactic:
dsimp [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
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₁} (tensorRight X)
a :
  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) ▷ T.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) ◁ η

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

Tactic:
rw [π_tensor_id_actRight]

Premises used: Bimod.TensorBimod.π_tensor_id_actRight
-- 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₁} (tensorRight X)
slice_lhs :
  tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X ◁ η ≫
      Iso.hom (α_ P.X 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) =
    coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
      Iso.hom (ρ_ (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) P.X Q.X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
          T.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) ▷ T.X :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))
              T.X)
        (actRight P Q : tensorObj.{v₁, u₁} (𝒞 := inst) (X P Q) T.X ⟶ X P Q) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) (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) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
        Iso.hom (ρ_ (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) P.X Q.X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
        coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft))

Tactic:
slice_lhs 2 3 => rw [π_tensor_id_actRight]

Premises used: Bimod.TensorBimod.π_tensor_id_actRight