ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).inv Z) (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).hom) (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).hom Z) (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).inv Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).hom Z) (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).inv) (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).hom Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).hom) (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).inv Z) (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).inv Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).hom Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.MonoidalCategory.associator X Y Z).inv) (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (𝟙_ C) Y).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitor X).hom Y) = CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.leftUnitor Y).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitor X).inv Y) (CategoryTheory.MonoidalCategory.associator X (𝟙_ C) Y).hom = CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.leftUnitor Y).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.leftUnitor Y).inv) (CategoryTheory.MonoidalCategory.associator X (𝟙_ C) Y).inv = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitor X).inv Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).hom Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).hom (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).inv Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.rightUnitor Y).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv (CategoryTheory.MonoidalCategory.associator X Y (𝟙_ C)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).hom Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).inv Y) (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y (𝟙_ C)).hom (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.rightUnitor Y).hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.rightUnitor Y).inv) (CategoryTheory.MonoidalCategory.associator X Y (𝟙_ C)).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z X' Y' Z' : C<VAR>f : X ⟶ X'<VAR>g : Y ⟶ Y'<VAR>h : Z ⟶ Z'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h)) (CategoryTheory.MonoidalCategory.associator X' Y' Z').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' Y Y' Z Z' : C<VAR>f : X ⟶ X'<VAR>g : Y ⟶ Y'<VAR>h : Z ⟶ Z'<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h)) (CategoryTheory.MonoidalCategory.associator X' Y' Z').inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' Y Y' Z Z' : C<VAR>f : X ⟶ X'<VAR>g : Y ⟶ Y'<VAR>h : Z ⟶ Z'<GOAL>CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.MonoidalCategory.tensorHom g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f g) h) (CategoryTheory.MonoidalCategory.associator X' Y' Z').hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z Z' : C<VAR>h : Z ⟶ Z'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)) h) (CategoryTheory.MonoidalCategory.associator X Y Z').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) h))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z X' : C<VAR>f : X ⟶ X'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y Z))) (CategoryTheory.MonoidalCategory.associator X' Y Z).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y)) (CategoryTheory.CategoryStruct.id Z))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom g) (CategoryTheory.MonoidalCategory.tensorHom f.inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.inv g) (CategoryTheory.MonoidalCategory.tensorHom f.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f.hom) (CategoryTheory.MonoidalCategory.tensorHom h f.inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id V)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id V))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ≅ W<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f.inv) (CategoryTheory.MonoidalCategory.tensorHom h f.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id W))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ⟶ W<VAR>CategoryTheory.IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id V) h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ⟶ W<VAR>CategoryTheory.IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) g) (CategoryTheory.MonoidalCategory.tensorHom f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) g) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ⟶ W<VAR>CategoryTheory.IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.inv f)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id V)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id V))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>V W X Y Z : C<VAR>f : V ⟶ W<VAR>CategoryTheory.IsIso f<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.inv f)) (CategoryTheory.MonoidalCategory.tensorHom h f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.MonoidalCategory.tensorHom h (CategoryTheory.CategoryStruct.id W))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id Z))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) f) (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id X)) = CategoryTheory.MonoidalCategory.tensorHom g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id W)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) = CategoryTheory.MonoidalCategory.tensorHom g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (𝟙_ C)) f = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (𝟙_ C)) g ↔ f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (𝟙_ C)) = CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id (𝟙_ C)) ↔ f = g
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C × C<GOAL>(CategoryTheory.MonoidalCategory.tensor C).obj X = CategoryTheory.MonoidalCategory.tensorObj X.1 X.2
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C × C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.MonoidalCategory.tensor C).map f = CategoryTheory.MonoidalCategory.tensorHom f.1 f.2
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C × C × C<GOAL>(CategoryTheory.MonoidalCategory.leftAssocTensor C).obj X = CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X.1 X.2.1) X.2.2
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C × C × C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.MonoidalCategory.leftAssocTensor C).map f = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f.1 f.2.1) f.2.2
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C × C × C<GOAL>(CategoryTheory.MonoidalCategory.rightAssocTensor C).obj X = CategoryTheory.MonoidalCategory.tensorObj X.1 (CategoryTheory.MonoidalCategory.tensorObj X.2.1 X.2.2)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C × C × C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.MonoidalCategory.rightAssocTensor C).map f = CategoryTheory.MonoidalCategory.tensorHom f.1 (CategoryTheory.MonoidalCategory.tensorHom f.2.1 f.2.2)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (Y_1 : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).map f).app Y_1 = CategoryTheory.MonoidalCategory.whiskerRight f Y_1
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ {X_1 Y : C} (g : X_1 ⟶ Y), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X).map g = CategoryTheory.MonoidalCategory.whiskerLeft X g
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>((CategoryTheory.MonoidalCategory.curriedTensor C).obj X).obj Y = CategoryTheory.MonoidalCategory.tensorObj X Y
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.tensorLeft X).obj Y = CategoryTheory.MonoidalCategory.tensorObj X Y
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ {X_1 Y : C} (g : X_1 ⟶ Y), (CategoryTheory.MonoidalCategory.tensorLeft X).map g = CategoryTheory.MonoidalCategory.whiskerLeft X g
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X j : C<GOAL>(CategoryTheory.MonoidalCategory.tensorRight X).obj j = CategoryTheory.MonoidalCategory.tensorObj j X
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ {X_1 Y : C} (f : X_1 ⟶ Y), (CategoryTheory.MonoidalCategory.tensorRight X).map f = CategoryTheory.MonoidalCategory.whiskerRight f X
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C × C × C<GOAL>(CategoryTheory.MonoidalCategory.associatorNatIso C).hom.app X = (CategoryTheory.MonoidalCategory.associator X.1 X.2.1 X.2.2).hom
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C × C × C<GOAL>(CategoryTheory.MonoidalCategory.associatorNatIso C).inv.app X = (CategoryTheory.MonoidalCategory.associator X.1 X.2.1 X.2.2).inv
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitorNatIso C).hom.app X = (CategoryTheory.MonoidalCategory.leftUnitor X).hom
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitorNatIso C).inv.app X = (CategoryTheory.MonoidalCategory.leftUnitor X).inv
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitorNatIso C).hom.app X = (CategoryTheory.MonoidalCategory.rightUnitor X).hom
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitorNatIso C).inv.app X = (CategoryTheory.MonoidalCategory.rightUnitor X).inv