ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>(𝟙_ (CategoryTheory.Dial C)).src = ⊤_ C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>∀ {X₁ X₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Dial C), (CategoryTheory.MonoidalCategory.whiskerRight f Y).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>∀ (x x_1 : CategoryTheory.Dial C) (f : x ⟶ x_1), (CategoryTheory.MonoidalCategory.whiskerLeft X f).f = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X.src) f.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>∀ (x x_1 : CategoryTheory.Dial C) (f : x ⟶ x_1), (CategoryTheory.MonoidalCategory.whiskerLeft X f).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) f.F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>∀ {X₁ X₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Dial C), (CategoryTheory.MonoidalCategory.whiskerRight f Y).f = CategoryTheory.Limits.prod.map f.f (CategoryTheory.CategoryStruct.id Y.src)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>(𝟙_ (CategoryTheory.Dial C)).rel = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj X.rel ⊓ (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj Y.rel
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<GOAL>∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), (CategoryTheory.MonoidalCategory.tensorHom f g).F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.f = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.f = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X.src) (CategoryTheory.Limits.terminal.from X.src)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.f = CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X₁ X₂ : CategoryTheory.Dial C<GOAL>CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.Dial C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom f₁ f₂) (CategoryTheory.Dial.tensorHom g₁ g₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.Dial C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (CategoryTheory.Dial.tensorHom f₁ f₂) f₃) (Y₁.associator Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (X₁.associator X₂ X₃).hom (CategoryTheory.Dial.tensorHom f₁ (CategoryTheory.Dial.tensorHom f₂ f₃))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Dial C))) f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Dial C)))) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>W X Y Z : CategoryTheory.Dial C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (W.associator X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (W.associator (X.tensorObj Y) Z).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id W) (X.associator Y Z).hom)) = CategoryTheory.CategoryStruct.comp ((W.tensorObj X).associator Y Z).hom (W.associator X (Y.tensorObj Z)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>CategoryTheory.CategoryStruct.comp (X.associator (𝟙_ (CategoryTheory.Dial C)) Y).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id X) Y.leftUnitor.hom) = CategoryTheory.Dial.tensorHom X.rightUnitor.hom (CategoryTheory.CategoryStruct.id Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(X.braiding Y).hom.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(X.braiding Y).hom.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(X.braiding Y).inv.F = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>(X.braiding Y).inv.f = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<GOAL>CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (Y.braiding X).hom = CategoryTheory.CategoryStruct.id (X.tensorObj Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X : CategoryTheory.Dial C<VAR>Y Z : CategoryTheory.Dial C<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id X) f) (X.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Y).hom (CategoryTheory.Dial.tensorHom f (CategoryTheory.CategoryStruct.id X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : CategoryTheory.Dial C<VAR>f : X ⟶ Y<VAR>Z : CategoryTheory.Dial C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom f (CategoryTheory.CategoryStruct.id Z)) (Y.braiding Z).hom = CategoryTheory.CategoryStruct.comp (X.braiding Z).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id Z) f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>CategoryTheory.CategoryStruct.comp (X.associator Y Z).hom (CategoryTheory.CategoryStruct.comp (X.braiding (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (Y.associator Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (X.braiding Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (Y.associator X Z).hom (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id Y) (X.braiding Z).hom))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y Z : CategoryTheory.Dial C<GOAL>CategoryTheory.CategoryStruct.comp (X.associator Y Z).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.tensorObj X Y).braiding Z).hom (Z.associator X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Dial.tensorHom (CategoryTheory.CategoryStruct.id X) (Y.braiding Z).hom) (CategoryTheory.CategoryStruct.comp (X.associator Z Y).inv (CategoryTheory.Dial.tensorHom (X.braiding Z).hom (CategoryTheory.CategoryStruct.id Y)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{v, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Finite J<VAR>F : J → CategoryTheory.Idempotents.Karoubi C<VAR>j : J<GOAL>((CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).ι j).f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun j => (F j).X) j) (CategoryTheory.Limits.biproduct.map fun j => (F j).p)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{v, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Finite J<VAR>F : J → CategoryTheory.Idempotents.Karoubi C<VAR>j : J<GOAL>((CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).π j).f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map fun j => (F j).p) ((CategoryTheory.Limits.biproduct.bicone fun j => (F j).X).π j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{v, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Finite J<VAR>F : J → CategoryTheory.Idempotents.Karoubi C<GOAL>(CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).pt.p = CategoryTheory.Limits.biproduct.map fun j => (F j).p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{v, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<VAR>J : Type<VAR>Finite J<VAR>F : J → CategoryTheory.Idempotents.Karoubi C<GOAL>(CategoryTheory.Idempotents.Karoubi.Biproducts.bicone F).pt.X = ⨁ fun j => (F j).X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{v, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<GOAL>CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Idempotents.Karoubi C)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{v, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>P.complement.X = P.X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{v, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>P.complement.p = CategoryTheory.CategoryStruct.id P.X - P.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.IsIdempotentComplete C<VAR>X : C<VAR>p : X ⟶ X<GOAL>p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>CategoryTheory.IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → CategoryTheory.Limits.HasEqualizer (𝟙 X) p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : C<VAR>p : X ⟶ X<VAR>hp : p ≫ p = p<GOAL>(𝟙 X - p) ≫ (𝟙 X - p) = 𝟙 X - p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<GOAL>CategoryTheory.IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → CategoryTheory.Limits.HasKernel p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X X' : C<VAR>φ : X ≅ X'<VAR>p : X ⟶ X<VAR>p' : X' ⟶ X'<VAR>hpp' : p ≫ φ.hom = φ.hom ≫ p'<VAR>h : ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p<GOAL>∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X X' : C<VAR>φ : X ≅ X'<VAR>p : X ⟶ X<VAR>p' : X' ⟶ X'<VAR>hpp' : p ≫ φ.hom = φ.hom ≫ p'<GOAL>(∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>ε : C ≌ D<VAR>h : CategoryTheory.IsIdempotentComplete C<GOAL>CategoryTheory.IsIdempotentComplete D
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>ε : C ≌ D<GOAL>CategoryTheory.IsIdempotentComplete C ↔ CategoryTheory.IsIdempotentComplete D
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>h : CategoryTheory.IsIdempotentComplete Cᵒᵖ<GOAL>CategoryTheory.IsIdempotentComplete C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>CategoryTheory.IsIdempotentComplete Cᵒᵖ ↔ CategoryTheory.IsIdempotentComplete C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.Idempotents.Karoubi C<GOAL>CategoryTheory.CategoryStruct.comp self.p self.p = self.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>h_X : P.X = Q.X<VAR>h_p : CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.eqToHom h_X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h_X) Q.p<GOAL>P = Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>self : P.Hom Q<GOAL>self.f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp self.f Q.p)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P.Hom Q<GOAL>CategoryTheory.CategoryStruct.comp P.p f.f = f.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P.Hom Q<GOAL>CategoryTheory.CategoryStruct.comp f.f Q.p = f.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P.Hom Q<GOAL>CategoryTheory.CategoryStruct.comp P.p f.f = CategoryTheory.CategoryStruct.comp f.f Q.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q R : CategoryTheory.Idempotents.Karoubi C<VAR>g : Q.Hom R<VAR>f : P.Hom Q<GOAL>CategoryTheory.CategoryStruct.comp f.f g.f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f.f g.f) R.p)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f g : P ⟶ Q<GOAL>f = g ↔ f.f = g.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f g : P ⟶ Q<VAR>h : f.f = g.f<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q R : CategoryTheory.Idempotents.Karoubi C<VAR>f : P ⟶ Q<VAR>g : Q ⟶ R<GOAL>(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>(CategoryTheory.CategoryStruct.id P).f = P.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>CategoryTheory.CategoryStruct.id P = { f := P.p, comm := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>{ X := X, p := CategoryTheory.CategoryStruct.id X, idem := ⋯ }.X = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>{ X := X, p := CategoryTheory.CategoryStruct.id X, idem := ⋯ }.p = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>h : P = Q<GOAL>(CategoryTheory.eqToHom h).f = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>((CategoryTheory.Idempotents.toKaroubi C).obj X).p = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Idempotents.toKaroubi C).map f).f = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>((CategoryTheory.Idempotents.toKaroubi C).obj X).X = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f g : P ⟶ Q<GOAL>f + g = { f := f.f + g.f, comm := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P ⟶ Q<GOAL>-f = { f := -f.f, comm := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<GOAL>0 = { f := 0, comm := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P ⟶ Q<GOAL>f = 0 ↔ f.f = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P ⟶ Q<GOAL>(P.inclusionHom Q) f = f.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → (P ⟶ Q)<GOAL>(∑ x ∈ s, f x).f = ∑ x ∈ s, (f x).f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>P.decompId_i.f = P.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>P.decompId_p.f = P.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>CategoryTheory.CategoryStruct.id P = CategoryTheory.CategoryStruct.comp P.decompId_i P.decompId_p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi C<GOAL>(CategoryTheory.Idempotents.toKaroubi C).map P.p = CategoryTheory.CategoryStruct.comp P.decompId_p P.decompId_i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>((CategoryTheory.Idempotents.toKaroubi C).obj X).decompId_i = CategoryTheory.CategoryStruct.id ((CategoryTheory.Idempotents.toKaroubi C).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<GOAL>((CategoryTheory.Idempotents.toKaroubi C).obj X).decompId_p = CategoryTheory.CategoryStruct.id { X := ((CategoryTheory.Idempotents.toKaroubi C).obj X).X, p := CategoryTheory.CategoryStruct.id ((CategoryTheory.Idempotents.toKaroubi C).obj X).X, idem := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp f Q.decompId_i = CategoryTheory.CategoryStruct.comp P.decompId_i { f := f.f, comm := ⋯ }
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>f : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp P.decompId_p f = CategoryTheory.CategoryStruct.comp { f := f.f, comm := ⋯ } Q.decompId_p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>P Q : CategoryTheory.Idempotents.Karoubi C<VAR>n : ℤ<VAR>f : P ⟶ Q<GOAL>(n • f).f = n • f.f
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>X Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)<GOAL>∀ {X_1 Y_1 : J} (f : X_1 ⟶ Y_1) (g : CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) X_1 X ⟶ CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) X_1 Y), (CategoryTheory.Cat.HasLimits.homDiagram X Y).map f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map f).map g) (CategoryTheory.eqToHom ⋯))
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J CategoryTheory.Cat<VAR>X Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)<VAR>j : J<GOAL>(CategoryTheory.Cat.HasLimits.homDiagram X Y).obj j = (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j X ⟶ CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j Y)