ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>K L : CategoryTheory.Coverage C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type u_1)<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (K ⊔ L)) P ↔ CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ∧ CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C L) P
<VAR>C : Type u_1<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Category.{u_3, u_4} D<VAR>K : CategoryTheory.Coverage C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.covering X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))
<VAR>C : Type u_1<VAR>D : Type u_4<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Category.{u_3, u_4} D<VAR>K L : CategoryTheory.Coverage C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (K ⊔ L)) P ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ∧ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Coverage.toGrothendieck C L) P
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.Additive<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>F.map (f + g) = F.map f + F.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>F.map (f + g) = F.map f + F.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.mapAddHom f = F.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<GOAL>⇑F.mapAddHom = F.map
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.map (-f) = -F.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>F.map (f - g) = F.map f - F.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>n : ℕ<GOAL>F.map (n • f) = n • F.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>r : ℤ<GOAL>F.map (r • f) = r • F.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>X Y : C<VAR>α : Type u_4<VAR>f : α → (X ⟶ Y)<VAR>s : Finset α<GOAL>F.map (∑ a ∈ s, f a) = ∑ a ∈ s, F.map (f a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>G : CategoryTheory.Functor C D<VAR>e : F ≅ G<GOAL>G.Additive
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Preadditive E<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>F.Full<VAR>F.EssSurj<VAR>G : CategoryTheory.Functor D E<VAR>(F.comp G).Additive<GOAL>G.Additive
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Preadditive E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>G.Additive<VAR>(F.comp G).Additive<VAR>G.Faithful<GOAL>F.Additive
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<VAR>CategoryTheory.Limits.HasZeroObject C<GOAL>CategoryTheory.Limits.HasZeroObject D
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>F.PreservesZeroMorphisms<VAR>CategoryTheory.Limits.PreservesBinaryBiproducts F<GOAL>F.Additive
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>F.PreservesZeroMorphisms<GOAL>F.Additive
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>(CategoryTheory.AdditiveFunctor.of F).obj = F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : C ⥤+ D<GOAL>(CategoryTheory.AdditiveFunctor.forget C D).obj F = F.obj
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Functor C D<VAR>F.Additive<GOAL>(CategoryTheory.AdditiveFunctor.forget C D).obj (CategoryTheory.AdditiveFunctor.of F) = F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F G : C ⥤+ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.AdditiveFunctor.forget C D).map α = α
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>F : C ⥤ₗ D<GOAL>((CategoryTheory.AdditiveFunctor.ofLeftExact C D).obj F).obj = F.obj
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>F : C ⥤ᵣ D<GOAL>((CategoryTheory.AdditiveFunctor.ofRightExact C D).obj F).obj = F.obj
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>F : C ⥤ₑ D<GOAL>((CategoryTheory.AdditiveFunctor.ofExact C D).obj F).obj = F.obj
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>F G : C ⥤ₗ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.AdditiveFunctor.ofLeftExact C D).map α = α
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>F G : C ⥤ᵣ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.AdditiveFunctor.ofRightExact C D).map α = α
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroObject D<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>F G : C ⥤ₑ D<VAR>α : F ⟶ G<GOAL>(CategoryTheory.AdditiveFunctor.ofExact C D).map α = α
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>Y : C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.preadditiveYonedaObj Y).obj X = ModuleCat.of (CategoryTheory.End Y) (Opposite.unop X ⟶ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>Y : C<GOAL>∀ {X Y_1 : Cᵒᵖ} (f : X ⟶ Y_1), (CategoryTheory.preadditiveYonedaObj Y).map f = ModuleCat.ofHom { toFun := fun g => CategoryTheory.CategoryStruct.comp f.unop g, map_add' := ⋯, map_smul' := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (X_1 : Cᵒᵖ) (g : ↑(((fun Y => (CategoryTheory.preadditiveYonedaObj Y).comp (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGrp)) X).obj X_1)), ((CategoryTheory.preadditiveYoneda.map f).app X_1) g = CategoryTheory.CategoryStruct.comp g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>Y : C<GOAL>CategoryTheory.preadditiveYoneda.obj Y = (CategoryTheory.preadditiveYonedaObj Y).comp (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGrp)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X : Cᵒᵖ<GOAL>∀ {X_1 Y : C} (f : X_1 ⟶ Y), (CategoryTheory.preadditiveCoyonedaObj X).map f = ModuleCat.ofHom { toFun := fun g => CategoryTheory.CategoryStruct.comp g f, map_add' := ⋯, map_smul' := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X : Cᵒᵖ<VAR>Y : C<GOAL>(CategoryTheory.preadditiveCoyonedaObj X).obj Y = ModuleCat.of (CategoryTheory.End X) (Opposite.unop X ⟶ Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>X : Cᵒᵖ<GOAL>CategoryTheory.preadditiveCoyoneda.obj X = (CategoryTheory.preadditiveCoyonedaObj X).comp (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End X)) AddCommGrp)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (Y_1 : C) (g : ↑(((fun X => (CategoryTheory.preadditiveCoyonedaObj X).comp (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End X)) AddCommGrp)) X).obj Y_1)), ((CategoryTheory.preadditiveCoyoneda.map f).app Y_1) g = CategoryTheory.CategoryStruct.comp f.unop g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<GOAL>CategoryTheory.preadditiveYoneda.comp ((CategoryTheory.whiskeringRight Cᵒᵖ AddCommGrp (Type v)).obj (CategoryTheory.forget AddCommGrp)) = CategoryTheory.yoneda
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<GOAL>CategoryTheory.preadditiveCoyoneda.comp ((CategoryTheory.whiskeringRight C AddCommGrp (Type v)).obj (CategoryTheory.forget AddCommGrp)) = CategoryTheory.coyoneda
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.InjectiveResolution Z<VAR>n : ℕ<GOAL>CategoryTheory.Injective (self.cocomplex.X n)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.InjectiveResolution Z<VAR>i : ℕ<GOAL>HomologicalComplex.HasHomology self.cocomplex i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.InjectiveResolution Z<GOAL>QuasiIso self.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>self : CategoryTheory.HasInjectiveResolution Z<GOAL>Nonempty (CategoryTheory.InjectiveResolution Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>self : CategoryTheory.HasInjectiveResolutions C<VAR>Z : C<GOAL>CategoryTheory.HasInjectiveResolution Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>I : CategoryTheory.InjectiveResolution Z<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt I.cocomplex (n + 1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>I : CategoryTheory.InjectiveResolution Z<VAR>n : ℕ<GOAL>(CategoryTheory.ShortComplex.mk (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>I : CategoryTheory.InjectiveResolution Z<VAR>n : ℕ<GOAL>I.ι.f (n + 1) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>I : CategoryTheory.InjectiveResolution Z<GOAL>CategoryTheory.CategoryStruct.comp (I.ι.f 0) (I.cocomplex.d 0 1) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>I : CategoryTheory.InjectiveResolution Z<VAR>n : ℕ<GOAL>CategoryTheory.CategoryStruct.comp (I.cocomplex.d n (n + 1)) (I.cocomplex.d (n + 1) (n + 2)) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>CategoryTheory.Injective Z<GOAL>(CategoryTheory.InjectiveResolution.self Z).cocomplex = (CochainComplex.single₀ C).obj Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Z : C<VAR>CategoryTheory.Injective Z<GOAL>(CategoryTheory.InjectiveResolution.self Z).ι = CategoryTheory.CategoryStruct.id ((CochainComplex.single₀ C).obj Z)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>Y Y' : D<VAR>h : Y ≅ Y'<VAR>hY : Y ∈ F.essImage<GOAL>Y' ∈ F.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>h : F ≅ F'<VAR>Y : D<VAR>hY : Y ∈ F.essImage<GOAL>Y ∈ F'.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>h : F ≅ F'<GOAL>F.essImage = F'.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D C<VAR>Y : D<GOAL>F.obj Y ∈ F.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>self : CategoryTheory.FullSubcategory F.essImage<GOAL>F.essImageInclusion.obj self = self.obj
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.InducedCategory D CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), F.essImageInclusion.map f = f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>(F.toEssImage.obj X).obj = F.obj X
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>∀ {X Y : C} (f : X ⟶ Y), F.toEssImage.map f = F.map f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>F.toEssImageCompEssentialImageInclusion.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>F.toEssImageCompEssentialImageInclusion.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>self : F.EssSurj<VAR>Y : D<GOAL>Y ∈ F.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>h : Function.Surjective F.obj<GOAL>F.EssSurj
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>F.EssSurj<VAR>α : F ≅ G<GOAL>G.EssSurj
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>(F.comp G).EssSurj<VAR>G.Faithful<VAR>G.Full<GOAL>F.EssSurj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_4} D₁<VAR>CategoryTheory.Category.{u_6, u_5} D₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>L₂.IsLocalization W₂<VAR>G : CategoryTheory.Functor C₁ D₂<VAR>G' : CategoryTheory.Functor D₁ D₂<VAR>CategoryTheory.Localization.Lifting L₁ W₁ G G'<VAR>F : CategoryTheory.Functor C₂ D₁<VAR>F' : CategoryTheory.Functor D₂ D₁<VAR>CategoryTheory.Localization.Lifting L₂ W₂ F F'<VAR>α : G.comp F' ≅ L₁<VAR>β : F.comp G' ≅ L₂<VAR>X : C₂<GOAL>(CategoryTheory.Localization.equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) = (CategoryTheory.Localization.Lifting.iso L₂ W₂ (F.comp G') (F'.comp G')).app X ≪≫ β.app X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_4} D₁<VAR>CategoryTheory.Category.{u_7, u_5} D₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>L₂.IsLocalization W₂<VAR>G : CategoryTheory.Functor C₁ D₂<VAR>G' : CategoryTheory.Functor D₁ D₂<VAR>CategoryTheory.Localization.Lifting L₁ W₁ G G'<VAR>F : CategoryTheory.Functor C₂ D₁<VAR>F' : CategoryTheory.Functor D₂ D₁<VAR>CategoryTheory.Localization.Lifting L₂ W₂ F F'<VAR>α : G.comp F' ≅ L₁<VAR>β : F.comp G' ≅ L₂<GOAL>G'.IsEquivalence
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>L₁ : CategoryTheory.Functor C₁ D<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>L₂ : CategoryTheory.Functor C₂ D<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>E : C₁ ≌ C₂<VAR>hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor<VAR>hW₂ : W₂.IsInvertedBy L₂<VAR>L₁.IsLocalization W₁<VAR>iso : E.functor.comp L₂ ≅ L₁<GOAL>L₂.IsLocalization W₂
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_4} D₁<VAR>CategoryTheory.Category.{u_9, u_5} D₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>E : C₁ ≌ C₂<VAR>E' : D₁ ≌ D₂<VAR>CategoryTheory.CatCommSq E.functor L₁ L₂ E'.functor<VAR>hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor<VAR>hW₂ : W₂.IsInvertedBy L₂<GOAL>L₂.IsLocalization W₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.Localization.LeftBousfield.W P f<VAR>Z : C<VAR>hZ : P Z<VAR>g : Y ⟶ Z<GOAL>(hf.homEquiv Z hZ) g = CategoryTheory.CategoryStruct.comp f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>P : C → Prop<GOAL>CategoryTheory.Localization.LeftBousfield.W (CategoryTheory.isoClosure P) = CategoryTheory.Localization.LeftBousfield.W P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.Localization.LeftBousfield.W P f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hX : P X<VAR>hY : P Y<GOAL>CategoryTheory.Localization.LeftBousfield.W P f ↔ CategoryTheory.IsIso f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : G ⊣ F<VAR>F.Full<VAR>F.Faithful<VAR>X : D<GOAL>CategoryTheory.Localization.LeftBousfield.W (fun x => x ∈ Set.range F.obj) (adj.unit.app X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : G ⊣ F<VAR>F.Full<VAR>F.Faithful<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Localization.LeftBousfield.W (fun x => x ∈ Set.range F.obj) f ↔ CategoryTheory.IsIso (G.map f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : G ⊣ F<VAR>F.Full<VAR>F.Faithful<GOAL>(CategoryTheory.Localization.LeftBousfield.W fun x => x ∈ Set.range F.obj) = (CategoryTheory.MorphismProperty.isomorphisms C).inverseImage G
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : G ⊣ F<VAR>F.Full<VAR>F.Faithful<GOAL>G.IsLocalization (CategoryTheory.Localization.LeftBousfield.W fun x => x ∈ Set.range F.obj)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α : F ⟶ G<GOAL>(CategoryTheory.NatTrans.appHom X) α = α.app X