ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom = (CategoryTheory.MonoidalCategory.rightUnitor X.obj).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X Y Z : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator X.obj Y.obj Z.obj).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X : CategoryTheory.FullSubcategory P<GOAL>∀ (x x_1 : CategoryTheory.FullSubcategory P) (f : x ⟶ x_1), CategoryTheory.MonoidalCategory.whiskerLeft X f = CategoryTheory.MonoidalCategory.whiskerLeft X.obj f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X Y : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).obj = CategoryTheory.MonoidalCategory.tensorObj X.obj Y.obj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<GOAL>(𝟙_ (CategoryTheory.FullSubcategory P)).obj = 𝟙_ C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom = (CategoryTheory.MonoidalCategory.leftUnitor X.obj).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv = (CategoryTheory.MonoidalCategory.leftUnitor X.obj).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X Y : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.fullSubcategoryInclusion P).obj X) ((CategoryTheory.fullSubcategoryInclusion P).obj Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<GOAL>(CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toFunctor = CategoryTheory.fullSubcategoryInclusion P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<GOAL>(CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>P' : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P'<VAR>h : ∀ ⦃X : C⦄, P X → P' X<GOAL>(CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).ε = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.FullSubcategory P'))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>P' : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P'<VAR>h : ∀ ⦃X : C⦄, P X → P' X<VAR>X Y : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).obj X) ((CategoryTheory.FullSubcategory.map h).obj Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>P' : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P'<VAR>h : ∀ ⦃X : C⦄, P X → P' X<GOAL>(CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toFunctor = CategoryTheory.FullSubcategory.map h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.obj Y.obj)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>CategoryTheory.BraidedCategory C<GOAL>(CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>CategoryTheory.BraidedCategory C<VAR>self : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).obj self = self.obj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>P' : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P'<VAR>CategoryTheory.BraidedCategory C<VAR>h : ∀ ⦃X : C⦄, P X → P' X<GOAL>∀ {X Y : CategoryTheory.FullSubcategory P} (f : X ⟶ Y), (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>P' : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P'<VAR>CategoryTheory.BraidedCategory C<VAR>h : ∀ ⦃X : C⦄, P X → P' X<VAR>X : CategoryTheory.FullSubcategory P<GOAL>((CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).obj X).obj = X.obj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>P' : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P'<VAR>CategoryTheory.BraidedCategory C<VAR>h : ∀ ⦃X : C⦄, P X → P' X<VAR>X Y : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).obj X) ((CategoryTheory.FullSubcategory.map h).obj Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>P' : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P'<VAR>CategoryTheory.BraidedCategory C<VAR>h : ∀ ⦃X : C⦄, P X → P' X<GOAL>(CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).ε = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.FullSubcategory P'))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalClosed C<VAR>self : CategoryTheory.MonoidalCategory.ClosedPredicate P<VAR>X Y : C<GOAL>P X → P Y → P ((CategoryTheory.ihom X).obj Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>CategoryTheory.MonoidalClosed C<VAR>CategoryTheory.MonoidalCategory.ClosedPredicate P<VAR>X Y : CategoryTheory.FullSubcategory P<GOAL>((CategoryTheory.ihom X).obj Y).obj = (CategoryTheory.ihom X.obj).obj Y.obj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>CategoryTheory.MonoidalClosed C<VAR>CategoryTheory.MonoidalCategory.ClosedPredicate P<VAR>X : CategoryTheory.FullSubcategory P<VAR>Y Z : CategoryTheory.FullSubcategory P<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.ihom X).map f = (CategoryTheory.ihom X.obj).map f
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>A : C<VAR>j : I<VAR>f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A<VAR>h : ∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) g<GOAL>f = g
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>A : C<VAR>k : I<VAR>f : (i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategory.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)<VAR>i₁ i₂ : I<VAR>hi : i₁ + i₂ = k<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ k hi) (CategoryTheory.GradedObject.Monoidal.tensorObjDesc f) = f i₁ i₂ hi
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<VAR>X₁.HasTensor Y₁<VAR>X₂.HasTensor Y₂<VAR>i₁ i₂ i₁₂ : I<VAR>h : i₁ + i₂ = i₁₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h) (CategoryTheory.GradedObject.Monoidal.tensorHom f g i₁₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f i₁) (g i₂)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.GradedObject I C<VAR>X.HasTensor Y<GOAL>CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.GradedObject.Monoidal.tensorObj X Y)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C<VAR>f₁ : X₁ ⟶ X₂<VAR>f₂ : X₂ ⟶ X₃<VAR>g₁ : Y₁ ⟶ Y₂<VAR>g₂ : Y₂ ⟶ Y₃<VAR>X₁.HasTensor Y₁<VAR>X₂.HasTensor Y₂<VAR>X₃.HasTensor Y₃<GOAL>CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ g₁) (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ g₂)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ Y₁ Y₂ : CategoryTheory.GradedObject I C<VAR>f : X₁ ⟶ X₂<VAR>g : Y₁ ⟶ Y₂<VAR>X₁.HasTensor Y₁<VAR>X₂.HasTensor Y₂<VAR>X₂.HasTensor Y₁<GOAL>CategoryTheory.GradedObject.Monoidal.tensorHom f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.whiskerRight f Y₁) (CategoryTheory.GradedObject.Monoidal.whiskerLeft X₂ g)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₂.HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<VAR>i₂₃ : I<VAR>h' : i₂ + i₃ = i₂₃<GOAL>CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (X₁ i₁) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h')) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) i₁ i₂₃ j ⋯)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<VAR>i₁₂ : I<VAR>h' : i₁ + i₂ = i₁₂<GOAL>CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ i₁₂ h') (X₃ i₃)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ i₁₂ i₃ j ⋯)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₂.HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C<VAR>Y₂.HasTensor Y₃<VAR>Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃) j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (f₁ i₁) (CategoryTheory.MonoidalCategory.tensorHom (f₂ i₂) (f₃ i₃))) (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C<VAR>Y₁.HasTensor Y₂<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃ j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom (f₁ i₁) (f₂ i₂)) (f₃ i₃)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₂.HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>j : I<VAR>A : C<VAR>f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j ⟶ A<VAR>H : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>h : ∀ (i₁ i₂ i₃ : I) (hi : i₁ + i₂ + i₃ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j hi) g<GOAL>f = g
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>j : I<VAR>A : C<VAR>f g : CategoryTheory.GradedObject.Monoidal.tensorObj (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ j ⟶ A<VAR>H : X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) g<GOAL>f = g
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>X₂.HasTensor X₃<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).hom (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>X₂.HasTensor X₃<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>i₁ i₂ i₃ j : I<VAR>h : i₁ + i₂ + i₃ = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).inv j) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (X₁ i₁) (X₂ i₂) (X₃ i₃)).inv (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₁.HasTensor X₂<VAR>X₂.HasTensor X₃<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : CategoryTheory.GradedObject I C<VAR>Y₁.HasTensor Y₂<VAR>Y₂.HasTensor Y₃<VAR>(CategoryTheory.GradedObject.Monoidal.tensorObj Y₁ Y₂).HasTensor Y₃<VAR>Y₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj Y₂ Y₃)<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<VAR>X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃<VAR>Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ f₂) f₃) (CategoryTheory.GradedObject.Monoidal.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃).hom (CategoryTheory.GradedObject.Monoidal.tensorHom f₁ (CategoryTheory.GradedObject.Monoidal.tensorHom f₂ f₃))
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ : CategoryTheory.GradedObject I C<VAR>X₂.HasTensor X₃<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)<VAR>j : I<VAR>A : C<VAR>Z : C<VAR>f g : CategoryTheory.MonoidalCategory.tensorObj Z (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) j) ⟶ A<VAR>H : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>hZ : CategoryTheory.GradedObject.HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j<VAR>h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft Z (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft Z (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)) g<GOAL>f = g
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C<VAR>X₃.HasTensor X₄<VAR>X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))<VAR>i₁ i₂ i₃ i₄ j : I<VAR>h : i₁ + i₂ + i₃ + i₄ = j<VAR>i₂₃₄ : I<VAR>hi : i₂ + i₃ + i₄ = i₂₃₄<GOAL>CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (X₁ i₁) (CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ hi)) (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)) i₁ i₂₃₄ j ⋯)
<VAR>I : Type u<VAR>AddMonoid I<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C<VAR>X₃.HasTensor X₄<VAR>X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)<VAR>X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))<VAR>j : I<VAR>A : C<VAR>f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)) j ⟶ A<VAR>X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>H : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>h : ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h) g<GOAL>f = g