awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategoryArrow) X (tensorObj (𝒞 := instCategoryArrow) Y Z)).right ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).right)
    (Arrow.Hom.right
      (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y)))
    (Arrow.Hom.right (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
refine :
  Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.right) (tensorObj (𝒞 := instCategoryArrow) Y Z).left ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (Arrow.Hom.left
        (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow) X (tensorObj (𝒞 := instCategoryArrow) Y Z) ⟶
      tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y)
    (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))
    (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext ?_ (by simp)) (by simp)

Premises used: CategoryTheory.Arrow.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorLeft X.right) (obj.{v, v, u, u} (obj (curriedTensor C) Y.right) Z.left) ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
    (map (tensorLeft X.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left
          (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
    (map (tensorLeft X.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorLeft X.right) (obj.{v, v, u, u} (obj (curriedTensor C) Y.left) Z.right) ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
    (map (tensorLeft X.right)
        (pushout.inr (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left
          (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
    (map (tensorLeft X.right)
        (pushout.inr (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))

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)
W X Y Z : C
f g : X ⟶ Y
h : tensorObj.{v₁, u₁} (𝒞 := inst) Z Y ⟶ W
wh : Z ◁ f ≫ h = Z ◁ g ≫ h
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Z (coequalizer f g)) (Z ◁ coequalizer.π f g)
      (CategoryStruct.comp (Y :=
        coequalizer (X := Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft Z) X) (CategoryTheory.Functor.map (tensorLeft Z) f)
          (CategoryTheory.Functor.map (tensorLeft Z) g))
        (Iso.inv (PreservesCoequalizer.iso (tensorLeft Z) f g)) (coequalizer.desc h wh)) =
    h

Tactic:
map_π_preserves_coequalizer_inv_desc (tensorLeft Z) f g h wh

Premises used: CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_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)
X Y Z X' Y' Z' : C
f g : X ⟶ Y
f' g' : X' ⟶ Y'
p : tensorObj.{v₁, u₁} (𝒞 := inst) Z X ⟶ X'
q : tensorObj.{v₁, u₁} (𝒞 := inst) Z Y ⟶ Y'
wf : Z ◁ f ≫ q = p ≫ f'
wg : Z ◁ g ≫ q = p ≫ g'
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) Z (coequalizer f g)) (Z ◁ coequalizer.π f g)
      (CategoryStruct.comp (Y :=
        coequalizer (X := Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft Z) X) (CategoryTheory.Functor.map (tensorLeft Z) f)
          (CategoryTheory.Functor.map (tensorLeft Z) g))
        (Iso.inv (PreservesCoequalizer.iso (tensorLeft Z) f g))
        (CategoryStruct.comp (Y := colimit (parallelPair f' g'))
          (colimMap (parallelPairHom (Z ◁ f) (Z ◁ g) f' g' p q wf wg)) (coequalizer.desc h wh))) =
    q ≫ h

Tactic:
map_π_preserves_coequalizer_inv_colimMap_desc (tensorLeft Z) f g f' g' p q wf wg h wh

Premises used: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.MonoidalCategory.tensorLeft
-- 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₁} (tensorRight X)
W X Y Z : C
f g : X ⟶ Y
h : tensorObj.{v₁, u₁} (𝒞 := inst) Y Z ⟶ W
wh : f ▷ Z ≫ h = g ▷ Z ≫ h
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer f g) Z) (coequalizer.π f g ▷ Z)
      (CategoryStruct.comp (Y :=
        coequalizer (X := Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight Z) X) (CategoryTheory.Functor.map (tensorRight Z) f)
          (CategoryTheory.Functor.map (tensorRight Z) g))
        (Iso.inv (PreservesCoequalizer.iso (tensorRight Z) f g)) (coequalizer.desc h wh)) =
    h

Tactic:
map_π_preserves_coequalizer_inv_desc (tensorRight Z) f g h wh

Premises used: CategoryTheory.MonoidalCategory.tensorRight, CategoryTheory.Limits.map_π_preserves_coequalizer_inv_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₁} (tensorRight X)
X Y Z X' Y' Z' : C
f g : X ⟶ Y
f' g' : X' ⟶ Y'
p : tensorObj.{v₁, u₁} (𝒞 := inst) X Z ⟶ X'
q : tensorObj.{v₁, u₁} (𝒞 := inst) Y Z ⟶ Y'
wf : f ▷ Z ≫ q = p ≫ f'
wg : g ▷ Z ≫ q = p ≫ g'
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer f g) Z) (coequalizer.π f g ▷ Z)
      (CategoryStruct.comp (Y :=
        coequalizer (X := Functor.obj.{v₁, v₁, u₁, u₁} (tensorRight Z) X) (CategoryTheory.Functor.map (tensorRight Z) f)
          (CategoryTheory.Functor.map (tensorRight Z) g))
        (Iso.inv (PreservesCoequalizer.iso (tensorRight Z) f g))
        (CategoryStruct.comp (Y := colimit (parallelPair f' g'))
          (colimMap (parallelPairHom (f ▷ Z) (g ▷ Z) f' g' p q wf wg)) (coequalizer.desc h wh))) =
    q ≫ h

Tactic:
map_π_preserves_coequalizer_inv_colimMap_desc (tensorRight Z) f g f' g' p q wf wg h wh

Premises used: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc, CategoryTheory.MonoidalCategory.tensorRight
-- 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 N : Bimod A B
f g : M ⟶ N
h : f.hom = g.hom
⊢ f = g

Tactic:
Hom.ext h

Premises used: Bimod.Hom.ext
-- 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
⊢ Hom.hom (𝟙 M) = 𝟙 M.X

Tactic:
rfl

Premises used: rfl
-- 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 N K : Bimod A B
f : M ⟶ N
g : N ⟶ K
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- 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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actLeft ≫ f.inv) ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₁ : Q.actLeft ≫ f.inv ≫ f.hom = (X.X ◁ f.inv ≫ P.actLeft) ≫ f.hom
rw₂ : Q.actLeft ≫ f.inv ≫ f.hom = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₃ : Q.actLeft ≫ 𝟙 Q.X = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₄ : Q.actLeft = X.X ◁ f.inv ≫ P.actLeft ≫ f.hom
rw₅ : Q.actLeft = X.X ◁ f.inv ≫ X.X ◁ f.hom ≫ Q.actLeft
rw₆ : Q.actLeft = (X.X ◁ f.inv ≫ X.X ◁ f.hom) ≫ Q.actLeft
rw₇ : Q.actLeft = X.X ◁ (f.inv ≫ f.hom) ≫ Q.actLeft
rw₈ : Q.actLeft = X.X ◁ 𝟙 Q.X ≫ Q.actLeft
rw₉ : Q.actLeft = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X Q.X) ≫ Q.actLeft
rw₁₀ rw₁₁ : Q.actLeft = Q.actLeft
⊢ Q.actLeft ≫ f.inv = X.X ◁ f.inv ≫ P.actLeft

Tactic:
rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_left_act_hom, ← Category.assoc, ← whiskerLeft_comp, Iso.inv_hom_id,
          whiskerLeft_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- 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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
rw : (Q.actRight ≫ f.inv) ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₁ : Q.actRight ≫ f.inv ≫ f.hom = (f.inv ▷ Y.X ≫ P.actRight) ≫ f.hom
rw₂ : Q.actRight ≫ f.inv ≫ f.hom = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₃ : Q.actRight ≫ 𝟙 Q.X = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₄ : Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom
rw₅ : Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight
rw₆ : Q.actRight = (f.inv ▷ Y.X ≫ f.hom ▷ Y.X) ≫ Q.actRight
rw₇ : Q.actRight = (f.inv ≫ f.hom) ▷ Y.X ≫ Q.actRight
rw₈ : Q.actRight = 𝟙 Q.X ▷ Y.X ≫ Q.actRight
rw₉ : Q.actRight = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) Q.X Y.X) ≫ Q.actRight
rw₁₀ rw₁₁ : Q.actRight = Q.actRight
⊢ Q.actRight ≫ f.inv = f.inv ▷ Y.X ≫ P.actRight

Tactic:
rw [← cancel_mono f.hom, Category.assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id,
          f_right_act_hom, ← Category.assoc, ← comp_whiskerRight, Iso.inv_hom_id,
          id_whiskerRight, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Iso.hom, CategoryTheory.Category.id_comp
-- 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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
h :
  Hom.hom
      ({ hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ : P.Hom Q } ≫
        { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ }) =
    Hom.hom (𝟙 P)
⊢ { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ : P.Hom Q } ≫
      { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ } =
    𝟙 P

Tactic:
ext
-- 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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
h : f.hom ≫ f.inv = 𝟙 P.X
⊢ Hom.hom
      ({ hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ : P.Hom Q } ≫
        { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ }) =
    Hom.hom (𝟙 P)

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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
h h₁ : Eq.{v₁ + 1} (α := P.X ⟶ P.X) (𝟙 P.X) (𝟙 P.X)
⊢ f.hom ≫ f.inv = 𝟙 P.X

Tactic:
rw [Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- 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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
h :
  Hom.hom
      ({ hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ : Q.Hom P } ≫
        { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ }) =
    Hom.hom (𝟙 Q)
⊢ { hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ : Q.Hom P } ≫
      { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ } =
    𝟙 Q

Tactic:
ext
-- 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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
h : f.inv ≫ f.hom = 𝟙 Q.X
⊢ Hom.hom
      ({ hom := f.inv, left_act_hom := ⋯, right_act_hom := ⋯ : Q.Hom P } ≫
        { hom := f.hom, left_act_hom := ⋯, right_act_hom := ⋯ }) =
    Hom.hom (𝟙 Q)

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
X Y : Mon.{v₁, u₁} C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
h h₁ : Eq.{v₁ + 1} (α := Q.X ⟶ Q.X) (𝟙 Q.X) (𝟙 Q.X)
⊢ f.inv ≫ f.hom = 𝟙 Q.X

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- 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)
erw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶ X P Q)
    ((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))
    (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) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶ X P Q)
    (R.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X S.X Q.X) ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q)
    (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:
erw [map_π_preserves_coequalizer_inv_colimMap (tensorLeft _)]

Premises used: CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap, CategoryTheory.MonoidalCategory.tensorLeft
-- 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) R.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶ X P Q)
    ((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))
    (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:
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₁} (tensorLeft X)
⊢ η ▷ X P Q ≫ actLeft P Q = Iso.hom (λ_ (X 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 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      X P Q)
    (CategoryTheory.Functor.map (tensorLeft (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 ≫ actLeft P Q)
    (CategoryTheory.Functor.map (tensorLeft (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 ≫ actLeft P Q = Iso.hom (λ_ (X 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)
dsimp :
  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)))
⊢ Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (tensorLeft (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X) ⟶
      X P Q)
    (CategoryTheory.Functor.map (tensorLeft (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 ≫ actLeft P Q)
    (CategoryTheory.Functor.map (tensorLeft (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