ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z X' Y' Z' : C<VAR>f g : X ⟶ Y<VAR>f' g' : X' ⟶ Y'<VAR>p : X ⊗ Z ⟶ X'<VAR>q : Y ⊗ Z ⟶ Y'<VAR>wf : f ▷ Z ≫ q = p ≫ f'<VAR>wg : g ▷ Z ≫ q = p ≫ g'<VAR>h : Y' ⟶ Z'<VAR>wh : f' ≫ h = g' ≫ h<GOAL>CategoryTheory.Limits.coequalizer.π f g ▷ Z ≫ (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv ≫ CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (f ▷ Z) (g ▷ Z) f' g' p q wf wg) ≫ CategoryTheory.Limits.coequalizer.desc h wh = q ≫ h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>self : Bimod A B<GOAL>self.X ◁ B.mul ≫ self.actRight = (α_ self.X B.X B.X).inv ≫ self.actRight ▷ B.X ≫ self.actRight
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>self : Bimod A B<GOAL>A.one ▷ self.X ≫ self.actLeft = (λ_ self.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>self : Bimod A B<GOAL>A.mul ▷ self.X ≫ self.actLeft = (α_ A.X A.X self.X).hom ≫ A.X ◁ self.actLeft ≫ self.actLeft
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>self : Bimod A B<GOAL>self.X ◁ B.one ≫ self.actRight = (ρ_ self.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>self : Bimod A B<GOAL>self.actLeft ▷ B.X ≫ self.actRight = (α_ A.X self.X B.X).hom ≫ A.X ◁ self.actRight ≫ self.actLeft
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>M N : Bimod A B<VAR>self : M.Hom N<GOAL>M.actLeft ≫ self.hom = A.X ◁ self.hom ≫ N.actLeft
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>M N : Bimod A B<VAR>self : M.Hom N<GOAL>M.actRight ≫ self.hom = self.hom ▷ B.X ≫ N.actRight
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<GOAL>M.id'.hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>M N O : Bimod A B<VAR>f : M.Hom N<VAR>g : N.Hom O<GOAL>(Bimod.comp f g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>M N : Bimod A B<VAR>f g : M ⟶ N<VAR>h : f.hom = g.hom<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<GOAL>(𝟙 M).hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : Mon_ C<VAR>M N K : Bimod A B<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>(f ≫ g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : Mon_ C<VAR>P Q : Bimod X Y<VAR>f : P.X ≅ Q.X<VAR>f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft<VAR>f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight<GOAL>(Bimod.isoOfIso f f_left_act_hom f_right_act_hom).inv.hom = f.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : Mon_ C<VAR>P Q : Bimod X Y<VAR>f : P.X ≅ Q.X<VAR>f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft<VAR>f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight<GOAL>(Bimod.isoOfIso f f_left_act_hom f_right_act_hom).hom.hom = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>(Bimod.regular A).X = A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>(Bimod.regular A).actRight = A.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ C<GOAL>(Bimod.regular A).actLeft = A.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<GOAL>R.X ◁ CategoryTheory.Limits.coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ Bimod.TensorBimod.actLeft P Q = (α_ R.X P.X Q.X).inv ≫ P.actLeft ▷ Q.X ≫ CategoryTheory.Limits.coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<GOAL>R.one ▷ Bimod.TensorBimod.X P Q ≫ Bimod.TensorBimod.actLeft P Q = (λ_ (Bimod.TensorBimod.X P Q)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<GOAL>R.mul ▷ Bimod.TensorBimod.X P Q ≫ Bimod.TensorBimod.actLeft P Q = (α_ R.X R.X (Bimod.TensorBimod.X P Q)).hom ≫ R.X ◁ Bimod.TensorBimod.actLeft P Q ≫ Bimod.TensorBimod.actLeft P Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>CategoryTheory.Limits.coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ≫ Bimod.TensorBimod.actRight P Q = (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ CategoryTheory.Limits.coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>Bimod.TensorBimod.X P Q ◁ T.one ≫ Bimod.TensorBimod.actRight P Q = (ρ_ (Bimod.TensorBimod.X P Q)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>Bimod.TensorBimod.X P Q ◁ T.mul ≫ Bimod.TensorBimod.actRight P Q = (α_ (Bimod.TensorBimod.X P Q) T.X T.X).inv ≫ Bimod.TensorBimod.actRight P Q ▷ T.X ≫ Bimod.TensorBimod.actRight P Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>Bimod.TensorBimod.actLeft P Q ▷ T.X ≫ Bimod.TensorBimod.actRight P Q = (α_ R.X (Bimod.TensorBimod.X P Q) T.X).hom ≫ R.X ◁ Bimod.TensorBimod.actRight P Q ≫ Bimod.TensorBimod.actLeft P Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>(M.tensorBimod N).actRight = Bimod.TensorBimod.actRight M N
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>(M.tensorBimod N).X = Bimod.TensorBimod.X M N
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>(M.tensorBimod N).actLeft = Bimod.TensorBimod.actLeft M N
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(M.whiskerLeft f).hom = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(Bimod.whiskerRight f N).hom = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>((P.tensorBimod Q).tensorBimod L).actLeft ≫ Bimod.AssociatorBimod.hom P Q L = R.X ◁ Bimod.AssociatorBimod.hom P Q L ≫ (P.tensorBimod (Q.tensorBimod L)).actLeft
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>((P.tensorBimod Q).tensorBimod L).actRight ≫ Bimod.AssociatorBimod.hom P Q L = Bimod.AssociatorBimod.hom P Q L ▷ U.X ≫ (P.tensorBimod (Q.tensorBimod L)).actRight
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>Bimod.AssociatorBimod.hom P Q L ≫ Bimod.AssociatorBimod.inv P Q L = 𝟙 ((P.tensorBimod Q).tensorBimod L).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>Bimod.AssociatorBimod.inv P Q L ≫ Bimod.AssociatorBimod.hom P Q L = 𝟙 (P.tensorBimod (Q.tensorBimod L)).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>Bimod.LeftUnitorBimod.hom P ≫ Bimod.LeftUnitorBimod.inv P = 𝟙 (Bimod.TensorBimod.X (Bimod.regular R) P)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>Bimod.LeftUnitorBimod.inv P ≫ Bimod.LeftUnitorBimod.hom P = 𝟙 P.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>((Bimod.regular R).tensorBimod P).actLeft ≫ Bimod.LeftUnitorBimod.hom P = R.X ◁ Bimod.LeftUnitorBimod.hom P ≫ P.actLeft
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>((Bimod.regular R).tensorBimod P).actRight ≫ Bimod.LeftUnitorBimod.hom P = Bimod.LeftUnitorBimod.hom P ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>Bimod.RightUnitorBimod.hom P ≫ Bimod.RightUnitorBimod.inv P = 𝟙 (Bimod.TensorBimod.X P (Bimod.regular S))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<GOAL>Bimod.RightUnitorBimod.inv P ≫ Bimod.RightUnitorBimod.hom P = 𝟙 P.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>(P.tensorBimod (Bimod.regular S)).actLeft ≫ Bimod.RightUnitorBimod.hom P = R.X ◁ Bimod.RightUnitorBimod.hom P ≫ P.actLeft
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<GOAL>(P.tensorBimod (Bimod.regular S)).actRight ≫ Bimod.RightUnitorBimod.hom P = Bimod.RightUnitorBimod.hom P ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>M.whiskerLeft (𝟙 N) = 𝟙 (M.tensorBimod N)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>Bimod.whiskerRight (𝟙 M) N = 𝟙 (M.tensorBimod N)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N P Q : Bimod Y Z<VAR>f : N ⟶ P<VAR>g : P ⟶ Q<GOAL>M.whiskerLeft (f ≫ g) = M.whiskerLeft f ≫ M.whiskerLeft g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>(Bimod.regular X).whiskerLeft f = M.leftUnitorBimod.hom ≫ f ≫ N.leftUnitorBimod.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>(M.tensorBimod N).whiskerLeft f = (M.associatorBimod N P).hom ≫ M.whiskerLeft (N.whiskerLeft f) ≫ (M.associatorBimod N P').inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N P : Bimod X Y<VAR>f : M ⟶ N<VAR>g : N ⟶ P<VAR>Q : Bimod Y Z<GOAL>Bimod.whiskerRight (f ≫ g) Q = Bimod.whiskerRight f Q ≫ Bimod.whiskerRight g Q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>Bimod.whiskerRight f (Bimod.regular Y) = M.rightUnitorBimod.hom ≫ f ≫ N.rightUnitorBimod.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.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>Bimod.whiskerRight f (N.tensorBimod P) = (M.associatorBimod N P).inv ≫ Bimod.whiskerRight (Bimod.whiskerRight f N) P ≫ (M'.associatorBimod N P).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N N' : Bimod X Y<VAR>f : N ⟶ N'<VAR>P : Bimod Y Z<GOAL>Bimod.whiskerRight (M.whiskerLeft f) P = (M.associatorBimod N P).hom ≫ M.whiskerLeft (Bimod.whiskerRight f P) ≫ (M.associatorBimod N' P).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M N : Bimod X Y<VAR>P Q : Bimod Y Z<VAR>f : M ⟶ N<VAR>g : P ⟶ Q<GOAL>M.whiskerLeft g ≫ Bimod.whiskerRight f Q = Bimod.whiskerRight f P ≫ N.whiskerLeft g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>Bimod.whiskerRight (M.associatorBimod N P).hom Q ≫ (M.associatorBimod (N.tensorBimod P) Q).hom ≫ M.whiskerLeft (N.associatorBimod P Q).hom = ((M.tensorBimod N).associatorBimod P Q).hom ≫ (M.associatorBimod N (P.tensorBimod Q)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.Limits.HasCoequalizers C<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)<VAR>(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)<VAR>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N : Bimod Y Z<GOAL>(M.associatorBimod (Bimod.regular Y) N).hom ≫ M.whiskerLeft N.leftUnitorBimod.hom = Bimod.whiskerRight M.rightUnitorBimod.hom N
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : MonovaryOn f g ↑s<GOAL>(∑ i ∈ s, f i) • ∑ i ∈ s, g i ≤ s.card • ∑ i ∈ s, f i • g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrderedRing α<VAR>LinearOrderedAddCommGroup β<VAR>Module α β<VAR>OrderedSMul α β<VAR>s : Finset ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<GOAL>s.card • ∑ i ∈ s, f i • g i ≤ (∑ i ∈ s, f i) • ∑ i ∈ s, g i