ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>CategoryTheory.CoverPreserving J (e.inverse.inducedTopology J) e.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>self : CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<GOAL>K = e.inverse.inducedTopology J
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<GOAL>K = e.inverse.inducedTopology J
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>F : CategoryTheory.Sheaf J A<GOAL>∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).obj F).val.map f = F.val.map (e.inverse.map f.unop).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>F : CategoryTheory.Sheaf J A<VAR>X : Dᵒᵖ<GOAL>((CategoryTheory.Equivalence.sheafCongr.functor J K e A).obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj (Opposite.unop X)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<GOAL>∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).map f).val.app X_1 = f.val.app (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>F : CategoryTheory.Sheaf K A<VAR>X : Cᵒᵖ<GOAL>((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj (Opposite.unop X)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>F : CategoryTheory.Sheaf K A<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).obj F).val.map f = F.val.map (e.functor.map f.unop).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<GOAL>∀ {X Y : CategoryTheory.Sheaf K A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.inverse J K e A).map f).val.app X_1 = f.val.app (Opposite.op (e.functor.obj (Opposite.unop X_1)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>X : CategoryTheory.Sheaf J A<GOAL>∀ (X_1 : Cᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.unitIso J K e A).inv.app X).val.app X_1 = X.val.map (e.unitIso.hom.app (Opposite.unop X_1)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>X : CategoryTheory.Sheaf J A<GOAL>∀ (X_1 : Cᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.unitIso J K e A).hom.app X).val.app X_1 = X.val.map (e.unitIso.inv.app (Opposite.unop X_1)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>X : CategoryTheory.Sheaf K A<GOAL>∀ (X_1 : Dᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.counitIso J K e A).inv.app X).val.app X_1 = X.val.map (e.counitIso.hom.app (Opposite.unop X_1)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>X : CategoryTheory.Sheaf K A<GOAL>∀ (X_1 : Dᵒᵖ), ((CategoryTheory.Equivalence.sheafCongr.counitIso J K e A).hom.app X).val.app X_1 = X.val.map (e.counitIso.inv.app (Opposite.unop X_1)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>CategoryTheory.HasSheafify K A<GOAL>CategoryTheory.HasSheafify J A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>e : C ≌ D<VAR>CategoryTheory.Equivalence.TransportsGrothendieckTopology J K e<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>B : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} B<VAR>F : CategoryTheory.Functor A B<VAR>K.HasSheafCompose F<GOAL>J.HasSheafCompose F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor D C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>G.IsCoverDense J<VAR>G.IsContinuous K J<VAR>G.Full<VAR>(G.sheafPushforwardContinuous A K J).EssSurj<GOAL>K.W.inverseImage ((CategoryTheory.whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor D C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>G.IsCoverDense J<VAR>G.IsContinuous K J<VAR>G.Full<VAR>(G.sheafPushforwardContinuous A K J).EssSurj<VAR>P Q : CategoryTheory.Functor Cᵒᵖ A<VAR>f : P ⟶ Q<GOAL>K.W (CategoryTheory.whiskerLeft G.op f) ↔ J.W f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor D C<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>G.IsCoverDense J<VAR>G.IsContinuous K J<VAR>G.Full<VAR>(G.sheafPushforwardContinuous A K J).EssSurj<VAR>G.IsCocontinuous K J<VAR>hG : CategoryTheory.CoverPreserving K J G<VAR>CategoryTheory.ConcreteCategory A<VAR>K.WEqualsLocallyBijective A<GOAL>J.WEqualsLocallyBijective A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ∈ (CategoryTheory.extensiveTopology C).sieves X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A₀ A₁ : CategoryTheory.Endofunctor.Algebra F<VAR>self : A₀.Hom A₁<GOAL>CategoryTheory.CategoryStruct.comp (F.map self.f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str self.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A B : CategoryTheory.Endofunctor.Algebra F<VAR>f g : A ⟶ B<VAR>w : f.f = g.f := by aesop_cat<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Algebra F<GOAL>CategoryTheory.Endofunctor.Algebra.Hom.id A = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Algebra F<GOAL>(CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A₀ A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<VAR>f : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<GOAL>CategoryTheory.Endofunctor.Algebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A₀ A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<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>F : CategoryTheory.Functor C C<VAR>A₀ A₁ : CategoryTheory.Endofunctor.Algebra F<VAR>h : A₀.a ≅ A₁.a<VAR>w : CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom := by aesop_cat<GOAL>(CategoryTheory.Endofunctor.Algebra.isoMk h w).inv.f = h.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A₀ A₁ : CategoryTheory.Endofunctor.Algebra F<VAR>h : A₀.a ≅ A₁.a<VAR>w : CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom := by aesop_cat<GOAL>(CategoryTheory.Endofunctor.Algebra.isoMk h w).hom.f = h.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<GOAL>∀ {X Y : CategoryTheory.Endofunctor.Algebra F} (self : X.Hom Y), (CategoryTheory.Endofunctor.Algebra.forget F).map self = self.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Algebra F<GOAL>(CategoryTheory.Endofunctor.Algebra.forget F).obj A = A.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A₀ A₁ : CategoryTheory.Endofunctor.Algebra F<VAR>f : A₀ ⟶ A₁<VAR>CategoryTheory.IsIso f.f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X Y : CategoryTheory.Endofunctor.Algebra F<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>F : CategoryTheory.Functor C C<VAR>X Y : CategoryTheory.Endofunctor.Algebra F<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>F G : CategoryTheory.Functor C C<VAR>α : G ⟶ F<VAR>A : CategoryTheory.Endofunctor.Algebra F<GOAL>((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).obj A).a = A.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : G ⟶ F<VAR>A : CategoryTheory.Endofunctor.Algebra F<GOAL>((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).obj A).str = CategoryTheory.CategoryStruct.comp (α.app A.a) A.str
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : G ⟶ F<GOAL>∀ {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y), ((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).map f).f = f.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : CategoryTheory.Endofunctor.Algebra F<GOAL>(CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.hom.app X).f = CategoryTheory.CategoryStruct.id X.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : CategoryTheory.Endofunctor.Algebra F<GOAL>(CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.inv.app X).f = CategoryTheory.CategoryStruct.id X.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₀ F₁ F₂ : CategoryTheory.Functor C C<VAR>α : F₀ ⟶ F₁<VAR>β : F₁ ⟶ F₂<VAR>X : CategoryTheory.Endofunctor.Algebra F₂<GOAL>((CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α β).hom.app X).f = CategoryTheory.CategoryStruct.id X.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₀ F₁ F₂ : CategoryTheory.Functor C C<VAR>α : F₀ ⟶ F₁<VAR>β : F₁ ⟶ F₂<VAR>X : CategoryTheory.Endofunctor.Algebra F₂<GOAL>((CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α β).inv.app X).f = CategoryTheory.CategoryStruct.id X.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α β : F ⟶ G<VAR>h : α = β<VAR>X : CategoryTheory.Endofunctor.Algebra G<GOAL>((CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h).hom.app X).f = CategoryTheory.CategoryStruct.id X.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α β : F ⟶ G<VAR>h : α = β<VAR>X : CategoryTheory.Endofunctor.Algebra G<GOAL>((CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h).inv.app X).f = CategoryTheory.CategoryStruct.id X.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).functor = CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).counitIso = (CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α.inv α.hom).symm ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq ⋯ ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransId
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).unitIso = CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.symm ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq ⋯ ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α.hom α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).inverse = CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Algebra F<VAR>h : CategoryTheory.Limits.IsInitial A<GOAL>{ f := CategoryTheory.CategoryStruct.comp (CategoryTheory.Endofunctor.Algebra.Initial.strInv h) A.str, h := ⋯ } = CategoryTheory.CategoryStruct.id A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Algebra F<VAR>h : CategoryTheory.Limits.IsInitial A<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Endofunctor.Algebra.Initial.strInv h) A.str = CategoryTheory.CategoryStruct.id A.a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Algebra F<VAR>h : CategoryTheory.Limits.IsInitial A<GOAL>CategoryTheory.CategoryStruct.comp A.str (CategoryTheory.Endofunctor.Algebra.Initial.strInv h) = CategoryTheory.CategoryStruct.id (F.obj A.a)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Algebra F<VAR>h : CategoryTheory.Limits.IsInitial A<GOAL>CategoryTheory.IsIso A.str
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F<VAR>self : V₀.Hom V₁<GOAL>CategoryTheory.CategoryStruct.comp V₀.str (F.map self.f) = CategoryTheory.CategoryStruct.comp self.f V₁.str
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A B : CategoryTheory.Endofunctor.Coalgebra F<VAR>f g : A ⟶ B<VAR>w : f.f = g.f := by aesop_cat<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>V : CategoryTheory.Endofunctor.Coalgebra F<GOAL>CategoryTheory.Endofunctor.Coalgebra.Hom.id V = CategoryTheory.CategoryStruct.id V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>V : CategoryTheory.Endofunctor.Coalgebra F<GOAL>(CategoryTheory.CategoryStruct.id V).f = CategoryTheory.CategoryStruct.id V.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>V₀ V₁ V₂ : CategoryTheory.Endofunctor.Coalgebra F<VAR>f : V₀ ⟶ V₁<VAR>g : V₁ ⟶ V₂<GOAL>CategoryTheory.Endofunctor.Coalgebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>V₀ V₁ V₂ : CategoryTheory.Endofunctor.Coalgebra F<VAR>f : V₀ ⟶ V₁<VAR>g : V₁ ⟶ V₂<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>F : CategoryTheory.Functor C C<VAR>V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F<VAR>h : V₀.V ≅ V₁.V<VAR>w : CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str := by aesop_cat<GOAL>(CategoryTheory.Endofunctor.Coalgebra.isoMk h w).hom.f = h.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F<VAR>h : V₀.V ≅ V₁.V<VAR>w : CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str := by aesop_cat<GOAL>(CategoryTheory.Endofunctor.Coalgebra.isoMk h w).inv.f = h.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<GOAL>∀ {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y), (CategoryTheory.Endofunctor.Coalgebra.forget F).map f = f.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>A : CategoryTheory.Endofunctor.Coalgebra F<GOAL>(CategoryTheory.Endofunctor.Coalgebra.forget F).obj A = A.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F<VAR>f : V₀ ⟶ V₁<VAR>CategoryTheory.IsIso f.f<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X Y : CategoryTheory.Endofunctor.Coalgebra F<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>F : CategoryTheory.Functor C C<VAR>X Y : CategoryTheory.Endofunctor.Coalgebra F<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>F G : CategoryTheory.Functor C C<VAR>α : F ⟶ G<VAR>V : CategoryTheory.Endofunctor.Coalgebra F<GOAL>((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).obj V).V = V.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ⟶ G<GOAL>∀ {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y), ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).map f).f = f.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ⟶ G<VAR>V : CategoryTheory.Endofunctor.Coalgebra F<GOAL>((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).obj V).str = CategoryTheory.CategoryStruct.comp V.str (α.app V.V)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : CategoryTheory.Endofunctor.Coalgebra F<GOAL>(CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.inv.app X).f = CategoryTheory.CategoryStruct.id X.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : CategoryTheory.Endofunctor.Coalgebra F<GOAL>(CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.hom.app X).f = CategoryTheory.CategoryStruct.id X.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₀ F₁ F₂ : CategoryTheory.Functor C C<VAR>α : F₀ ⟶ F₁<VAR>β : F₁ ⟶ F₂<VAR>X : CategoryTheory.Endofunctor.Coalgebra F₀<GOAL>((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α β).inv.app X).f = CategoryTheory.CategoryStruct.id X.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F₀ F₁ F₂ : CategoryTheory.Functor C C<VAR>α : F₀ ⟶ F₁<VAR>β : F₁ ⟶ F₂<VAR>X : CategoryTheory.Endofunctor.Coalgebra F₀<GOAL>((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α β).hom.app X).f = CategoryTheory.CategoryStruct.id X.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α β : F ⟶ G<VAR>h : α = β<VAR>X : CategoryTheory.Endofunctor.Coalgebra F<GOAL>((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h).inv.app X).f = CategoryTheory.CategoryStruct.id X.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α β : F ⟶ G<VAR>h : α = β<VAR>X : CategoryTheory.Endofunctor.Coalgebra F<GOAL>((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h).hom.app X).f = CategoryTheory.CategoryStruct.id X.V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).counitIso = (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α.inv α.hom).symm ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq ⋯ ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).functor = CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).inverse = CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>α : F ≅ G<GOAL>(CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).unitIso = CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.symm ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq ⋯ ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α.hom α.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>adj : F ⊣ G<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<VAR>f : A₁ ⟶ A₂<GOAL>CategoryTheory.CategoryStruct.comp ((adj.homEquiv A₁.a A₁.a) A₁.str) (G.map f.f) = CategoryTheory.CategoryStruct.comp f.f ((adj.homEquiv A₂.a A₂.a) A₂.str)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor C C<VAR>adj : F ⊣ G<VAR>V₁ V₂ : CategoryTheory.Endofunctor.Coalgebra G<VAR>f : V₁ ⟶ V₂<GOAL>CategoryTheory.CategoryStruct.comp (F.map f.f) ((adj.homEquiv V₂.V V₂.V).symm V₂.str) = CategoryTheory.CategoryStruct.comp ((adj.homEquiv V₁.V V₁.V).symm V₁.str) f.f