ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>h : ∀ ⦃X₁' X₂' X₃' : C⦄ (u₁₂' : X₁' ⟶ X₂') (u₂₃' : X₂' ⟶ X₃'), ∃ X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ u₁₂ u₂₃ e₁ e₂ e₃, ∃ (_ : CategoryTheory.CategoryStruct.comp u₁₂' e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom u₁₂) (_ : CategoryTheory.CategoryStruct.comp u₂₃' e₃.hom = CategoryTheory.CategoryStruct.comp e₂.hom u₂₃), ∃ v₁₂ w₁₂, ∃ (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), ∃ v₂₃ w₂₃, ∃ (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), ∃ v₁₃ w₁₃, ∃ (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk (CategoryTheory.CategoryStruct.comp u₁₂ u₂₃) v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (CategoryTheory.Triangulated.Octahedron ⋯ h₁₂ h₂₃ h₁₃)<GOAL>CategoryTheory.IsTriangulated C
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ Mon_ C<GOAL>(Mon_.limit F).X = CategoryTheory.Limits.limit (F ⋙ Mon_.forget C)
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ Mon_ C<GOAL>(Mon_.limit F).one = CategoryTheory.Limits.limit.lift (F ⋙ Mon_.forget C) ((CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).one).obj { pt := 𝟙_ C, π := { app := fun j => 𝟙 (𝟙_ C), naturality := ⋯ } })
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ Mon_ C<GOAL>(Mon_.limit F).mul = CategoryTheory.Limits.limit.lift (F ⋙ Mon_.forget C) ((CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).mul).obj { pt := CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.Limits.limit (F ⋙ Mon_.forget C)) (CategoryTheory.Limits.limit (F ⋙ Mon_.forget C)), π := { app := fun j => CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.limit.π (F ⋙ Mon_.forget C) j) (CategoryTheory.Limits.limit.π (F ⋙ Mon_.forget C) j), naturality := ⋯ } })
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ Mon_ C<GOAL>(Mon_.limitCone F).pt = Mon_.limit F
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ Mon_ C<VAR>j : J<GOAL>((Mon_.limitCone F).π.app j).hom = CategoryTheory.Limits.limit.π (F ⋙ Mon_.forget C) j
<VAR>J : Type w<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : J ⥤ Mon_ C<VAR>s : CategoryTheory.Limits.Cone F<GOAL>((Mon_.limitConeIsLimit F).lift s).hom = CategoryTheory.Limits.limit.lift (F ⋙ Mon_.forget C) ((Mon_.forget C).mapCone s)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).hom ≫ (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X).hom (𝟙 Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).hom = (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).inv ≫ CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X).hom (𝟙 Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X).inv (𝟙 Y) ≫ (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.tensorHom (𝟙 X) (CategoryTheory.MonoidalCategory.rightUnitor Y).inv = (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv ≫ (CategoryTheory.MonoidalCategory.associator X Y (𝟙_ C)).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X).inv (𝟙 Y) = (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X Y)).inv ≫ (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X Y).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv ≫ CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).inv (𝟙 Z) ≫ (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom = CategoryTheory.MonoidalCategory.tensorHom (𝟙 W) (CategoryTheory.MonoidalCategory.associator X Y Z).hom ≫ (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom = (CategoryTheory.MonoidalCategory.rightUnitor (𝟙_ C)).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv = (CategoryTheory.MonoidalCategory.rightUnitor (𝟙_ C)).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom ≫ CategoryTheory.MonoidalCategory.tensorHom (𝟙 W) (CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv ≫ CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).hom (𝟙 Z) ≫ (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv ≫ CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).hom (𝟙 Z) = (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom ≫ CategoryTheory.MonoidalCategory.tensorHom (𝟙 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>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : C ⥤ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.FunctorCategory.tensorObj F G).obj X = F.obj X ⊗ G.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : C ⥤ D<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Monoidal.FunctorCategory.tensorObj F G).map f = F.map f ⊗ G.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G F' G' : C ⥤ D<VAR>α : F ⟶ G<VAR>β : F' ⟶ G'<VAR>X : C<GOAL>(CategoryTheory.Monoidal.FunctorCategory.tensorHom α β).app X = α.app X ⊗ β.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F' G' : C ⥤ D<VAR>F : C ⥤ D<VAR>β : F' ⟶ G'<VAR>X : C<GOAL>(CategoryTheory.Monoidal.FunctorCategory.whiskerLeft F β).app X = F.obj X ◁ β.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>F' : C ⥤ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.FunctorCategory.whiskerRight α F').app X = α.app X ▷ F'.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : C<GOAL>(𝟙_ (C ⥤ D)).obj X = 𝟙_ D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(𝟙_ (C ⥤ D)).map f = 𝟙 (𝟙_ D)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : C ⥤ D<VAR>X : C<GOAL>(F ⊗ G).obj X = F.obj X ⊗ G.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(F ⊗ G).map f = F.map f ⊗ G.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G F' G' : C ⥤ D<VAR>α : F ⟶ G<VAR>β : F' ⟶ G'<VAR>X : C<GOAL>(α ⊗ β).app X = α.app X ⊗ β.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F F' G' : C ⥤ D<VAR>β : F' ⟶ G'<VAR>X : C<GOAL>(F ◁ β).app X = F.obj X ◁ β.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G F' : C ⥤ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(α ▷ F').app X = α.app X ▷ F'.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ D<VAR>X : C<GOAL>(λ_ F).hom.app X = (λ_ (F.obj X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ D<VAR>X : C<GOAL>(λ_ F).inv.app X = (λ_ (F.obj X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ D<VAR>X : C<GOAL>(ρ_ F).hom.app X = (ρ_ (F.obj X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ D<VAR>X : C<GOAL>(ρ_ F).inv.app X = (ρ_ (F.obj X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G H : C ⥤ D<VAR>X : C<GOAL>(α_ F G H).hom.app X = (α_ (F.obj X) (G.obj X) (H.obj X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F G H : C ⥤ D<VAR>X : C<GOAL>(α_ F G H).inv.app X = (α_ (F.obj X) (G.obj X) (H.obj X)).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>t : CategoryTheory.Limits.BinaryFan P Q<GOAL>t.swap.fst = t.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>t : CategoryTheory.Limits.BinaryFan P Q<GOAL>t.swap.snd = t.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>t : CategoryTheory.Limits.BinaryFan P Q<VAR>I : CategoryTheory.Limits.IsLimit t<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair Q P)<GOAL>I.swapBinaryFan.lift s = I.lift (CategoryTheory.Limits.BinaryFan.swap s)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P Q : C<VAR>CategoryTheory.Limits.HasBinaryProduct P Q<GOAL>CategoryTheory.Limits.HasBinaryProduct Q P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>sXY : CategoryTheory.Limits.BinaryFan X Y<VAR>sYZ : CategoryTheory.Limits.BinaryFan Y Z<VAR>Q : CategoryTheory.Limits.IsLimit sYZ<VAR>s : CategoryTheory.Limits.BinaryFan sXY.pt Z<GOAL>(CategoryTheory.Limits.BinaryFan.assoc Q s).fst = CategoryTheory.CategoryStruct.comp s.fst sXY.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>sXY : CategoryTheory.Limits.BinaryFan X Y<VAR>sYZ : CategoryTheory.Limits.BinaryFan Y Z<VAR>Q : CategoryTheory.Limits.IsLimit sYZ<VAR>s : CategoryTheory.Limits.BinaryFan sXY.pt Z<GOAL>(CategoryTheory.Limits.BinaryFan.assoc Q s).snd = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp s.fst sXY.snd) s.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>sXY : CategoryTheory.Limits.BinaryFan X Y<VAR>P : CategoryTheory.Limits.IsLimit sXY<VAR>sYZ : CategoryTheory.Limits.BinaryFan Y Z<VAR>s : CategoryTheory.Limits.BinaryFan X sYZ.pt<GOAL>(CategoryTheory.Limits.BinaryFan.assocInv P s).fst = P.lift (CategoryTheory.Limits.BinaryFan.mk s.fst (CategoryTheory.CategoryStruct.comp s.snd sYZ.fst))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>sXY : CategoryTheory.Limits.BinaryFan X Y<VAR>P : CategoryTheory.Limits.IsLimit sXY<VAR>sYZ : CategoryTheory.Limits.BinaryFan Y Z<VAR>s : CategoryTheory.Limits.BinaryFan X sYZ.pt<GOAL>(CategoryTheory.Limits.BinaryFan.assocInv P s).snd = CategoryTheory.CategoryStruct.comp s.snd sYZ.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>sXY : CategoryTheory.Limits.BinaryFan X Y<VAR>P : CategoryTheory.Limits.IsLimit sXY<VAR>sYZ : CategoryTheory.Limits.BinaryFan Y Z<VAR>Q : CategoryTheory.Limits.IsLimit sYZ<VAR>s : CategoryTheory.Limits.BinaryFan sXY.pt Z<VAR>R : CategoryTheory.Limits.IsLimit s<VAR>t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X sYZ.pt)<GOAL>(P.assoc Q R).lift t = R.lift (CategoryTheory.Limits.BinaryFan.assocInv P t)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>t : CategoryTheory.Limits.BinaryFan s.pt X<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryFan.leftUnitor P Q).hom = t.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>t : CategoryTheory.Limits.BinaryFan s.pt X<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryFan.leftUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }) (CategoryTheory.CategoryStruct.id { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }.pt))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>t : CategoryTheory.Limits.BinaryFan X s.pt<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryFan.rightUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X) (P.lift { pt := X, π := { app := fun x => x.as.elim, naturality := ⋯ } }))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)<VAR>P : CategoryTheory.Limits.IsLimit s<VAR>t : CategoryTheory.Limits.BinaryFan X s.pt<VAR>Q : CategoryTheory.Limits.IsLimit t<GOAL>(CategoryTheory.Limits.BinaryFan.rightUnitor P Q).hom = t.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X₁ X₂ : C<GOAL>CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X₁ X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<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.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f₁ f₂) (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ g₁ g₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y) Z).hom (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id W) (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ W X) Y Z).hom (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ W X (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ Y Z)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) = CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (CategoryTheory.CategoryStruct.id Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id 𝒯.cone.pt) f) (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f (CategoryTheory.CategoryStruct.id 𝒯.cone.pt)) (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)<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.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f₁ f₂) f₃) (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f₁ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f₂ f₃))
<VAR>M : Type u<VAR>Monoid M<VAR>X Y : CategoryTheory.Discrete M<GOAL>(X ⊗ Y).as = X.as * Y.as
<VAR>M : Type u<VAR>AddMonoid M<VAR>X Y Z : CategoryTheory.Discrete M<GOAL>α_ X Y Z = CategoryTheory.Discrete.eqToIso ⋯
<VAR>M : Type u<VAR>AddMonoid M<VAR>X : CategoryTheory.Discrete M<GOAL>λ_ X = CategoryTheory.Discrete.eqToIso ⋯
<VAR>M : Type u<VAR>Monoid M<VAR>X : CategoryTheory.Discrete M<GOAL>λ_ X = CategoryTheory.Discrete.eqToIso ⋯
<VAR>M : Type u<VAR>AddMonoid M<VAR>X Y : CategoryTheory.Discrete M<GOAL>(X ⊗ Y).as = X.as + Y.as
<VAR>M : Type u<VAR>Monoid M<VAR>X Y Z : CategoryTheory.Discrete M<GOAL>α_ X Y Z = CategoryTheory.Discrete.eqToIso ⋯
<VAR>M : Type u<VAR>Monoid M<VAR>X : CategoryTheory.Discrete M<GOAL>ρ_ X = CategoryTheory.Discrete.eqToIso ⋯
<VAR>M : Type u<VAR>AddMonoid M<VAR>X : CategoryTheory.Discrete M<GOAL>ρ_ X = CategoryTheory.Discrete.eqToIso ⋯
<VAR>M : Type u<VAR>Monoid M<GOAL>(𝟙_ (CategoryTheory.Discrete M)).as = 1
<VAR>M : Type u<VAR>AddMonoid M<GOAL>(𝟙_ (CategoryTheory.Discrete M)).as = 0
<VAR>M : Type u<VAR>AddMonoid M<VAR>N : Type u'<VAR>AddMonoid N<VAR>F : M →+ N<VAR>X Y : CategoryTheory.Discrete M<GOAL>(CategoryTheory.Discrete.addMonoidalFunctor F).μ X Y = CategoryTheory.Discrete.eqToHom ⋯
<VAR>M : Type u<VAR>AddMonoid M<VAR>N : Type u'<VAR>AddMonoid N<VAR>F : M →+ N<GOAL>∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.addMonoidalFunctor F).map f = CategoryTheory.Discrete.eqToHom ⋯
<VAR>M : Type u<VAR>Monoid M<VAR>N : Type u'<VAR>Monoid N<VAR>F : M →* N<VAR>X Y : CategoryTheory.Discrete M<GOAL>(CategoryTheory.Discrete.monoidalFunctor F).μ X Y = CategoryTheory.Discrete.eqToHom ⋯
<VAR>M : Type u<VAR>AddMonoid M<VAR>N : Type u'<VAR>AddMonoid N<VAR>F : M →+ N<VAR>X : CategoryTheory.Discrete M<GOAL>((CategoryTheory.Discrete.addMonoidalFunctor F).obj X).as = F X.as
<VAR>M : Type u<VAR>AddMonoid M<VAR>N : Type u'<VAR>AddMonoid N<VAR>F : M →+ N<GOAL>(CategoryTheory.Discrete.addMonoidalFunctor F).ε = CategoryTheory.Discrete.eqToHom ⋯
<VAR>M : Type u<VAR>Monoid M<VAR>N : Type u'<VAR>Monoid N<VAR>F : M →* N<VAR>X : CategoryTheory.Discrete M<GOAL>((CategoryTheory.Discrete.monoidalFunctor F).obj X).as = F X.as
<VAR>M : Type u<VAR>Monoid M<VAR>N : Type u'<VAR>Monoid N<VAR>F : M →* N<GOAL>∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.monoidalFunctor F).map f = CategoryTheory.Discrete.eqToHom ⋯
<VAR>M : Type u<VAR>Monoid M<VAR>N : Type u'<VAR>Monoid N<VAR>F : M →* N<GOAL>(CategoryTheory.Discrete.monoidalFunctor F).ε = CategoryTheory.Discrete.eqToHom ⋯
<GOAL>∀ {X Y : CategoryTheory.InducedCategory (Type u_1) CategoryTheory.Bundled.α} (f : X ⟶ Y) (a : ↑X), FintypeCat.incl.map f a = f a
<VAR>self : CategoryTheory.Bundled Fintype<GOAL>FintypeCat.incl.obj self = ↑self
<VAR>X : FintypeCat<VAR>x : ↑X<GOAL>𝟙 X x = x
<VAR>X Y Z : FintypeCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : ↑X<GOAL>(f ≫ g) x = g (f x)
<VAR>X Y : FintypeCat<VAR>f : X ≅ Y<VAR>x : ↑X<GOAL>f.inv (f.hom x) = x
<VAR>X Y : FintypeCat<VAR>f : X ≅ Y<VAR>y : ↑Y<GOAL>f.hom (f.inv y) = y
<VAR>A B : FintypeCat<VAR>e : ↑A ≃ ↑B<VAR>a : ↑B<GOAL>(FintypeCat.equivEquivIso e).inv a = e.symm a
<VAR>A B : FintypeCat<VAR>i : A ≅ B<GOAL>∀ (a : ↑A), (FintypeCat.equivEquivIso.symm i) a = i.hom a
<VAR>A B : FintypeCat<VAR>i : A ≅ B<GOAL>∀ (a : ↑B), (FintypeCat.equivEquivIso.symm i).symm a = i.inv a
<VAR>A B : FintypeCat<VAR>e : ↑A ≃ ↑B<VAR>a : ↑A<GOAL>(FintypeCat.equivEquivIso e).hom a = e a