ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₂ = 𝟙 X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₂ = 𝟙 X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₂ = 𝟙 X.obj₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₁ = 𝟙 X.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app X.obj₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>(CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₁ = 𝟙 X.obj₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<GOAL>(CategoryTheory.Pretriangulated.triangleRotation C).functor = CategoryTheory.Pretriangulated.rotate C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<GOAL>(CategoryTheory.Pretriangulated.triangleRotation C).unitIso = CategoryTheory.Pretriangulated.rotCompInvRot
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<GOAL>(CategoryTheory.Pretriangulated.triangleRotation C).counitIso = CategoryTheory.Pretriangulated.invRotCompRot
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<GOAL>(CategoryTheory.Pretriangulated.triangleRotation C).inverse = CategoryTheory.Pretriangulated.invRotate C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.Subcategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → self.P T.obj₁ → self.P T.obj₃ → CategoryTheory.isoClosure self.P T.obj₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.Subcategory C<VAR>X : C<VAR>n : ℤ<GOAL>self.P X → self.P ((CategoryTheory.shiftFunctor C n).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.Subcategory C<GOAL>∃ Z, ∃ (_ : CategoryTheory.Limits.IsZero Z), self.P Z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>CategoryTheory.ClosedUnderIsomorphisms S.P<GOAL>S.P 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>CategoryTheory.ClosedUnderIsomorphisms S.P<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₁ : S.P T.obj₁<VAR>h₃ : S.P T.obj₃<GOAL>S.P T.obj₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>S.W f ↔ ∃ Z g h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), S.P Z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>S.W g ↔ ∃ X f h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), S.P X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : S.P T.obj₃<GOAL>S.W T.mor₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h : S.P T.obj₁<GOAL>S.W T.mor₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<GOAL>S.isoClosure.W = S.W
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>S.W f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>n : ℤˣ<GOAL>S.W (n • f) ↔ S.W f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>hf : S.W f<VAR>n : ℤ<GOAL>S.W ((CategoryTheory.shiftFunctor C n).map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>n : ℤ<VAR>hf : S.W ((CategoryTheory.shiftFunctor C n).map f)<GOAL>S.W f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>CategoryTheory.ClosedUnderIsomorphisms S.P<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<GOAL>S.W T.mor₁ ↔ S.P T.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>CategoryTheory.ClosedUnderIsomorphisms S.P<VAR>h₂ : S.P T.obj₂<VAR>h₃ : S.P T.obj₃<GOAL>S.P T.obj₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>CategoryTheory.ClosedUnderIsomorphisms S.P<VAR>h₁ : S.P T.obj₁<VAR>h₂ : S.P T.obj₂<GOAL>S.P T.obj₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₂ : S.P T.obj₂<VAR>h₃ : S.P T.obj₃<GOAL>CategoryTheory.isoClosure S.P T.obj₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.Preadditive C<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>S : CategoryTheory.Triangulated.Subcategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle C<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>h₁ : S.P T.obj₁<VAR>h₂ : S.P T.obj₂<GOAL>CategoryTheory.isoClosure S.P T.obj₃
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_8, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<GOAL>∀ {X Y : CategoryTheory.GradedObject I C₁} (φ : X ⟶ Y) (Y_1 : CategoryTheory.GradedObject J C₂) (ij : I × J), ((CategoryTheory.GradedObject.mapBifunctor F I J).map φ).app Y_1 ij = (F.map (φ ij.1)).app (Y_1 ij.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_8, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>X : CategoryTheory.GradedObject I C₁<VAR>Y : CategoryTheory.GradedObject J C₂<VAR>ij : I × J<GOAL>((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y ij = (F.obj (X ij.1)).obj (Y ij.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_8, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>X : CategoryTheory.GradedObject I C₁<GOAL>∀ {X_1 Y : CategoryTheory.GradedObject J C₂} (φ : X_1 ⟶ Y) (ij : I × J), ((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).map φ ij = (F.obj (X ij.1)).map (φ ij.2)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X₁ X₂ : CategoryTheory.GradedObject I C₁<VAR>f : X₁ ⟶ X₂<VAR>Y₁ Y₂ : CategoryTheory.GradedObject J C₂<VAR>g : Y₁ ⟶ Y₂<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p<VAR>i : I<VAR>j : J<VAR>k : K<VAR>h : p (i, j) = k<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₁ Y₁ i j k h) (CategoryTheory.GradedObject.mapBifunctorMapMap F p f g k) = CategoryTheory.CategoryStruct.comp ((F.map (f i)).app (Y₁ j)) (CategoryTheory.CategoryStruct.comp ((F.obj (X₂ i)).map (g j)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X₂ Y₂ i j k h))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_9, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X : CategoryTheory.GradedObject I C₁<VAR>Y : CategoryTheory.GradedObject J C₂<VAR>A : C₃<VAR>k : K<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>f g : CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k ⟶ A<VAR>h : ∀ (i : I) (j : J) (hij : p (i, j) = k), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) g<GOAL>f = g
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_9, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X : CategoryTheory.GradedObject I C₁<VAR>Y : CategoryTheory.GradedObject J C₂<VAR>A : C₃<VAR>k : K<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)<VAR>i : I<VAR>j : J<VAR>hij : p (i, j) = k<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij) (CategoryTheory.GradedObject.mapBifunctorMapObjDesc f) = f i j hij
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X₁ X₂ : CategoryTheory.GradedObject I C₁<VAR>Y₁ Y₂ : CategoryTheory.GradedObject J C₂<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p<VAR>e : X₁ ≅ X₂<VAR>e' : Y₁ ≅ Y₂<VAR>i : K<GOAL>(CategoryTheory.GradedObject.mapBifunctorMapMapIso F p e e').inv i = CategoryTheory.GradedObject.mapBifunctorMapMap F p e.inv e'.inv i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X₁ X₂ : CategoryTheory.GradedObject I C₁<VAR>Y₁ Y₂ : CategoryTheory.GradedObject J C₂<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p<VAR>e : X₁ ≅ X₂<VAR>e' : Y₁ ≅ Y₂<VAR>i : K<GOAL>(CategoryTheory.GradedObject.mapBifunctorMapMapIso F p e e').hom i = CategoryTheory.GradedObject.mapBifunctorMapMap F p e.hom e'.hom i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂), (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>X : CategoryTheory.GradedObject I C₁<VAR>Y : CategoryTheory.GradedObject J C₂<GOAL>((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).obj Y = CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂), (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>X : CategoryTheory.GradedObject I C₁<GOAL>∀ {X_1 Y : CategoryTheory.GradedObject J C₂} (ψ : X_1 ⟶ Y) (i : K), ((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).map ψ i = CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id X) ψ i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} C₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂), (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>X₁ X₂ : CategoryTheory.GradedObject I C₁<VAR>φ : X₁ ⟶ X₂<VAR>Y : CategoryTheory.GradedObject J C₂<VAR>i : K<GOAL>((CategoryTheory.GradedObject.mapBifunctorMap F p).map φ).app Y i = CategoryTheory.GradedObject.mapBifunctorMapMap F p φ (CategoryTheory.CategoryStruct.id Y) i
<VAR>R : Type u_1<VAR>Semiring R<VAR>C : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.Category.{u_5, u_3} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α : F ⟶ G<GOAL>(CategoryTheory.NatTrans.appLinearMap X) α = α.app X
<VAR>R : Type u_1<VAR>Semiring R<VAR>C : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_5, u_2} C<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>r : R<VAR>α : F ⟶ G<GOAL>(r • α).app X = r • α.app X
<VAR>C : Type u<VAR>X : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C<GOAL>CategoryTheory.FreeMonoidalCategory.inclusion.obj X = CategoryTheory.FreeMonoidalCategory.inclusionObj X.as
<VAR>C : Type u<VAR>X Y : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.FreeMonoidalCategory.inclusion.map f = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C<GOAL>(𝟙_ (CategoryTheory.FreeMonoidalCategory C)).normalizeObj n = n
<VAR>C : Type u<VAR>X Y : CategoryTheory.FreeMonoidalCategory C<VAR>n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).normalizeObj n = Y.normalizeObj (X.normalizeObj n)
<VAR>C : Type u<VAR>X Y : CategoryTheory.FreeMonoidalCategory C<VAR>f : X ⟶ Y<VAR>n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C<GOAL>((CategoryTheory.FreeMonoidalCategory.tensorFunc C).map f).app n = CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as }) f
<VAR>C : Type u<VAR>Z : CategoryTheory.FreeMonoidalCategory C<VAR>n n' : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C<VAR>f : n ⟶ n'<GOAL>((CategoryTheory.FreeMonoidalCategory.tensorFunc C).obj Z).map f = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.FreeMonoidalCategory.inclusion.map f) Z
<VAR>C : Type u<VAR>X : CategoryTheory.FreeMonoidalCategory C<VAR>n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C<GOAL>CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X n = CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n.as
<VAR>C : Type u<VAR>X Y : CategoryTheory.FreeMonoidalCategory C<VAR>n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C<GOAL>CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C (CategoryTheory.MonoidalCategory.tensorObj X Y) n = (CategoryTheory.MonoidalCategory.associator (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as }) X Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X n) Y ≪≫ CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C Y { as := X.normalizeObj n.as }
<VAR>C : Type u<VAR>n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C<GOAL>CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C (𝟙_ (CategoryTheory.FreeMonoidalCategory C)) n = CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := n.as })
<VAR>C : Type u<VAR>n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C<VAR>X Y : CategoryTheory.FreeMonoidalCategory C<VAR>f : X ⟶ Y<GOAL>X.normalizeObj n = Y.normalizeObj n
<VAR>C : Type u<VAR>n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C<VAR>X Y : CategoryTheory.FreeMonoidalCategory C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.FreeMonoidalCategory.inclusionObj n) f) (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C Y n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n).hom (CategoryTheory.FreeMonoidalCategory.inclusion.map (CategoryTheory.eqToHom ⋯))