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)
V W X Y Z : Mon.{v₁, u₁} C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
a :
  Iso.hom (α_ M.X N.X (tensorObj.{v₁, u₁} (𝒞 := inst) P.X Q.X)) ≫
    M.X ◁ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft)
| tensorObj.{v₁, u₁} (𝒞 := inst) M.X N.X ◁
      coequalizer.π (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.X Q.X) ≫ P.X ◁ Q.actLeft) ≫
    Iso.hom (α_ M.X N.X (coequalizer (P.actRight ▷ Q.X) (Iso.hom (α_ P.X Y.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
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
dsimp :
  Eq (α := (M.tensorBimod (regular Y)).tensorBimod N ⟶ M.tensorBimod N)
    (Iso.hom
        (isoOfIso
          { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
            inv_hom_id := ⋯ :
            TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
          ⋯ ⋯) ≫
      M.whiskerLeft
        (Iso.hom
          (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯)))
    (whiskerRight
      (Iso.hom
        (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯))
      N)
⊢ Eq (α := (M.tensorBimod (regular Y)).tensorBimod N ⟶ M.tensorBimod N)
    (Iso.hom (M.associatorBimod (regular Y) N) ≫ M.whiskerLeft (Iso.hom N.leftUnitorBimod))
    (whiskerRight (Iso.hom M.rightUnitorBimod) N)

Tactic:
dsimp [associatorBimod, leftUnitorBimod, rightUnitorBimod]

Premises used: Bimod.leftUnitorBimod, Bimod.associatorBimod, Bimod.rightUnitorBimod
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
h :
  Eq (α := ((M.tensorBimod (regular Y)).tensorBimod N).X ⟶ (M.tensorBimod N).X)
    (Hom.hom
      (Iso.hom
          (isoOfIso
            { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
              inv_hom_id := ⋯ :
              TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
            ⋯ ⋯) ≫
        M.whiskerLeft
          (Iso.hom
            (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯))))
    (Hom.hom
      (whiskerRight
        (Iso.hom
          (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯))
        N))
⊢ Eq (α := (M.tensorBimod (regular Y)).tensorBimod N ⟶ M.tensorBimod N)
    (Iso.hom
        (isoOfIso
          { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
            inv_hom_id := ⋯ :
            TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
          ⋯ ⋯) ≫
      M.whiskerLeft
        (Iso.hom
          (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯)))
    (whiskerRight
      (Iso.hom
        (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯))
      N)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
h :
  coequalizer.π ((M.tensorBimod (regular Y)).actRight ▷ N.X)
        (Iso.hom (α_ (M.tensorBimod (regular Y)).X Y.X N.X) ≫ (M.tensorBimod (regular Y)).X ◁ N.actLeft) ≫
      Hom.hom
        (Iso.hom
            (isoOfIso
              { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
                inv_hom_id := ⋯ :
                TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
              ⋯ ⋯) ≫
          M.whiskerLeft
            (Iso.hom
              (isoOfIso
                { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ :
                  TensorBimod.X (regular Y) N ≅ N.X }
                ⋯ ⋯))) =
    coequalizer.π ((M.tensorBimod (regular Y)).actRight ▷ N.X)
        (Iso.hom (α_ (M.tensorBimod (regular Y)).X Y.X N.X) ≫ (M.tensorBimod (regular Y)).X ◁ N.actLeft) ≫
      Hom.hom
        (whiskerRight
          (Iso.hom
            (isoOfIso
              { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ :
                TensorBimod.X M (regular Y) ≅ M.X }
              ⋯ ⋯))
          N)
⊢ Eq (α := ((M.tensorBimod (regular Y)).tensorBimod N).X ⟶ (M.tensorBimod N).X)
    (Hom.hom
      (Iso.hom
          (isoOfIso
            { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
              inv_hom_id := ⋯ :
              TensorBimod.X (M.tensorBimod (regular Y)) N ≅ TensorBimod.X M ((regular Y).tensorBimod N) }
            ⋯ ⋯) ≫
        M.whiskerLeft
          (Iso.hom
            (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯))))
    (Hom.hom
      (whiskerRight
        (Iso.hom
          (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯))
        N))

Tactic:
apply coequalizer.hom_ext

Premises used: CategoryTheory.Limits.coequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
a : AssociatorBimod.homAux M (regular Y) N
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (coequalizer.desc (AssociatorBimod.homAux M (regular Y) N) ⋯)

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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
rw :
  RightUnitorBimod.hom M ▷ N.X ≫
    colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one
| CategoryStruct.comp (Y :=
    coequalizer (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
      (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft))
    (colimMap
      (parallelPairHom (TensorBimod.actRight M (regular Y) ▷ N.X)
        (Iso.hom (α_ (TensorBimod.X M (regular Y)) Y.X N.X) ≫ TensorBimod.X M (regular Y) ◁ N.actLeft)
        (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) (RightUnitorBimod.hom M ▷ Y.X ▷ N.X)
        (RightUnitorBimod.hom M ▷ N.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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
a : M.X ◁ N.actLeft
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
    (M.X ◁ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)) (M.X ◁ coequalizer.desc N.actLeft ⋯)

Tactic:
rw [← whiskerLeft_comp, coequalizer.π_desc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, 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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
      (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
      (coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) M.X (coequalizer (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft)))
        (M.X ◁ coequalizer.π (μ ▷ N.X) (Iso.hom (α_ Y.X Y.X N.X) ≫ Y.X ◁ N.actLeft))
        (M.X ◁ coequalizer.desc N.actLeft ⋯ ≫
          colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
            WalkingParallelPair.one))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
      (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
      (coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one))

Tactic:
slice_lhs 2 3 => rw [← whiskerLeft_comp, coequalizer.π_desc]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, 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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
a : M.actRight ▷ N.X
| CategoryStruct.comp (Y :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
    (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X) (coequalizer.desc M.actRight ⋯ ▷ N.X)

Tactic:
rw [← comp_whiskerRight, coequalizer.π_desc]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, 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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    (M.actRight ▷ N.X ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (coequalizer (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ)) N.X)
      (coequalizer.π (M.actRight ▷ Y.X) (Iso.hom (α_ M.X Y.X Y.X) ≫ M.X ◁ μ) ▷ N.X)
      (coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one))

Tactic:
slice_rhs 1 2 => rw [← comp_whiskerRight, coequalizer.π_desc]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, 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 Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
rw :
  (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫
    coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)
| M.actRight ▷ N.X ≫
    colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one

Tactic:
rw [coequalizer.condition]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
h :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    ((Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫
      coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    (M.actRight ▷ N.X ≫
      colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one)

Tactic:
slice_rhs 1 2 => rw [coequalizer.condition]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Monoidal.Bimod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : HasCoequalizers.{v₁, u₁} C
inst_3 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst_4 : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon.{v₁, u₁} C
M : Bimod X Y
N : Bimod Y Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X Y.X) N.X ⟶ TensorBimod.X M N)
    (Iso.hom (α_ M.X Y.X N.X) ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))
          WalkingParallelPair.one)
    ((Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft) ≫
      coequalizer.π (M.actRight ▷ N.X) (Iso.hom (α_ M.X Y.X N.X) ≫ M.X ◁ N.actLeft))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Bimon.{v₁, u₁} C
f g : X ⟶ Y
w : f.hom.hom = g.hom.hom
⊢ f = g

Tactic:
Comon.Hom.ext (Mon.Hom.ext w)

Premises used: CategoryTheory.Mon.Hom.ext, CategoryTheory.Comon.Hom.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Comon.Hom.hom (𝟙 M) = 𝟙 M.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M N K : Bimon.{v₁, u₁} C
f : M ⟶ N
g : N ⟶ K
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq (α := Bimon.{v₁, u₁} C ⥤ C) (toMon C ⋙ Mon.forget C) (forget C)

Tactic:
rfl

Premises used: CategoryTheory.Bimon.forget, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq (α := Bimon.{v₁, u₁} C ⥤ C) (toComon C ⋙ Comon.forget C) (forget C)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Comon.forget, CategoryTheory.Bimon.toComon, CategoryTheory.Bimon.forget, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj (𝒞 := Comon.instCategory) (Functor.obj (toComon C) M) (Functor.obj (toComon C) M)).X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (toComon C) M).X (Functor.obj (toComon C) M).X)
    (μ ≫ Δ) (Δ ≫ (μ ⊗ₘ μ))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Mon (Comon.{v₁, u₁} C)
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (ofMonComonObjX M).X) η
    (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ Comon.Hom.hom η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Mon (Comon.{v₁, u₁} C)
⊢ μ = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) ≫ Comon.Hom.hom μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (Functor.obj (toMonComon C ⋙ ofMonComon C) M).X.X) η
    (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ η)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ μ = 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) ≫ μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Mon (Comon.{v₁, u₁} C)
⊢ Eq (α := (Functor.obj (ofMonComon C ⋙ toMonComon C) M).X.X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε
    (ε ≫ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Mon (Comon.{v₁, u₁} C)
⊢ Δ = Δ ≫ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := (Functor.obj (toComon C) M).X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε (Mon.Hom.hom ε)

Tactic:
Category.comp_id _

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    (Functor.obj (toComon C) M).X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (toComon C) M).X (Functor.obj (toComon C) M).X)
    Δ (Mon.Hom.hom Δ)

Tactic:
Category.comp_id _

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
rw :
  Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (ε ▷ M.X.X))
    (Iso.inv (λ_ M.X.X))
rw₁ :
  Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X) (Δ ≫ ε ▷ M.X.X)
    (Iso.inv (λ_ M.X.X))
rw₂ rw₃ :
  Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (Iso.inv (λ_ M.X.X)) (Iso.inv (λ_ M.X.X))
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M.X.X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (Mon.Hom.hom ε ▷ M.X.X))
    (Iso.inv (λ_ M.X.X))

Tactic:
rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.counit_comul]

Premises used: CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.ComonObj.counit_comul