ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<GOAL>(CategoryTheory.Comonad.ForgetCreatesLimits'.newCone c).π = CategoryTheory.CategoryStruct.comp c.π CategoryTheory.Comonad.ForgetCreatesLimits'.γ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor<VAR>j : J<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t) (T.map (c.π.app j)) = CategoryTheory.CategoryStruct.comp (c.π.app j) (D.obj j).a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<GOAL>(CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t).a = CategoryTheory.Comonad.ForgetCreatesLimits'.lambda c t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<GOAL>(CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t).A = c.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<GOAL>(CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone c t).pt = CategoryTheory.Comonad.ForgetCreatesLimits'.conePoint c t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<VAR>j : J<GOAL>((CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone c t).π.app j).f = c.π.app j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>c : CategoryTheory.Limits.Cone (D.comp T.forget)<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor<VAR>CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor<VAR>s : CategoryTheory.Limits.Cone D<GOAL>((CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit c t).lift s).f = t.lift (T.forget.mapCone s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>T : CategoryTheory.Comonad C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape J T.toFunctor<VAR>D : CategoryTheory.Functor J T.Coalgebra<VAR>CategoryTheory.Limits.HasLimit (D.comp T.forget)<GOAL>CategoryTheory.Limits.HasLimit D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : CategoryTheory.Functor J D<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasColimit (F.comp R)<VAR>CategoryTheory.Coreflective R<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Coreflective R<GOAL>CategoryTheory.Limits.HasColimitsOfShape J D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C<VAR>CategoryTheory.Coreflective R<GOAL>CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₂, u₂} D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Coreflective R<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>R : CategoryTheory.Functor D C<VAR>CategoryTheory.Coreflective R<VAR>CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₁, u₁} C<GOAL>CategoryTheory.Limits.HasLimitsOfSize.{v, u, v₂, u₂} D
<VAR>α : Type u_1<VAR>Fintype α<VAR>CategoryTheory.SmallCategory α<VAR>CategoryTheory.FinCategory α<GOAL>∀ {X Y Z : CategoryTheory.FinCategory.AsType α} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = (Fintype.equivFin (X ⟶ Z)) (CategoryTheory.CategoryStruct.comp ((Fintype.equivFin (X ⟶ Y)).symm f) ((Fintype.equivFin (Y ⟶ Z)).symm g))
<VAR>α : Type u_1<VAR>Fintype α<VAR>CategoryTheory.SmallCategory α<VAR>CategoryTheory.FinCategory α<VAR>i : CategoryTheory.FinCategory.AsType α<GOAL>CategoryTheory.CategoryStruct.id i = (Fintype.equivFin (i ⟶ i)) (CategoryTheory.CategoryStruct.id i)
<VAR>α : Type u_1<VAR>Fintype α<VAR>CategoryTheory.SmallCategory α<VAR>CategoryTheory.FinCategory α<VAR>X Y : CategoryTheory.FinCategory.AsType α<VAR>a : Fin (Fintype.card (X ⟶ Y))<GOAL>(CategoryTheory.FinCategory.asTypeToObjAsType α).map a = (Fintype.equivFin (X ⟶ Y)).symm a
<VAR>α : Type u_1<VAR>Fintype α<VAR>CategoryTheory.SmallCategory α<VAR>CategoryTheory.FinCategory α<VAR>a : CategoryTheory.FinCategory.AsType α<GOAL>(CategoryTheory.FinCategory.asTypeToObjAsType α).obj a = id a
<VAR>α : Type u_1<VAR>Fintype α<VAR>CategoryTheory.SmallCategory α<VAR>CategoryTheory.FinCategory α<VAR>X Y : CategoryTheory.FinCategory.ObjAsType α<VAR>a : X ⟶ Y<GOAL>(CategoryTheory.FinCategory.objAsTypeToAsType α).map a = (Fintype.equivFin (X ⟶ Y)) a
<VAR>α : Type u_1<VAR>Fintype α<VAR>CategoryTheory.SmallCategory α<VAR>CategoryTheory.FinCategory α<VAR>a : CategoryTheory.FinCategory.ObjAsType α<GOAL>(CategoryTheory.FinCategory.objAsTypeToAsType α).obj a = id a
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>DecidableEq J<VAR>j : J<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : J<VAR>h : i = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).inv ((CategoryTheory.GradedObject.single j).map f i) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).inv
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>DecidableEq J<VAR>j : J<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : J<VAR>h : i = j<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f i) (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).hom f
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>DecidableEq J<VAR>j : J<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).inv ((CategoryTheory.GradedObject.single j).map f j) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.GradedObject.singleObjApplyIso j Y).inv
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>DecidableEq J<VAR>j : J<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j) (CategoryTheory.GradedObject.singleObjApplyIso j Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).hom f
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>DecidableEq J<VAR>j : J<VAR>X : C<GOAL>(CategoryTheory.GradedObject.singleCompEval C j).inv.app X = (CategoryTheory.GradedObject.singleObjApplyIso j X).inv
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>DecidableEq J<VAR>j : J<VAR>X : C<GOAL>(CategoryTheory.GradedObject.singleCompEval C j).hom.app X = (CategoryTheory.GradedObject.singleObjApplyIso j X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>self : CategoryTheory.NatTrans F G<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α β : CategoryTheory.NatTrans F G<VAR>h : α = β<VAR>X : C<GOAL>α.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>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>(CategoryTheory.NatTrans.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G H : CategoryTheory.Functor C D<VAR>α : CategoryTheory.NatTrans F G<VAR>β : CategoryTheory.NatTrans G H<VAR>X : C<GOAL>(α.vcomp β).app X = CategoryTheory.CategoryStruct.comp (α.app 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_4, u_2} C<VAR>CategoryTheory.Category.{u_5, u_3} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.Linear R D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>self : CategoryTheory.Functor.Linear R F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>r : R<GOAL>F.map (r • f) = r • F.map f
<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 C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.Linear R D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Functor.Linear R F<VAR>X Y : C<VAR>r : R<VAR>f : X ⟶ Y<GOAL>F.map (r • f) = r • F.map f
<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 C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.Linear R D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Functor.Linear R F<VAR>X Y : C<VAR>r : Rˣ<VAR>f : X ⟶ Y<GOAL>F.map (r • f) = r • F.map f
<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 C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.Linear R D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Functor.Linear R F<VAR>X Y : C<GOAL>∀ (a : X ⟶ Y), (CategoryTheory.Functor.mapLinearMap R F) a = (↑F.mapAddHom).toFun a
<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 C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.Linear R D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Functor.Linear R F<VAR>X Y : C<GOAL>⇑(CategoryTheory.Functor.mapLinearMap R F) = F.map
<VAR>R : Type w<VAR>Semiring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>self : CategoryTheory.Linear R C<VAR>X Y Z : C<VAR>r : R<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(r • f) ≫ g = r • f ≫ g
<VAR>R : Type w<VAR>Semiring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>self : CategoryTheory.Linear R C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>r : R<VAR>g : Y ⟶ Z<GOAL>f ≫ (r • g) = r • f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type w<VAR>Semiring R<VAR>CategoryTheory.Linear R C<VAR>X Y : C<VAR>Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Linear.leftComp R Z f) g = f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type w<VAR>Semiring R<VAR>CategoryTheory.Linear R C<VAR>X : C<VAR>Y Z : C<VAR>g : Y ⟶ Z<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Linear.rightComp R X g) f = f ≫ g
<VAR>k : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>Semiring k<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear k C<VAR>X Y W Z : C<VAR>f₁ : X ≅ Y<VAR>f₂ : W ≅ Z<VAR>f : X ⟶ W<GOAL>(CategoryTheory.Linear.homCongr k f₁ f₂) f = (f₁.inv ≫ f) ≫ f₂.hom
<VAR>k : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>Semiring k<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear k C<VAR>X Y W Z : C<VAR>f₁ : X ≅ Y<VAR>f₂ : W ≅ Z<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.Linear.homCongr k f₁ f₂).symm f = f₁.hom ≫ f ≫ f₂.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type w<VAR>Semiring R<VAR>CategoryTheory.Linear R C<VAR>X Y Z : C<VAR>r : Rˣ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(r • f) ≫ g = r • f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type w<VAR>Semiring R<VAR>CategoryTheory.Linear R C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>r : Rˣ<VAR>g : Y ⟶ Z<GOAL>f ≫ (r • g) = r • f ≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>S : Type w<VAR>CommSemiring S<VAR>CategoryTheory.Linear S C<VAR>X Y Z : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Linear.comp X Y Z) f = CategoryTheory.Linear.leftComp S Z f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>CategoryTheory.Category.{u_15, u_1} C₁<VAR>CategoryTheory.Category.{u_14, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_5} C₃<VAR>CategoryTheory.Category.{u_11, u_6} C₄<VAR>CategoryTheory.Category.{u_13, u_3} C₁₂<VAR>CategoryTheory.Category.{u_17, u_4} C₂₃<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₁₂ : Type u_3<VAR>C₂₃ : Type u_4<VAR>C₃ : Type u_5<VAR>C₄ : Type u_6<VAR>CategoryTheory.Category.{u_13, u_1} C₁<VAR>CategoryTheory.Category.{u_15, u_2} C₂<VAR>CategoryTheory.Category.{u_14, u_5} C₃<VAR>CategoryTheory.Category.{u_11, u_6} C₄<VAR>CategoryTheory.Category.{u_17, u_3} C₁₂<VAR>CategoryTheory.Category.{u_12, u_4} C₂₃<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) = CategoryTheory.CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃)) (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D<VAR>φ : F ⟶ G<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>φ.app P = CategoryTheory.CategoryStruct.comp (F.map P.decompId_i) (CategoryTheory.CategoryStruct.comp (φ.app { X := P.X, p := CategoryTheory.CategoryStruct.id P.X, idem := ⋯ }) (G.map P.decompId_p))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi C} (f : X ⟶ Y), ((CategoryTheory.Idempotents.FunctorExtension₁.obj F).map f).f = (F.map f.f).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>((CategoryTheory.Idempotents.FunctorExtension₁.obj F).obj P).X = (F.obj P.X).X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>((CategoryTheory.Idempotents.FunctorExtension₁.obj F).obj P).p = (F.map P.p).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F G : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)<VAR>φ : F ⟶ G<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>((CategoryTheory.Idempotents.FunctorExtension₁.map φ).app P).f = CategoryTheory.CategoryStruct.comp (F.map P.p).f (φ.app P.X).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)<GOAL>(CategoryTheory.Idempotents.functorExtension₁ C D).obj F = CategoryTheory.Idempotents.FunctorExtension₁.obj F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<GOAL>∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)} (φ : X ⟶ Y), (CategoryTheory.Idempotents.functorExtension₁ C D).map φ = CategoryTheory.Idempotents.FunctorExtension₁.map φ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)<GOAL>∀ (X_1 : C), (((CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso C D).hom.app X).app X_1).f = (X.obj X_1).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)<GOAL>∀ (X_1 : C), (((CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso C D).inv.app X).app X_1).f = (X.obj X_1).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>(((CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso C D).hom.app X).app P).f = (X.map P.decompId_p).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>X : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>(((CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso C D).inv.app X).app P).f = (X.map P.decompId_i).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<GOAL>(CategoryTheory.Idempotents.karoubiUniversal₁ C D).unitIso = (CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso C D).symm
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<GOAL>(CategoryTheory.Idempotents.karoubiUniversal₁ C D).inverse = (CategoryTheory.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) (CategoryTheory.Idempotents.Karoubi D)).obj (CategoryTheory.Idempotents.toKaroubi C)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<GOAL>(CategoryTheory.Idempotents.karoubiUniversal₁ C D).functor = CategoryTheory.Idempotents.functorExtension₁ C D
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<GOAL>(CategoryTheory.Idempotents.karoubiUniversal₁ C D).counitIso = CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso C D