Loogle!

Result

Found 89 declarations mentioning CategoryTheory.Limits.HasCoequalizers.

• CategoryTheory.Limits.HasCoequalizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
• CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair 📋 Mathlib.CategoryTheory.Limits.Shapes.Equalizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)] : CategoryTheory.Limits.HasCoequalizers C
• CategoryTheory.Limits.hasCokernels_of_hasCoequalizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Kernels
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasCokernels C
• CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCokernels C] : CategoryTheory.Limits.HasCoequalizers C
• ModuleCat.instHasCoequalizers 📋 Mathlib.Algebra.Category.ModuleCat.Colimits
  (R : Type w) [Ring R] : CategoryTheory.Limits.HasCoequalizers (ModuleCat R)
• CategoryTheory.Limits.hasCoequalizers_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C] : CategoryTheory.Limits.HasCoequalizers Cᵒᵖ
• CategoryTheory.Limits.hasEqualizers_opposite 📋 Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasEqualizers Cᵒᵖ
• CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.Equalizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Limits.HasCoequalizers C
• CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasFiniteColimits C
• CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C
• CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasFiniteCoproducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesFiniteCoproducts G] : CategoryTheory.Limits.PreservesFiniteColimits G
• CategoryTheory.Limits.preservesColimits_of_preservesCoequalizers_and_coproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasCoproducts C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, v, v₂, u, u₂} G
• CategoryTheory.Limits.createsFiniteColimitsOfCreatesCoequalizersAndFiniteCoproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasFiniteCoproducts D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.CreatesFiniteCoproducts G] : CategoryTheory.Limits.CreatesFiniteColimits G
• CategoryTheory.Limits.createsColimitsOfSizeOfCreatesCoequalizersAndCoproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Limits.HasCoproducts D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [(J : Type w) → CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) G] : CategoryTheory.CreatesColimitsOfSize.{w, w, v, v₂, u, u₂} G
• CategoryTheory.Limits.preservesColimit_of_preservesCoequalizers_and_coproduct 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) C] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) C] [CategoryTheory.Limits.HasCoequalizers C] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) G] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G] : CategoryTheory.Limits.PreservesColimitsOfShape J G
• CategoryTheory.Limits.createsColimitsOfShapeOfCreatesCoequalizersAndCoproducts 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete J) D] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) D] [CategoryTheory.Limits.HasCoequalizers D] (G : CategoryTheory.Functor C D) [G.ReflectsIsomorphisms] [CategoryTheory.CreatesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G] [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) G] [CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete ((p : J × J) × (p.1 ⟶ p.2))) G] : CategoryTheory.CreatesColimitsOfShape J G
• CategoryTheory.Limits.colimitCoconeOfCoequalizerAndCoproduct 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.1)] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.ColimitCocone F
• CategoryTheory.Limits.hasColimit_of_coequalizer_and_coproduct 📋 Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor F.obj)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Discrete.functor fun f => F.obj f.fst.1)] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasColimit F
• CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers 📋 Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasPushouts C
• CategoryTheory.NormalEpiCategory.hasCoequalizers 📋 Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.IsNormalEpiCategory C] : CategoryTheory.Limits.HasCoequalizers C
• CategoryTheory.Abelian.hasCoequalizers 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] : CategoryTheory.Limits.HasCoequalizers C
• CategoryTheory.Functor.preservesFiniteColimits_of_preservesCokernels 📋 Mathlib.CategoryTheory.Preadditive.LeftExact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F] : CategoryTheory.Limits.PreservesFiniteColimits F
• CategoryTheory.HasCodetector.hasCoseparator 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.HasCodetector C] : CategoryTheory.HasCoseparator C
• CategoryTheory.IsCodetector.isCoseparator 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C] {G : C} : CategoryTheory.IsCodetector G → CategoryTheory.IsCoseparator G
• CategoryTheory.isCoseparator_codetector 📋 Mathlib.CategoryTheory.Generator.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.HasCodetector C] : CategoryTheory.IsCoseparator (CategoryTheory.codetector C)
• CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasCoequalizers C] : P.IsCodetecting → P.IsCoseparating
• CategoryTheory.ObjectProperty.isCodetecting_iff_isCoseparating 📋 Mathlib.CategoryTheory.Generator.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Balanced C] : P.IsCodetecting ↔ P.IsCoseparating
• CategoryTheory.Limits.hasCoequalizers_of_hasWideCoequalizers 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideCoequalizers C] : CategoryTheory.Limits.HasCoequalizers C
• CategoryTheory.Limits.hasReflexiveCoequalizers_of_hasCoequalizers 📋 Mathlib.CategoryTheory.Limits.Shapes.Reflexive
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoequalizers C] : CategoryTheory.Limits.HasReflexiveCoequalizers C
• AlgebraicGeometry.LocallyRingedSpace.instHasCoequalizers 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
  : CategoryTheory.Limits.HasCoequalizers AlgebraicGeometry.LocallyRingedSpace
• CategoryTheory.ObjectProperty.SerreClassLocalization.hasCoequalizers 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] : CategoryTheory.Limits.HasCoequalizers D
• Bimod.TensorBimod.X 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) : C
• Bimod.monBicategory 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.Bicategory (CategoryTheory.Mon C)
• Bimod.LeftUnitorBimod.hom 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : Bimod.TensorBimod.X (Bimod.regular R) P ⟶ P.X
• Bimod.LeftUnitorBimod.inv 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : P.X ⟶ Bimod.TensorBimod.X (Bimod.regular R) P
• Bimod.RightUnitorBimod.hom 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : Bimod.TensorBimod.X P (Bimod.regular S) ⟶ P.X
• Bimod.RightUnitorBimod.inv 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : P.X ⟶ Bimod.TensorBimod.X P (Bimod.regular S)
• Bimod.tensorBimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : Bimod X Z
• Bimod.leftUnitorBimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y : CategoryTheory.Mon C} (M : Bimod X Y) : (Bimod.regular X).tensorBimod M ≅ M
• Bimod.rightUnitorBimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y : CategoryTheory.Mon C} (M : Bimod X Y) : M.tensorBimod (Bimod.regular Y) ≅ M
• Bimod.TensorBimod.actLeft 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.MonoidalCategoryStruct.tensorObj R.X (Bimod.TensorBimod.X P Q) ⟶ Bimod.TensorBimod.X P Q
• Bimod.TensorBimod.actRight 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.MonoidalCategoryStruct.tensorObj (Bimod.TensorBimod.X P Q) T.X ⟶ Bimod.TensorBimod.X P Q
• Bimod.tensorBimod_X 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : (M.tensorBimod N).X = Bimod.TensorBimod.X M N
• Bimod.LeftUnitorBimod.inv_hom_id 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.LeftUnitorBimod.inv P) (Bimod.LeftUnitorBimod.hom P) = CategoryTheory.CategoryStruct.id P.X
• Bimod.RightUnitorBimod.inv_hom_id 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.RightUnitorBimod.inv P) (Bimod.RightUnitorBimod.hom P) = CategoryTheory.CategoryStruct.id P.X
• Bimod.associatorBimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W X Y Z : CategoryTheory.Mon C} (L : Bimod W X) (M : Bimod X Y) (N : Bimod Y Z) : (L.tensorBimod M).tensorBimod N ≅ L.tensorBimod (M.tensorBimod N)
• Bimod.tensorBimod_actLeft 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : (M.tensorBimod N).actLeft = Bimod.TensorBimod.actLeft M N
• Bimod.tensorBimod_actRight 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : (M.tensorBimod N).actRight = Bimod.TensorBimod.actRight M N
• Bimod.AssociatorBimod.hom 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : ((P.tensorBimod Q).tensorBimod L).X ⟶ (P.tensorBimod (Q.tensorBimod L)).X
• Bimod.AssociatorBimod.inv 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : (P.tensorBimod (Q.tensorBimod L)).X ⟶ ((P.tensorBimod Q).tensorBimod L).X
• Bimod.AssociatorBimod.homAux 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.MonoidalCategoryStruct.tensorObj (P.tensorBimod Q).X L.X ⟶ (P.tensorBimod (Q.tensorBimod L)).X
• Bimod.AssociatorBimod.invAux 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (Q.tensorBimod L).X ⟶ ((P.tensorBimod Q).tensorBimod L).X
• Bimod.LeftUnitorBimod.hom_inv_id 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.LeftUnitorBimod.hom P) (Bimod.LeftUnitorBimod.inv P) = CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X (Bimod.regular R) P)
• Bimod.RightUnitorBimod.hom_inv_id 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.RightUnitorBimod.hom P) (Bimod.RightUnitorBimod.inv P) = CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X P (Bimod.regular S))
• Bimod.whiskerLeft 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N₁ N₂ : Bimod Y Z} (f : N₁ ⟶ N₂) : M.tensorBimod N₁ ⟶ M.tensorBimod N₂
• Bimod.whiskerRight 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} {M₁ M₂ : Bimod X Y} (f : M₁ ⟶ M₂) (N : Bimod Y Z) : M₁.tensorBimod N ⟶ M₂.tensorBimod N
• Bimod.id_whiskerRight_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} {M : Bimod X Y} {N : Bimod Y Z} : Bimod.whiskerRight (CategoryTheory.CategoryStruct.id M) N = CategoryTheory.CategoryStruct.id (M.tensorBimod N)
• Bimod.whiskerLeft_id_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} {M : Bimod X Y} {N : Bimod Y Z} : M.whiskerLeft (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (M.tensorBimod N)
• Bimod.TensorBimod.actRight_one' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Bimod.TensorBimod.X P Q) CategoryTheory.MonObj.one) (Bimod.TensorBimod.actRight P Q) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Bimod.TensorBimod.X P Q)).hom
• Bimod.TensorBimod.one_act_left' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (Bimod.TensorBimod.X P Q)) (Bimod.TensorBimod.actLeft P Q) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Bimod.TensorBimod.X P Q)).hom
• Bimod.AssociatorBimod.hom_inv_id 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (Bimod.AssociatorBimod.hom P Q L) (Bimod.AssociatorBimod.inv P Q L) = CategoryTheory.CategoryStruct.id ((P.tensorBimod Q).tensorBimod L).X
• Bimod.AssociatorBimod.inv_hom_id 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (Bimod.AssociatorBimod.inv P Q L) (Bimod.AssociatorBimod.hom P Q L) = CategoryTheory.CategoryStruct.id (P.tensorBimod (Q.tensorBimod L)).X
• Bimod.LeftUnitorBimod.hom_left_act_hom' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp ((Bimod.regular R).tensorBimod P).actLeft (Bimod.LeftUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.LeftUnitorBimod.hom P)) P.actLeft
• Bimod.LeftUnitorBimod.hom_right_act_hom' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp ((Bimod.regular R).tensorBimod P).actRight (Bimod.LeftUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.LeftUnitorBimod.hom P) S.X) P.actRight
• Bimod.RightUnitorBimod.hom_left_act_hom' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (P.tensorBimod (Bimod.regular S)).actLeft (Bimod.RightUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.RightUnitorBimod.hom P)) P.actLeft
• Bimod.RightUnitorBimod.hom_right_act_hom' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (P.tensorBimod (Bimod.regular S)).actRight (Bimod.RightUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.RightUnitorBimod.hom P) S.X) P.actRight
• Bimod.comp_whiskerRight_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} {M N P : Bimod X Y} (f : M ⟶ N) (g : N ⟶ P) (Q : Bimod Y Z) : Bimod.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Q = CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight f Q) (Bimod.whiskerRight g Q)
• Bimod.whiskerLeft_comp_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N P Q : Bimod Y Z} (f : N ⟶ P) (g : P ⟶ Q) : M.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (M.whiskerLeft f) (M.whiskerLeft g)
• Bimod.id_whiskerLeft_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y : CategoryTheory.Mon C} {M N : Bimod X Y} (f : M ⟶ N) : (Bimod.regular X).whiskerLeft f = CategoryTheory.CategoryStruct.comp M.leftUnitorBimod.hom (CategoryTheory.CategoryStruct.comp f N.leftUnitorBimod.inv)
• Bimod.whiskerRight_id_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y : CategoryTheory.Mon C} {M N : Bimod X Y} (f : M ⟶ N) : Bimod.whiskerRight f (Bimod.regular Y) = CategoryTheory.CategoryStruct.comp M.rightUnitorBimod.hom (CategoryTheory.CategoryStruct.comp f N.rightUnitorBimod.inv)
• Bimod.whisker_exchange_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} {M N : Bimod X Y} {P Q : Bimod Y Z} (f : M ⟶ N) (g : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (M.whiskerLeft g) (Bimod.whiskerRight f Q) = CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight f P) (N.whiskerLeft g)
• Bimod.triangle_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : CategoryTheory.CategoryStruct.comp (M.associatorBimod (Bimod.regular Y) N).hom (M.whiskerLeft N.leftUnitorBimod.hom) = Bimod.whiskerRight M.rightUnitorBimod.hom N
• Bimod.AssociatorBimod.hom_left_act_hom' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp ((P.tensorBimod Q).tensorBimod L).actLeft (Bimod.AssociatorBimod.hom P Q L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.AssociatorBimod.hom P Q L)) (P.tensorBimod (Q.tensorBimod L)).actLeft
• Bimod.AssociatorBimod.hom_right_act_hom' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp ((P.tensorBimod Q).tensorBimod L).actRight (Bimod.AssociatorBimod.hom P Q L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.AssociatorBimod.hom P Q L) U.X) (P.tensorBimod (Q.tensorBimod L)).actRight
• Bimod.TensorBimod.left_assoc' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (Bimod.TensorBimod.X P Q)) (Bimod.TensorBimod.actLeft P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X R.X (Bimod.TensorBimod.X P Q)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.TensorBimod.actLeft P Q)) (Bimod.TensorBimod.actLeft P Q))
• Bimod.TensorBimod.right_assoc' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Bimod.TensorBimod.X P Q) CategoryTheory.MonObj.mul) (Bimod.TensorBimod.actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (Bimod.TensorBimod.X P Q) T.X T.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.TensorBimod.actRight P Q) T.X) (Bimod.TensorBimod.actRight P Q))
• Bimod.TensorBimod.middle_assoc' 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.TensorBimod.actLeft P Q) T.X) (Bimod.TensorBimod.actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X (Bimod.TensorBimod.X P Q) T.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.TensorBimod.actRight P Q)) (Bimod.TensorBimod.actLeft P Q))
• Bimod.comp_whiskerLeft_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W X Y Z : CategoryTheory.Mon C} (M : Bimod W X) (N : Bimod X Y) {P P' : Bimod Y Z} (f : P ⟶ P') : (M.tensorBimod N).whiskerLeft f = CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).hom (CategoryTheory.CategoryStruct.comp (M.whiskerLeft (N.whiskerLeft f)) (M.associatorBimod N P').inv)
• Bimod.whiskerRight_comp_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W X Y Z : CategoryTheory.Mon C} {M M' : Bimod W X} (f : M ⟶ M') (N : Bimod X Y) (P : Bimod Y Z) : Bimod.whiskerRight f (N.tensorBimod P) = CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).inv (CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight (Bimod.whiskerRight f N) P) (M'.associatorBimod N P).hom)
• Bimod.whisker_assoc_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W X Y Z : CategoryTheory.Mon C} (M : Bimod W X) {N N' : Bimod X Y} (f : N ⟶ N') (P : Bimod Y Z) : Bimod.whiskerRight (M.whiskerLeft f) P = CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).hom (CategoryTheory.CategoryStruct.comp (M.whiskerLeft (Bimod.whiskerRight f P)) (M.associatorBimod N' P).inv)
• id_tensor_π_preserves_coequalizer_inv_desc 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] {W X Y Z : C} (f g : X ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ W) (wh : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv (CategoryTheory.Limits.coequalizer.desc h wh)) = h
• π_tensor_id_preserves_coequalizer_inv_desc 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W X Y Z : C} (f g : X ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ W) (wh : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π f g) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv (CategoryTheory.Limits.coequalizer.desc h wh)) = h
• Bimod.pentagon_bimod 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {V W X Y Z : CategoryTheory.Mon C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y) (Q : Bimod Y Z) : CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight (M.associatorBimod N P).hom Q) (CategoryTheory.CategoryStruct.comp (M.associatorBimod (N.tensorBimod P) Q).hom (M.whiskerLeft (N.associatorBimod P Q).hom)) = CategoryTheory.CategoryStruct.comp ((M.tensorBimod N).associatorBimod P Q).hom (M.associatorBimod N (P.tensorBimod Q)).hom
• id_tensor_π_preserves_coequalizer_inv_colimMap_desc 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] {X Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ X') (q : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) q = CategoryTheory.CategoryStruct.comp p g') (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) f' g' p q wf wg)) (CategoryTheory.Limits.coequalizer.desc h wh))) = CategoryTheory.CategoryStruct.comp q h
• π_tensor_id_preserves_coequalizer_inv_colimMap_desc 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ X') (q : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) q = CategoryTheory.CategoryStruct.comp p g') (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π f g) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) f' g' p q wf wg)) (CategoryTheory.Limits.coequalizer.desc h wh))) = CategoryTheory.CategoryStruct.comp q h
• Bimod.whiskerLeft_hom 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N₁ N₂ : Bimod Y Z} (f : N₁ ⟶ N₂) : (M.whiskerLeft f).hom = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₁.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₁.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₁.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₂.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₂.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₂.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X Y.X) f.hom) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X f.hom) ⋯ ⋯)
• Bimod.whiskerRight_hom 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X Y Z : CategoryTheory.Mon C} {M₁ M₂ : Bimod X Y} (f : M₁ ⟶ M₂) (N : Bimod Y Z) : (Bimod.whiskerRight f N).hom = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₁.actRight N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₁.X Y.X N.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁.X N.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₂.actRight N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₂.X Y.X N.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₂.X N.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X) N.X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom N.X) ⋯ ⋯)
• Bimod.TensorBimod.whiskerLeft_π_actLeft 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))) (Bimod.TensorBimod.actLeft P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X P.X Q.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actLeft Q.X) (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))))
• Bimod.TensorBimod.π_tensor_id_actRight 📋 Mathlib.CategoryTheory.Monoidal.Bimod
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))) T.X) (Bimod.TensorBimod.actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X Q.X T.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actRight) (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c