ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) f₃) (CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom (CategoryTheory.MonoidalCategory.tensorHom f₁ (CategoryTheory.MonoidalCategory.tensorHom f₂ f₃))
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f X₂) (CategoryTheory.MonoidalCategory.whiskerLeft Y₁ g)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.id X) Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ : C<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator W X Y).hom Z) (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)) = 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
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorHom g₁ g₂)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y₁ Y₂ : C<VAR>f : Y₁ ⟶ Y₂<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f = CategoryTheory.MonoidalCategory.whiskerLeft X f
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>Y : C<GOAL>CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.MonoidalCategory.whiskerRight f Y
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W : C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft W (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W f) (CategoryTheory.MonoidalCategory.whiskerLeft W g)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.leftUnitor Y).inv)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>Z Z' : C<VAR>f : Z ⟶ Z'<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X Y) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y f)) (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 : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (CategoryTheory.MonoidalCategory.whiskerRight g Z)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.rightUnitor Y).inv)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight f (CategoryTheory.MonoidalCategory.tensorObj Y Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight f Y) Z) (CategoryTheory.MonoidalCategory.associator X' Y Z).hom)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Y' : C<VAR>f : Y ⟶ Y'<VAR>Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X f) Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerRight f Z)) (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<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft W g) (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Y) (CategoryTheory.MonoidalCategory.whiskerLeft X g)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X₁ g) (CategoryTheory.MonoidalCategory.whiskerRight f Y₂)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>Z₁ Z₂ : C<VAR>f : Z₁ ⟶ Z₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y f)) (CategoryTheory.MonoidalCategory.associator X Y Z₂).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z₁).inv (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X Y) f)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ≅ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f.hom) (CategoryTheory.MonoidalCategory.whiskerLeft X f.inv) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f.hom Z) (CategoryTheory.MonoidalCategory.whiskerRight f.inv Z) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Z)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ≅ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f.inv) (CategoryTheory.MonoidalCategory.whiskerLeft X f.hom) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Z)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f.inv Z) (CategoryTheory.MonoidalCategory.whiskerRight f.hom Z) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y Z)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.inv f)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.inv f) Z) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Z)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.inv f)) (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Z)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.inv f) Z) (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y Z)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ≅ Z<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeftIso X f).hom = CategoryTheory.MonoidalCategory.whiskerLeft X f.hom
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ≅ Z<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeftIso X f).inv = CategoryTheory.MonoidalCategory.whiskerLeft X f.inv
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.inv (CategoryTheory.MonoidalCategory.whiskerLeft X f) = CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.inv f)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X : C<GOAL>CategoryTheory.MonoidalCategory.whiskerLeftIso W (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorObj W X)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W : C<VAR>X Y Z : C<VAR>f : X ≅ Y<VAR>g : Y ≅ Z<GOAL>CategoryTheory.MonoidalCategory.whiskerLeftIso W (f ≪≫ g) = CategoryTheory.MonoidalCategory.whiskerLeftIso W f ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso W g
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W : C<VAR>X Y : C<VAR>f : X ≅ Y<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeftIso W f).symm = CategoryTheory.MonoidalCategory.whiskerLeftIso W f.symm
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>Z : C<GOAL>(CategoryTheory.MonoidalCategory.whiskerRightIso f Z).inv = CategoryTheory.MonoidalCategory.whiskerRight f.inv Z
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>Z : C<GOAL>(CategoryTheory.MonoidalCategory.whiskerRightIso f Z).hom = CategoryTheory.MonoidalCategory.whiskerRight f.hom Z
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.inv (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.inv f) Z
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X W : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.Iso.refl X) W = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategory.tensorObj X W)
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<VAR>f : X ≅ Y<VAR>g : Y ≅ Z<VAR>W : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRightIso (f ≪≫ g) W = CategoryTheory.MonoidalCategory.whiskerRightIso f W ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso g W
<VAR>C : Type u<VAR>𝒞 : CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>W : C<GOAL>(CategoryTheory.MonoidalCategory.whiskerRightIso f W).symm = CategoryTheory.MonoidalCategory.whiskerRightIso f.symm W
<VAR>C : Type u<VAR>X Y X' Y' : C<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f : X ≅ Y<VAR>g : X' ≅ Y'<GOAL>(f ⊗ g).inv = CategoryTheory.MonoidalCategory.tensorHom f.inv g.inv
<VAR>C : Type u<VAR>X Y X' Y' : C<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>f : X ≅ Y<VAR>g : X' ≅ Y'<GOAL>(f ⊗ g).hom = CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom
<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>CategoryTheory.IsIso f<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<GOAL>CategoryTheory.inv (CategoryTheory.MonoidalCategory.tensorHom f g) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.inv f) (CategoryTheory.inv g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : Prop<VAR>Decidable P<VAR>X : C<VAR>Y Z : C<VAR>f : P → (Y ⟶ Z)<VAR>f' : ¬P → (Y ⟶ Z)<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (if h : P then f h else f' h) = if h : P then CategoryTheory.MonoidalCategory.whiskerLeft X (f h) else CategoryTheory.MonoidalCategory.whiskerLeft X (f' h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : Prop<VAR>Decidable P<VAR>X Y : C<VAR>f : P → (X ⟶ Y)<VAR>f' : ¬P → (X ⟶ Y)<VAR>Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (if h : P then f h else f' h) Z = if h : P then CategoryTheory.MonoidalCategory.whiskerRight (f h) Z else CategoryTheory.MonoidalCategory.whiskerRight (f' h) Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : Prop<VAR>Decidable P<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : P → (Y ⟶ Z)<VAR>g' : ¬P → (Y ⟶ Z)<GOAL>CategoryTheory.MonoidalCategory.tensorHom f (if h : P then g h else g' h) = if h : P then CategoryTheory.MonoidalCategory.tensorHom f (g h) else CategoryTheory.MonoidalCategory.tensorHom f (g' h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : Prop<VAR>Decidable P<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : P → (Y ⟶ Z)<VAR>g' : ¬P → (Y ⟶ Z)<GOAL>CategoryTheory.MonoidalCategory.tensorHom (if h : P then g h else g' h) f = if h : P then CategoryTheory.MonoidalCategory.tensorHom (g h) f else CategoryTheory.MonoidalCategory.tensorHom (g' h) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y = Z<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.eqToHom f) = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X = Y<VAR>Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.eqToHom f) Z = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight f Y) Z) (CategoryTheory.MonoidalCategory.associator X' Y Z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.MonoidalCategory.whiskerRight f (CategoryTheory.MonoidalCategory.tensorObj Y Z))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.MonoidalCategory.associator X' Y Z).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight f Y) Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<VAR>Y Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight f Y) Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.MonoidalCategory.associator X' Y Z).inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Y' : C<VAR>f : Y ⟶ Y'<VAR>Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X f) Z) (CategoryTheory.MonoidalCategory.associator X Y' Z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerRight f Z))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Y' : C<VAR>f : Y ⟶ Y'<VAR>Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerRight f Z)) (CategoryTheory.MonoidalCategory.associator X Y' Z).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X f) Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Y' : C<VAR>f : Y ⟶ Y'<VAR>Z : C<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerRight f Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X f) Z) (CategoryTheory.MonoidalCategory.associator X Y' Z).hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>Z Z' : C<VAR>f : Z ⟶ Z'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X Y) f) (CategoryTheory.MonoidalCategory.associator X Y Z').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>Z Z' : C<VAR>f : Z ⟶ Z'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y f)) (CategoryTheory.MonoidalCategory.associator X Y Z').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X Y) f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>Z Z' : C<VAR>f : Z ⟶ Z'<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.whiskerLeft Y f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X Y) f) (CategoryTheory.MonoidalCategory.associator X Y Z').hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.leftUnitor Y).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<GOAL>f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) f) (CategoryTheory.MonoidalCategory.leftUnitor X').hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' : C<VAR>f : X ⟶ X'<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategory.rightUnitor X').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f (𝟙_ C)) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom)
<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.whiskerLeft (𝟙_ C) f = CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ 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.whiskerRight f (𝟙_ C) = CategoryTheory.MonoidalCategory.whiskerRight g (𝟙_ C) ↔ f = g
<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).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)) = 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