ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : CategoryTheory.LaxMonoidalFunctor C D<VAR>α β : F ⟶ G<VAR>w : ∀ (X : C), α.app X = β.app X<GOAL>α = β
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G H : CategoryTheory.MonoidalFunctor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>(α ≫ β).toNatTrans = α.toNatTrans ≫ β.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F G : CategoryTheory.LaxMonoidalFunctor C D<VAR>H K : CategoryTheory.LaxMonoidalFunctor D E<VAR>α : CategoryTheory.MonoidalNatTrans F G<VAR>β : CategoryTheory.MonoidalNatTrans H K<GOAL>(α.hcomp β).toNatTrans = α.toNatTrans ◫ β.toNatTrans
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F G : CategoryTheory.LaxMonoidalFunctor C D<VAR>H K : CategoryTheory.LaxMonoidalFunctor C E<VAR>α : CategoryTheory.MonoidalNatTrans F G<VAR>β : CategoryTheory.MonoidalNatTrans H K<VAR>X : C<GOAL>(α.prod β).app X = (α.app X, β.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : CategoryTheory.LaxMonoidalFunctor C D<VAR>app : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f<VAR>unit : F.ε ≫ (app (𝟙_ C)).hom = G.ε<VAR>tensor : ∀ (X Y : C), F.μ X Y ≫ (app (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom ≫ G.μ X Y<VAR>X : C<GOAL>(CategoryTheory.MonoidalNatIso.ofComponents app naturality unit tensor).hom.app X = (app X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : CategoryTheory.LaxMonoidalFunctor C D<VAR>app : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f<VAR>unit : F.ε ≫ (app (𝟙_ C)).hom = G.ε<VAR>tensor : ∀ (X Y : C), F.μ X Y ≫ (app (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.MonoidalCategory.tensorHom (app X).hom (app Y).hom ≫ G.μ X Y<VAR>X : C<GOAL>(CategoryTheory.MonoidalNatIso.ofComponents app naturality unit tensor).inv.app X = (app X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<GOAL>(CategoryTheory.monoidalCounit F h).toNatTrans = h.counit
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.MonoidalPreadditive C<VAR>X Y Z : C<VAR>f g : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (f + g) X = CategoryTheory.MonoidalCategory.whiskerRight f X + CategoryTheory.MonoidalCategory.whiskerRight g X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.MonoidalPreadditive C<VAR>X Y Z : C<VAR>f g : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (f + g) = CategoryTheory.MonoidalCategory.whiskerLeft X f + CategoryTheory.MonoidalCategory.whiskerLeft X g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.MonoidalPreadditive C<VAR>X Y Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.MonoidalPreadditive C<VAR>X Y Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight 0 X = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>W X Y Z : C<VAR>f : W ⟶ X<GOAL>CategoryTheory.MonoidalCategory.tensorHom f 0 = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>W X Y Z : C<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.tensorHom 0 f = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g h : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.tensorHom f (g + h) = CategoryTheory.MonoidalCategory.tensorHom f g + CategoryTheory.MonoidalCategory.tensorHom f h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>W X Y Z : C<VAR>f g : W ⟶ X<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.tensorHom (f + g) h = CategoryTheory.MonoidalCategory.tensorHom f h + CategoryTheory.MonoidalCategory.tensorHom g h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.MonoidalFunctor D C<VAR>F.Faithful<VAR>F.Additive<GOAL>CategoryTheory.MonoidalPreadditive D
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>P : C<VAR>Q R : C<VAR>J : Type u_2<VAR>s : Finset J<VAR>g : J → (Q ⟶ R)<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft P (∑ j ∈ s, g j) = ∑ j ∈ s, CategoryTheory.MonoidalCategory.whiskerLeft P (g j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>Q R : C<VAR>J : Type u_2<VAR>s : Finset J<VAR>g : J → (Q ⟶ R)<VAR>P : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (∑ j ∈ s, g j) P = ∑ j ∈ s, CategoryTheory.MonoidalCategory.whiskerRight (g j) P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>P Q R S : C<VAR>J : Type u_2<VAR>s : Finset J<VAR>f : P ⟶ Q<VAR>g : J → (R ⟶ S)<GOAL>CategoryTheory.MonoidalCategory.tensorHom f (∑ j ∈ s, g j) = ∑ j ∈ s, CategoryTheory.MonoidalCategory.tensorHom f (g j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>P Q R S : C<VAR>J : Type u_2<VAR>s : Finset J<VAR>f : P ⟶ Q<VAR>g : J → (R ⟶ S)<GOAL>CategoryTheory.MonoidalCategory.tensorHom (∑ j ∈ s, g j) f = ∑ j ∈ s, CategoryTheory.MonoidalCategory.tensorHom (g j) f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X : C<VAR>f : J → C<GOAL>(CategoryTheory.leftDistributor X f).hom = ∑ j : J, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X : C<VAR>f : J → C<GOAL>(CategoryTheory.leftDistributor X f).inv = ∑ j : J, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j) (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X : C<VAR>f : J → C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j) = CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X : C<VAR>f : J → C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) (CategoryTheory.leftDistributor X f).hom = CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X : C<VAR>f : J → C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X : C<VAR>f : J → C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategory.tensorObj X (f j)) j) (CategoryTheory.leftDistributor X f).inv = CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X Y : C<VAR>f : J → C<GOAL>((CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X) ⊗ CategoryTheory.leftDistributor Y f) ≪≫ CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategory.tensorObj Y (f j)) = (CategoryTheory.MonoidalCategory.associator X Y (⨁ f)).symm ≪≫ CategoryTheory.leftDistributor (CategoryTheory.MonoidalCategory.tensorObj X Y) f ≪≫ CategoryTheory.Limits.biproduct.mapIso fun j => CategoryTheory.MonoidalCategory.associator X Y (f j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X : C<GOAL>(CategoryTheory.rightDistributor f X).hom = ∑ j : J, CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X : C<GOAL>(CategoryTheory.rightDistributor f X).inv = ∑ j : J, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j) (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).hom (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j) = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) (CategoryTheory.rightDistributor f X).hom = CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) = CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X : C<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) X) j) (CategoryTheory.rightDistributor f X).inv = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X Y : C<GOAL>(CategoryTheory.rightDistributor f X ⊗ CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫ CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) X) Y = CategoryTheory.MonoidalCategory.associator (⨁ f) X Y ≪≫ CategoryTheory.rightDistributor f (CategoryTheory.MonoidalCategory.tensorObj X Y) ≪≫ CategoryTheory.Limits.biproduct.mapIso fun j => (CategoryTheory.MonoidalCategory.associator (f j) X Y).symm
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X : C<VAR>f : J → C<VAR>Y : C<GOAL>(CategoryTheory.leftDistributor X f ⊗ CategoryTheory.asIso (CategoryTheory.CategoryStruct.id Y)) ≪≫ CategoryTheory.rightDistributor (fun j => CategoryTheory.MonoidalCategory.tensorObj X (f j)) Y = CategoryTheory.MonoidalCategory.associator X (⨁ f) Y ≪≫ (CategoryTheory.asIso (CategoryTheory.CategoryStruct.id X) ⊗ CategoryTheory.rightDistributor f Y) ≪≫ (CategoryTheory.leftDistributor X fun j => CategoryTheory.MonoidalCategory.tensorObj (f j) Y) ≪≫ CategoryTheory.Limits.biproduct.mapIso fun j => (CategoryTheory.MonoidalCategory.associator X (f j) Y).symm
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : CategoryTheory.MonoidalCategory.tensorObj X (⨁ f) ⟶ Y<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j)) h<GOAL>g = h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y (⨁ f)<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategory.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j)) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategory.whiskerLeft Y (CategoryTheory.Limits.biproduct.π f j))<GOAL>g = h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X Y Z : C<VAR>f : J → C<VAR>g h : CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y (⨁ f)) ⟶ Z<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y (CategoryTheory.Limits.biproduct.ι f j))) h<GOAL>g = h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>X Y Z : C<VAR>f : J → C<VAR>g h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj Y (CategoryTheory.MonoidalCategory.tensorObj Z (⨁ f))<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategory.whiskerLeft Y (CategoryTheory.MonoidalCategory.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j))) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategory.whiskerLeft Y (CategoryTheory.MonoidalCategory.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j)))<GOAL>g = h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X ⟶ Y<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) h<GOAL>g = h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X Y : C<VAR>g h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj (⨁ f) Y<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y)<GOAL>g = h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X Y Z : C<VAR>g h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (⨁ f) X) Y ⟶ Z<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.ι f j) X) Y) h<GOAL>g = h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Fintype J<VAR>f : J → C<VAR>X Y Z : C<VAR>g h : X ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj (⨁ f) Y) Z<VAR>w : ∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z) = CategoryTheory.CategoryStruct.comp h (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Limits.biproduct.π f j) Y) Z)<GOAL>g = h
<VAR>C : Type u₁<GOAL>Function.Injective CategoryTheory.MonoidalOpposite.mop
<VAR>C : Type u₁<GOAL>Function.Injective CategoryTheory.MonoidalOpposite.unmop
<VAR>C : Type u₁<VAR>x y : C<GOAL>{ unmop := x } = { unmop := y } ↔ x = y
<VAR>C : Type u₁<VAR>x y : Cᴹᵒᵖ<GOAL>x.unmop = y.unmop ↔ x = y
<VAR>C : Type u₁<VAR>X : Cᴹᵒᵖ<GOAL>{ unmop := X.unmop } = X
<VAR>C : Type u₁<VAR>X : C<GOAL>{ unmop := X }.unmop = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<GOAL>Function.Injective Quiver.Hom.mop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᴹᵒᵖ<GOAL>Function.Injective Quiver.Hom.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f.mop.unmop = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᴹᵒᵖ<VAR>f : X ⟶ Y<GOAL>f.unmop.mop = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).mop = f.mop ≫ g.mop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(𝟙 X).mop = 𝟙 { unmop := X }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᴹᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).unmop = f.unmop ≫ g.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᴹᵒᵖ<GOAL>(𝟙 X).unmop = 𝟙 X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(𝟙 { unmop := X }).unmop = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᴹᵒᵖ<GOAL>(𝟙 X.unmop).mop = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>unmop : C<GOAL>(CategoryTheory.mopFunctor C).obj unmop = { unmop := unmop }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.mopFunctor C).map f = f.mop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : Cᴹᵒᵖ<GOAL>(CategoryTheory.unmopFunctor C).obj self = self.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : Cᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.unmopFunctor C).map f = f.unmop