ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 L : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c<VAR>f : K ⟶ L<VAR>n : ι<GOAL>(CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f).f.f n = (f.f n).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 ι<GOAL>∀ {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} (f : X ⟶ Y), CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.map f = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.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>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c<GOAL>CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.obj K = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K
<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>CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso.hom = CategoryTheory.eqToHom ⋯
<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>CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso.inv = CategoryTheory.eqToHom ⋯
<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.unitIso.hom.app P).f.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>n : ι<GOAL>(CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso.inv.app P).f.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 ι<GOAL>(CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).counitIso = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso
<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>(CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).unitIso = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso
<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>(CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).functor = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor
<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>(CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).inverse = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))<VAR>n : α<GOAL>(((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).X n).X = P.X.X n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>∀ {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)} (f : X ⟶ Y) (n : α), ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))} (f : X ⟶ Y) (n : α), (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.map f).f n).f = f.f.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)<VAR>i j : α<GOAL>((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))<VAR>n : α<GOAL>(((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.inv.app P).f.f n = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))<VAR>i j : α<GOAL>(((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).d i j).f = CategoryTheory.CategoryStruct.comp (P.X.d i j) (P.p.f j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>(CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).counitIso.hom = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>(CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).counitIso.inv = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>∀ {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)} (f : X ⟶ Y) (n : α), ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>(CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).counitIso.inv = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))<VAR>n : α<GOAL>(((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).X n).X = P.X.X n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>(CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).counitIso.hom = CategoryTheory.eqToHom ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).unitIso.inv.app P).f.f n = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))<VAR>n : α<GOAL>(((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)<VAR>n : α<GOAL>((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)<VAR>i j : α<GOAL>((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))<VAR>i j : α<GOAL>(((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).d i j).f = CategoryTheory.CategoryStruct.comp (P.X.d i j) (P.p.f j)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<GOAL>∀ {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))} (f : X ⟶ Y) (n : α), (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.map f).f n).f = f.f.f n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : CategoryTheory.Monad C<GOAL>M.toMon.X = M.toFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : CategoryTheory.Monad C<GOAL>M.toMon.mul = M.μ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : CategoryTheory.Monad C<GOAL>M.toMon.one = M.η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : CategoryTheory.Monad C<GOAL>(CategoryTheory.Monad.monadToMon C).obj M = M.toMon
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Monad C} (f : X ⟶ Y), ((CategoryTheory.Monad.monadToMon C).map f).hom = f.toNatTrans
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Mon_ (CategoryTheory.Functor C C)<GOAL>(CategoryTheory.Monad.ofMon M).μ = M.mul
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Mon_ (CategoryTheory.Functor C C)<GOAL>(CategoryTheory.Monad.ofMon M).η = M.one
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Mon_ (CategoryTheory.Functor C C)<VAR>X : C<GOAL>(CategoryTheory.Monad.ofMon M).obj X = M.X.obj X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : Mon_ (CategoryTheory.Functor C C)<VAR>f : X ⟶ Y<GOAL>((CategoryTheory.Monad.monToMonad C).map f).toNatTrans = f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Mon_ (CategoryTheory.Functor C C)<GOAL>(CategoryTheory.Monad.monToMonad C).obj M = CategoryTheory.Monad.ofMon M
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ (x : CategoryTheory.Monad C) (x_1 : C), ((CategoryTheory.Monad.monadMonEquiv C).unitIso.hom.app x).app x_1 = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Monad C)).obj x).obj x_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ (x : Mon_ (CategoryTheory.Functor C C)), ((CategoryTheory.Monad.monadMonEquiv C).counitIso.inv.app x).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (Mon_ (CategoryTheory.Functor C C))).obj x).X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.Monad.monadMonEquiv C).functor = CategoryTheory.Monad.monadToMon C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ (x : Mon_ (CategoryTheory.Functor C C)), ((CategoryTheory.Monad.monadMonEquiv C).counitIso.hom.app x).hom = CategoryTheory.CategoryStruct.id (((CategoryTheory.Monad.monToMonad C).comp (CategoryTheory.Monad.monadToMon C)).obj x).X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>(CategoryTheory.Monad.monadMonEquiv C).inverse = CategoryTheory.Monad.monToMonad C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ (x : CategoryTheory.Monad C) (x_1 : C), ((CategoryTheory.Monad.monadMonEquiv C).unitIso.inv.app x).app x_1 = CategoryTheory.CategoryStruct.id ((((CategoryTheory.Monad.monadToMon C).comp (CategoryTheory.Monad.monToMonad C)).obj x).obj x_1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<GOAL>CategoryTheory.MorphismProperty.bijective C = CategoryTheory.MorphismProperty.injective C ⊓ CategoryTheory.MorphismProperty.surjective C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>self : T.Algebra<GOAL>CategoryTheory.CategoryStruct.comp (T.μ.app self.A) self.a = CategoryTheory.CategoryStruct.comp (T.map self.a) self.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>self : T.Algebra<GOAL>CategoryTheory.CategoryStruct.comp (T.η.app self.A) self.a = CategoryTheory.CategoryStruct.id self.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A B : T.Algebra<VAR>self : A.Hom B<GOAL>CategoryTheory.CategoryStruct.comp (T.map self.f) B.a = CategoryTheory.CategoryStruct.comp A.a self.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X Y : T.Algebra<VAR>f g : X ⟶ Y<VAR>h : f.f = g.f<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A A' A'' : T.Algebra<VAR>f : A ⟶ A'<VAR>g : A' ⟶ A''<GOAL>CategoryTheory.Monad.Algebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A : T.Algebra<GOAL>CategoryTheory.Monad.Algebra.Hom.id A = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A : T.Algebra<GOAL>(CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A A' A'' : T.Algebra<VAR>f : A ⟶ A'<VAR>g : A' ⟶ A''<GOAL>(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A B : T.Algebra<VAR>h : A.A ≅ B.A<VAR>w : CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom := by aesop_cat<GOAL>(CategoryTheory.Monad.Algebra.isoMk h w).inv.f = h.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A B : T.Algebra<VAR>h : A.A ≅ B.A<VAR>w : CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom := by aesop_cat<GOAL>(CategoryTheory.Monad.Algebra.isoMk h w).hom.f = h.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<GOAL>∀ {X Y : T.Algebra} (f : X ⟶ Y), T.forget.map f = f.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A : T.Algebra<GOAL>T.forget.obj A = A.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : C<GOAL>(T.free.obj X).a = T.μ.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (T.free.map f).f = T.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : C<GOAL>(T.free.obj X).A = T.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<GOAL>T.adj.unit = { app := fun X => T.η.app X, naturality := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<GOAL>T.adj.counit = { app := fun Y => { f := Y.a, h := ⋯ }, naturality := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>A B : T.Algebra<VAR>f : A ⟶ B<VAR>CategoryTheory.IsIso f.f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X Y : T.Algebra<VAR>f : X ⟶ Y<VAR>h : CategoryTheory.Epi f.f<GOAL>CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X Y : T.Algebra<VAR>f : X ⟶ Y<VAR>h : CategoryTheory.Mono f.f<GOAL>CategoryTheory.Mono f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₂ ⟶ T₁<VAR>A : T₁.Algebra<GOAL>((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).a = CategoryTheory.CategoryStruct.comp (h.app A.A) A.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₂ ⟶ T₁<GOAL>∀ {X Y : T₁.Algebra} (f : X ⟶ Y), ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).map f).f = f.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₂ ⟶ T₁<VAR>A : T₁.Algebra<GOAL>((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).A = A.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ : CategoryTheory.Monad C<VAR>X : T₁.Algebra<GOAL>(CategoryTheory.Monad.algebraFunctorOfMonadHomId.inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ : CategoryTheory.Monad C<VAR>X : T₁.Algebra<GOAL>(CategoryTheory.Monad.algebraFunctorOfMonadHomId.hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ T₃ : CategoryTheory.Monad C<VAR>f : T₁ ⟶ T₂<VAR>g : T₂ ⟶ T₃<VAR>X : T₃.Algebra<GOAL>((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ T₃ : CategoryTheory.Monad C<VAR>f : T₁ ⟶ T₂<VAR>g : T₂ ⟶ T₃<VAR>X : T₃.Algebra<GOAL>((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>f g : T₁ ⟶ T₂<VAR>h : f = g<VAR>X : T₂.Algebra<GOAL>((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>f g : T₁ ⟶ T₂<VAR>h : f = g<VAR>X : T₂.Algebra<GOAL>((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₁ ≅ T₂<GOAL>(CategoryTheory.Monad.algebraEquivOfIsoMonads h).counitIso = (CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.inv h.hom).symm ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomEq ⋯ ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomId
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₁ ≅ T₂<GOAL>(CategoryTheory.Monad.algebraEquivOfIsoMonads h).unitIso = CategoryTheory.Monad.algebraFunctorOfMonadHomId.symm ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomEq ⋯ ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.hom h.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₁ ≅ T₂<GOAL>(CategoryTheory.Monad.algebraEquivOfIsoMonads h).functor = CategoryTheory.Monad.algebraFunctorOfMonadHom h.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₁ ≅ T₂<GOAL>(CategoryTheory.Monad.algebraEquivOfIsoMonads h).inverse = CategoryTheory.Monad.algebraFunctorOfMonadHom h.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T₁ T₂ : CategoryTheory.Monad C<VAR>h : T₁ ⟶ T₂<GOAL>(CategoryTheory.Monad.algebraFunctorOfMonadHom h).comp T₁.forget = T₂.forget
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>self : G.Coalgebra<GOAL>CategoryTheory.CategoryStruct.comp self.a (G.δ.app self.A) = CategoryTheory.CategoryStruct.comp self.a (G.map self.a)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>self : G.Coalgebra<GOAL>CategoryTheory.CategoryStruct.comp self.a (G.ε.app self.A) = CategoryTheory.CategoryStruct.id self.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A B : G.Coalgebra<VAR>self : A.Hom B<GOAL>CategoryTheory.CategoryStruct.comp A.a (G.map self.f) = CategoryTheory.CategoryStruct.comp self.f B.a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>X Y : G.Coalgebra<VAR>f g : X ⟶ Y<VAR>h : f.f = g.f<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A A' A'' : G.Coalgebra<VAR>f : A ⟶ A'<VAR>g : A' ⟶ A''<GOAL>CategoryTheory.Comonad.Coalgebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A : G.Coalgebra<GOAL>CategoryTheory.Comonad.Coalgebra.Hom.id A = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A : G.Coalgebra<GOAL>(CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A A' A'' : G.Coalgebra<VAR>f : A ⟶ A'<VAR>g : A' ⟶ A''<GOAL>(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>A B : G.Coalgebra<VAR>h : A.A ≅ B.A<VAR>w : CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a := by aesop_cat<GOAL>(CategoryTheory.Comonad.Coalgebra.isoMk h w).hom.f = h.hom