ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>AddCommGroupWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>m n : S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj
<VAR>S : Type u_1<VAR>AddCommGroupWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>m n : S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj
<VAR>S : Type u_1<VAR>AddCommGroupWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.DifferentialObject.shiftZero C).hom.app X).f = (CategoryTheory.shiftFunctorZero C S).hom.app X.obj
<VAR>S : Type u_1<VAR>AddCommGroupWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.DifferentialObject.shiftZero C).inv.app X).f = (CategoryTheory.shiftFunctorZero C S).inv.app X.obj
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>E : Type u₅<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>F₁ F₂ : CategoryTheory.Functor (W₁.Localization × W₂.Localization) E<VAR>h : (W₁.Q.prod W₂.Q).comp F₁ = (W₁.Q.prod W₂.Q).comp F₂<GOAL>F₁ = F₂
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>E : Type u₅<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>F : CategoryTheory.Functor (C₁ × C₂) E<VAR>hF : (W₁.prod W₂).IsInvertedBy F<VAR>W₂.ContainsIdentities<GOAL>W₁.Q.comp (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF) = CategoryTheory.curry.obj F
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>E : Type u₅<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>F : CategoryTheory.Functor (C₁ × C₂) E<VAR>hF : (W₁.prod W₂).IsInvertedBy F<VAR>W₁.ContainsIdentities<VAR>W₂.ContainsIdentities<GOAL>W₂.Q.comp (CategoryTheory.curry.obj (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF)).flip = (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF).flip
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>E : Type u₅<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>F : CategoryTheory.Functor (C₁ × C₂) E<VAR>hF : (W₁.prod W₂).IsInvertedBy F<VAR>W₁.ContainsIdentities<VAR>W₂.ContainsIdentities<GOAL>(W₁.Q.prod W₂.Q).comp (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF) = F
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>W₁.ContainsIdentities<VAR>W₂.ContainsIdentities<GOAL>(W₁.Q.prod W₂.Q).IsLocalization (W₁.prod W₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : 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} D'<VAR>W : CategoryTheory.MorphismProperty C<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>L.IsLocalization W<VAR>L'.IsLocalization W<VAR>X : C<VAR>f : CategoryTheory.StructuredArrow (L.obj X) L<GOAL>(CategoryTheory.Localization.structuredArrowEquiv W L L') f = CategoryTheory.StructuredArrow.mk ((CategoryTheory.Localization.homEquiv W L L') f.hom)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : 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} D'<VAR>W : CategoryTheory.MorphismProperty C<VAR>L : CategoryTheory.Functor C D<VAR>L' : CategoryTheory.Functor C D'<VAR>L.IsLocalization W<VAR>L'.IsLocalization W<VAR>X : C<VAR>f : CategoryTheory.StructuredArrow (L'.obj X) L'<GOAL>(CategoryTheory.Localization.structuredArrowEquiv W L L').symm f = CategoryTheory.StructuredArrow.mk ((CategoryTheory.Localization.homEquiv W L' L) f.hom)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X : C<VAR>P : CategoryTheory.StructuredArrow (W.Q.obj X) W.Q → Prop<VAR>hP₀ : P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (W.Q.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁), P (CategoryTheory.StructuredArrow.mk φ) → P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp φ (W.Q.map f)))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂), P (CategoryTheory.StructuredArrow.mk φ) → P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Localization.isoOfHom W.Q W w hw).inv))<VAR>g : CategoryTheory.StructuredArrow (W.Q.obj X) W.Q<GOAL>P 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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>X : C<VAR>P : CategoryTheory.StructuredArrow (L.obj X) L → Prop<VAR>hP₀ : P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (CategoryTheory.StructuredArrow.mk φ) → P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp φ (L.map f)))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂), P (CategoryTheory.StructuredArrow.mk φ) → P (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Localization.isoOfHom L W w hw).inv))<VAR>g : CategoryTheory.StructuredArrow (L.obj X) L<GOAL>P 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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>Y : C<VAR>P : CategoryTheory.CostructuredArrow L (L.obj Y) → Prop<VAR>hP₀ : P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj Y)))<VAR>hP₁ : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y), P (CategoryTheory.CostructuredArrow.mk φ) → P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (L.map f) φ))<VAR>hP₂ : ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y), P (CategoryTheory.CostructuredArrow.mk φ) → P (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W w hw).inv φ))<VAR>g : CategoryTheory.CostructuredArrow L (L.obj Y)<GOAL>P g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.HasLocalization<GOAL>CategoryTheory.MorphismProperty.HasLocalization.L.IsLocalization W
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>X : C<VAR>S : (J.Cover X)ᵒᵖ<GOAL>(J.diagram P X).obj S = CategoryTheory.Limits.multiequalizer ((Opposite.unop S).index P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>X : C<VAR>S T : (J.Cover X)ᵒᵖ<VAR>f : S ⟶ T<GOAL>(J.diagram P X).map f = CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop T).index P) ((fun S => CategoryTheory.Limits.multiequalizer ((Opposite.unop S).index P)) S) (fun I => CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop S).index P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.map I f.unop)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>S : (J.Cover Y)ᵒᵖ<GOAL>(J.diagramPullback P f).app S = CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop ((J.pullback f).op.obj S)).index P) ((J.diagram P Y).obj S) (fun I => CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop S).index P) (CategoryTheory.GrothendieckTopology.Cover.Arrow.base I)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>X : C<VAR>W : (J.Cover X)ᵒᵖ<GOAL>(J.diagramNatTrans η X).app W = CategoryTheory.Limits.Multiequalizer.lift ((Opposite.unop W).index Q) ((J.diagram P X).obj W) (fun i => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index P) i) (η.app (Opposite.op i.Y))) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>J.diagramNatTrans (CategoryTheory.CategoryStruct.id P) X = CategoryTheory.CategoryStruct.id (J.diagram P X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>CategoryTheory.Preadditive D<VAR>X : C<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<GOAL>J.diagramNatTrans 0 X = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P Q R : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>X : C<GOAL>J.diagramNatTrans (CategoryTheory.CategoryStruct.comp η γ) X = CategoryTheory.CategoryStruct.comp (J.diagramNatTrans η X) (J.diagramNatTrans γ X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.diagramFunctor D X).obj P = J.diagram P X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>X : C<GOAL>∀ {X_1 Y : CategoryTheory.Functor Cᵒᵖ D} (η : X_1 ⟶ Y), (J.diagramFunctor D X).map η = J.diagramNatTrans η X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>J.plusMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (J.plusObj P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>CategoryTheory.Preadditive D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<GOAL>J.plusMap 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<GOAL>J.plusMap (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusMap γ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.plusFunctor D).obj P = J.plusObj P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<GOAL>∀ {X Y : CategoryTheory.Functor Cᵒᵖ D} (η : X ⟶ Y), (J.plusFunctor D).map η = J.plusMap η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp η (J.toPlus Q) = CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusMap η)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.toPlusNatTrans D).app P = J.toPlus P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<GOAL>J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>CategoryTheory.IsIso (J.toPlus P)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>(J.isoToPlus P hP).hom = J.toPlus P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<GOAL>CategoryTheory.CategoryStruct.comp (J.toPlus P) (J.plusLift η hQ) = η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<VAR>γ : J.plusObj P ⟶ Q<VAR>hγ : CategoryTheory.CategoryStruct.comp (J.toPlus P) γ = η<GOAL>γ = J.plusLift η hQ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η γ : J.plusObj P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<VAR>h : CategoryTheory.CategoryStruct.comp (J.toPlus P) η = CategoryTheory.CategoryStruct.comp (J.toPlus P) γ<GOAL>η = γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>(J.isoToPlus P hP).inv = J.plusLift (CategoryTheory.CategoryStruct.id P) hP
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q R : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : CategoryTheory.Presheaf.IsSheaf J R<GOAL>CategoryTheory.CategoryStruct.comp (J.plusMap η) (J.plusLift γ hR) = J.plusLift (CategoryTheory.CategoryStruct.comp η γ) hR
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>self : CategoryTheory.LocalizerMorphism W₁ W₂<GOAL>W₁ ≤ W₂.inverseImage self.functor
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<GOAL>(CategoryTheory.LocalizerMorphism.id W₁).functor = CategoryTheory.Functor.id C₁
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>W₃ : CategoryTheory.MorphismProperty C₃<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>Ψ : CategoryTheory.LocalizerMorphism W₂ W₃<GOAL>(Φ.comp Ψ).functor = Φ.functor.comp Ψ.functor
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<GOAL>Φ.op.functor = Φ.functor.op
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₂ : Type u₅<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₅, u₅} D₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<GOAL>W₁.IsInvertedBy (Φ.functor.comp L₂)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₄, u₄} D₁<VAR>CategoryTheory.Category.{v₅, u₅} D₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<VAR>G : CategoryTheory.Functor D₁ D₂<VAR>CategoryTheory.CatCommSq Φ.functor L₁ L₂ G<VAR>D₁' : Type u₄'<VAR>D₂' : Type u₅'<VAR>CategoryTheory.Category.{v₄', u₄'} D₁'<VAR>CategoryTheory.Category.{v₅', u₅'} D₂'<VAR>L₁' : CategoryTheory.Functor C₁ D₁'<VAR>L₂' : CategoryTheory.Functor C₂ D₂'<VAR>L₁'.IsLocalization W₁<VAR>L₂'.IsLocalization W₂<VAR>G' : CategoryTheory.Functor D₁' D₂'<VAR>CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'<VAR>G.IsEquivalence<GOAL>G'.IsEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₄, u₄} D₁<VAR>CategoryTheory.Category.{v₅, u₅} D₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<VAR>G : CategoryTheory.Functor D₁ D₂<VAR>CategoryTheory.CatCommSq Φ.functor L₁ L₂ G<VAR>D₁' : Type u₄'<VAR>D₂' : Type u₅'<VAR>CategoryTheory.Category.{v₄', u₄'} D₁'<VAR>CategoryTheory.Category.{v₅', u₅'} D₂'<VAR>L₁' : CategoryTheory.Functor C₁ D₁'<VAR>L₂' : CategoryTheory.Functor C₂ D₂'<VAR>L₁'.IsLocalization W₁<VAR>L₂'.IsLocalization W₂<VAR>G' : CategoryTheory.Functor D₁' D₂'<VAR>CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'<GOAL>G.IsEquivalence ↔ G'.IsEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>self : Φ.IsLocalizedEquivalence<GOAL>(Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>D₁ : Type u₄<VAR>D₂ : Type u₅<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₄, u₄} D₁<VAR>CategoryTheory.Category.{v₅, u₅} D₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<VAR>G : CategoryTheory.Functor D₁ D₂<VAR>CategoryTheory.CatCommSq Φ.functor L₁ L₂ G<VAR>G.IsEquivalence<GOAL>Φ.IsLocalizedEquivalence