ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor T C<GOAL>∀ {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y), ((CategoryTheory.Comma.post L R F).map f).right = f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor T C<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.post L R F).obj X).right = X.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>C : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} C<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor T C<VAR>X : CategoryTheory.Comma L R<GOAL>((CategoryTheory.Comma.post L R F).obj X).hom = F.map X.hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)<GOAL>CategoryTheory.CategoryStruct.comp P.p.f P.p.f = P.p.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)<VAR>f : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp P.p.f f.f.f = CategoryTheory.CategoryStruct.comp f.f.f Q.p.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)<GOAL>((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).obj P).p = P.p.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)<GOAL>((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).obj P).X = P.X.X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)} (f : X ⟶ Y), ((CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).map f).f = f.f.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.Idempotents.Karoubi C<GOAL>((CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C).inv.app X).f = X.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.Idempotents.Karoubi C<GOAL>((CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C).hom.app X).f = X.p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)<GOAL>((CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C).hom.app P).f.f = P.p.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)<GOAL>((CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C).inv.app P).f.f = P.p.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>(CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).functor = CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>(CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).inverse = CategoryTheory.Idempotents.KaroubiKaroubi.inverse C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>(CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).counitIso = CategoryTheory.Idempotents.KaroubiKaroubi.counitIso C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>(CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).unitIso = CategoryTheory.Idempotents.KaroubiKaroubi.unitIso C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.ContainsIdentities<VAR>X : C<GOAL>W (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.ContainsIdentities<VAR>X : C<GOAL>W (CategoryTheory.CategoryStruct.id X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.op.ContainsIdentities<GOAL>W.ContainsIdentities
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>W.unop.ContainsIdentities<GOAL>W.ContainsIdentities
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>self : P.IsStableUnderComposition<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>P f → P g → P (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.IsStableUnderComposition<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hf : W f<VAR>hg : W g<GOAL>W (CategoryTheory.CategoryStruct.comp f g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>h : P.StableUnderInverse<GOAL>P.op.StableUnderInverse
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>h : P.StableUnderInverse<GOAL>P.unop.StableUnderInverse
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.MorphismProperty C<VAR>P.IsStableUnderComposition<VAR>hP : CategoryTheory.MorphismProperty.isomorphisms C ≤ P<GOAL>P.RespectsIso
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F₁ F₂ : CategoryTheory.Functor C D<VAR>app : (X : C) → F₁.obj X ⟶ F₂.obj X<GOAL>(CategoryTheory.MorphismProperty.naturalityProperty app).StableUnderInverse
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.op.IsMultiplicative<GOAL>W.IsMultiplicative
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty Cᵒᵖ<VAR>W.unop.IsMultiplicative<GOAL>W.IsMultiplicative
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.HasTwoOutOfThreeProperty<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>W f → W (CategoryTheory.CategoryStruct.comp f g) → W g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.HasTwoOutOfThreeProperty<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>W g → W (CategoryTheory.CategoryStruct.comp f g) → W f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasTwoOutOfThreeProperty<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hg : W g<VAR>hfg : W (CategoryTheory.CategoryStruct.comp f g)<GOAL>W f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasTwoOutOfThreeProperty<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hf : W f<VAR>hfg : W (CategoryTheory.CategoryStruct.comp f g)<GOAL>W g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasTwoOutOfThreeProperty<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hg : W g<GOAL>W (CategoryTheory.CategoryStruct.comp f g) ↔ W f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasTwoOutOfThreeProperty<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hf : W f<GOAL>W (CategoryTheory.CategoryStruct.comp f g) ↔ W g
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>B : D<VAR>CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<GOAL>∀ (a : CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj adj A ⟶ B), ((CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B) a).f = CategoryTheory.CategoryStruct.comp (adj.unit.app A.A) (G.map ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B) a))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>B : D<VAR>CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<GOAL>∀ (a : A ⟶ (CategoryTheory.Monad.comparison adj).obj B), (CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointHomEquiv adj A B).symm a = (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A)))) B).symm ⟨CategoryTheory.CategoryStruct.comp (F.map a.f) (adj.counit.app B), ⋯⟩
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<GOAL>(CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit = { app := fun Y => (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app Y))) (adj.counit.app (F.obj (G.obj Y))))) Y).symm ⟨adj.counit.app Y, ⋯⟩, naturality := ⋯ }
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>A : adj.toMonad.Algebra<GOAL>((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f = (adj.homEquiv A.A (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))) (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<GOAL>(CategoryTheory.Monad.MonadicityInternal.unitCofork A).pt = G.obj (CategoryTheory.Limits.coequalizer (F.map A.a) (adj.counit.app (F.obj A.A)))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<GOAL>(CategoryTheory.Monad.MonadicityInternal.unitCofork A).π = G.map (CategoryTheory.Limits.coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>A : adj.toMonad.Algebra<GOAL>((CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).unit.app A).f = (CategoryTheory.Monad.beckCoequalizer A).desc (CategoryTheory.Monad.MonadicityInternal.unitCofork A)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>B : D<GOAL>(CategoryTheory.Monad.MonadicityInternal.counitCofork adj B).pt = B
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>B : D<VAR>X : CategoryTheory.Limits.WalkingParallelPair<GOAL>(CategoryTheory.Monad.MonadicityInternal.counitCofork adj B).ι.app X = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.CategoryStruct.comp (adj.counit.app (F.obj (G.obj B))) (adj.counit.app B)) (adj.counit.app B) X
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F : CategoryTheory.Functor C D<VAR>adj : F ⊣ G<VAR>∀ (A : adj.toMonad.Algebra), CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>B : D<GOAL>(CategoryTheory.Monad.MonadicityInternal.comparisonAdjunction adj).counit.app B = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))) (CategoryTheory.Monad.MonadicityInternal.counitCofork adj B)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>self : CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G<VAR>A B : D<VAR>f g : A ⟶ B<VAR>G.IsSplitPair f g<GOAL>CategoryTheory.Limits.HasCoequalizer f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>Y : C<GOAL>(CategoryTheory.prodComonad X).obj Y = (X ⨯ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.prodComonad X).map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>Y : C<GOAL>(CategoryTheory.prodComonad X).ε.app Y = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>Y : C<GOAL>(CategoryTheory.prodComonad X).δ.app Y = CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.id (X ⨯ Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>A : (CategoryTheory.prodComonad X).Coalgebra<GOAL>(CategoryTheory.coalgebraToOver X).obj A = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp A.a CategoryTheory.Limits.prod.fst)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>∀ {X_1 Y : (CategoryTheory.prodComonad X).Coalgebra} (f : X_1 ⟶ Y), (CategoryTheory.coalgebraToOver X).map f = CategoryTheory.Over.homMk f.f ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>f : CategoryTheory.Over X<GOAL>((CategoryTheory.overToCoalgebra X).obj f).a = CategoryTheory.Limits.prod.lift f.hom (CategoryTheory.CategoryStruct.id f.left)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>∀ {X_1 Y : CategoryTheory.Over X} (g : X_1 ⟶ Y), ((CategoryTheory.overToCoalgebra X).map g).f = g.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>f : CategoryTheory.Over X<GOAL>((CategoryTheory.overToCoalgebra X).obj f).A = f.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>(CategoryTheory.coalgebraEquivOver X).counitIso = CategoryTheory.NatIso.ofComponents (fun f => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl (((CategoryTheory.overToCoalgebra X).comp (CategoryTheory.coalgebraToOver X)).obj f).left) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>(CategoryTheory.coalgebraEquivOver X).functor = CategoryTheory.coalgebraToOver X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>(CategoryTheory.coalgebraEquivOver X).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Comonad.Coalgebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.prodComonad X).Coalgebra).obj A).A) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>(CategoryTheory.coalgebraEquivOver X).inverse = CategoryTheory.overToCoalgebra X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>Y : C<GOAL>(CategoryTheory.coprodMonad X).η.app Y = CategoryTheory.Limits.coprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>Y : C<GOAL>(CategoryTheory.coprodMonad X).μ.app Y = CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.id (X ⨿ Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>Y : C<GOAL>(CategoryTheory.coprodMonad X).obj Y = (X ⨿ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>Y Z : C<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.coprodMonad X).map g = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>A : (CategoryTheory.coprodMonad X).Algebra<GOAL>(CategoryTheory.algebraToUnder X).obj A = CategoryTheory.Under.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl A.a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>∀ {X_1 Y : (CategoryTheory.coprodMonad X).Algebra} (f : X_1 ⟶ Y), (CategoryTheory.algebraToUnder X).map f = CategoryTheory.Under.homMk f.f ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>∀ {X_1 Y : CategoryTheory.Under X} (g : X_1 ⟶ Y), ((CategoryTheory.underToAlgebra X).map g).f = g.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>f : CategoryTheory.Under X<GOAL>((CategoryTheory.underToAlgebra X).obj f).a = CategoryTheory.Limits.coprod.desc f.hom (CategoryTheory.CategoryStruct.id f.right)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>f : CategoryTheory.Under X<GOAL>((CategoryTheory.underToAlgebra X).obj f).A = f.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>(CategoryTheory.algebraEquivUnder X).functor = CategoryTheory.algebraToUnder X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>(CategoryTheory.algebraEquivUnder X).unitIso = CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Monad.Algebra.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.coprodMonad X).Algebra).obj A).A) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>(CategoryTheory.algebraEquivUnder X).counitIso = CategoryTheory.NatIso.ofComponents (fun f => CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl (((CategoryTheory.underToAlgebra X).comp (CategoryTheory.algebraToUnder X)).obj f).right) ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<GOAL>(CategoryTheory.algebraEquivUnder X).inverse = CategoryTheory.underToAlgebra X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>f : P ⟶ Q<VAR>n : ι<GOAL>CategoryTheory.CategoryStruct.comp (P.p.f n) (f.f.f n) = f.f.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>f : P ⟶ Q<VAR>n : ι<GOAL>CategoryTheory.CategoryStruct.comp (f.f.f n) (Q.p.f n) = f.f.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>f : P ⟶ Q<VAR>n : ι<GOAL>CategoryTheory.CategoryStruct.comp (P.p.f n) (f.f.f n) = CategoryTheory.CategoryStruct.comp (f.f.f n) (Q.p.f n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>n : ι<GOAL>CategoryTheory.CategoryStruct.comp (P.p.f n) (P.p.f n) = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>i j : ι<GOAL>((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).d i j).f = CategoryTheory.CategoryStruct.comp (P.p.f i) (P.X.d i j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>n : ι<GOAL>((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).X n).p = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>n : ι<GOAL>((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).X n).X = P.X.X n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<VAR>f : P ⟶ Q<VAR>n : ι<GOAL>((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f).f n).f = f.f.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : X ⟶ Y), CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.map f = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)<GOAL>CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.obj P = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c<VAR>n : ι<GOAL>(CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).p.f n = (K.X n).p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c<VAR>n : ι<GOAL>(CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X.X n = (K.X n).X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c<VAR>i j : ι<GOAL>(CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X.d i j = (K.d i j).f