ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>f.hom ▷ TensorBimod.X N P ≫ colimit.ι (parallelPair (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) ≫ AssociatorBimod.inv M N P ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (TensorBimod.X M' N) Y.X P.X).hom ≫ TensorBimod.X M' N ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯) ≫ AssociatorBimod.hom M' N P
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P) ≫ coequalizer.desc (AssociatorBimod.invAux M N P) ⋯ ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯) ≫ AssociatorBimod.hom M' N P
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (AssociatorBimod.invAux M N P ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯)) ≫ AssociatorBimod.hom M' N P
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (((PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X P.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft)) ⋯) ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯)) ≫ coequalizer.desc (AssociatorBimod.homAux M' N P) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>(tensorLeft M.X).map (coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (tensorLeft M.X).map (coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ≫ (((PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X P.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft)) ⋯) ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯)) ≫ coequalizer.desc (AssociatorBimod.homAux M' N P) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ (((PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X P.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft)) ⋯) ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯)) ≫ coequalizer.desc (AssociatorBimod.homAux M' N P) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (((α_ M.X N.X P.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft)) ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯)) ≫ coequalizer.desc (AssociatorBimod.homAux M' N P) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (α_ M.X N.X P.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X ≫ colimit.ι (parallelPair (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft)) WalkingParallelPair.one) ≫ coequalizer.desc (AssociatorBimod.homAux M' N P) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (α_ M.X N.X P.X).inv ≫ ((f.hom ▷ N.X ≫ colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) WalkingParallelPair.one) ▷ P.X ≫ colimit.ι (parallelPair (TensorBimod.actRight M' N ▷ P.X) ((α_ (coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) Y.X P.X).hom ≫ coequalizer (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) ◁ P.actLeft)) WalkingParallelPair.one) ≫ coequalizer.desc (AssociatorBimod.homAux M' N P) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (α_ M.X N.X P.X).inv ≫ (f.hom ▷ N.X ≫ colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) WalkingParallelPair.one) ▷ P.X ≫ AssociatorBimod.homAux M' N P
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (α_ M.X N.X P.X).inv ≫ (f.hom ▷ N.X ≫ colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) WalkingParallelPair.one) ▷ P.X ≫ (PreservesCoequalizer.iso (tensorRight P.X) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M'.X N.X P.X).hom ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (α_ M.X N.X P.X).inv ≫ ((f.hom ▷ N.X ▷ P.X ≫ colimit.ι (parallelPair (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)) WalkingParallelPair.one ▷ P.X) ≫ (PreservesCoequalizer.iso (tensorRight P.X) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft)).inv) ≫ coequalizer.desc ((α_ M'.X N.X P.X).hom ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (α_ M.X N.X P.X).inv ≫ f.hom ▷ N.X ▷ P.X ≫ (α_ M'.X N.X P.X).hom ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (α_ M.X N.X P.X).inv ≫ (((α_ M.X N.X P.X).hom ≫ f.hom ▷ (N.X ⊗ P.X)) ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ≫ coequalizer.π (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ f.hom ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (f.hom ▷ (N.X ⊗ P.X) ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ≫ coequalizer.π (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>(f.hom ▷ (N.X ⊗ P.X) ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ≫ colimit.ι (parallelPair (M'.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M'.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M'.X ◁ TensorBimod.actLeft N P)) WalkingParallelPair.one = (f.hom ▷ (N.X ⊗ P.X) ≫ M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ≫ coequalizer.π (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)