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 w<VAR>CategoryTheory.Category.{max v u, w} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget 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>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>((CategoryTheory.plusPlusSheaf J D).obj P).val = J.sheafify 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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget 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>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>X : CategoryTheory.Functor Cᵒᵖ D<GOAL>(CategoryTheory.plusPlusAdjunction J D).unit.app X = J.toSheafify 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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget 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>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>Y : CategoryTheory.Sheaf J D<GOAL>((CategoryTheory.plusPlusAdjunction J D).counit.app Y).val = J.sheafifyLift (CategoryTheory.CategoryStruct.id Y.val) ⋯
<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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget 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>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>F G : CategoryTheory.Sheaf J D<VAR>f : F ⟶ G<GOAL>CategoryTheory.Mono f ↔ CategoryTheory.Mono f.val
<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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget 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>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>X : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.sheafificationIsoPresheafToSheafCompSheafToPreasheaf D).inv.app X = CategoryTheory.CategoryStruct.id (J.sheafify 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>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget 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>(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)<VAR>(CategoryTheory.forget D).ReflectsIsomorphisms<VAR>X : CategoryTheory.Functor Cᵒᵖ D<GOAL>(J.sheafificationIsoPresheafToSheafCompSheafToPreasheaf D).hom.app X = CategoryTheory.CategoryStruct.id (J.sheafify X)
<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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasRightCalculusOfFractions<VAR>n : ℕ<GOAL>(L.mapComposableArrows n).EssSurj
<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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>n : ℕ<GOAL>(L.mapComposableArrows n).EssSurj
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<VAR>self : CategoryTheory.NoetherianObject X<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<VAR>CategoryTheory.NoetherianObject X<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<VAR>self : CategoryTheory.ArtinianObject X<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : C<VAR>CategoryTheory.ArtinianObject X<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.Noetherian C<VAR>X : C<GOAL>CategoryTheory.NoetherianObject X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.Artinian C<VAR>X : C<GOAL>CategoryTheory.ArtinianObject X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : C<VAR>CategoryTheory.ArtinianObject X<VAR>h : ¬CategoryTheory.Limits.IsZero X<GOAL>∃ Y, CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>self : Φ.RightResolution X₂<GOAL>W₂ self.w
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>self : Φ.LeftResolution X₂<GOAL>W₂ self.w
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>R : Φ.RightResolution X₂<GOAL>∃ X₁ w, ∃ (hw : W₂ w), R = CategoryTheory.LocalizerMorphism.RightResolution.mk w hw
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>L : Φ.LeftResolution X₂<GOAL>∃ X₁ w, ∃ (hw : W₂ w), L = CategoryTheory.LocalizerMorphism.LeftResolution.mk w hw
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>R R' : Φ.RightResolution X₂<VAR>self : R.Hom R'<GOAL>CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map self.f) = R'.w
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>R R' : Φ.RightResolution X₂<VAR>self : R.Hom R'<GOAL>W₁ self.f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.ContainsIdentities<VAR>R : Φ.RightResolution X₂<GOAL>(CategoryTheory.LocalizerMorphism.RightResolution.Hom.id R).f = CategoryTheory.CategoryStruct.id R.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>R R' R'' : Φ.RightResolution X₂<VAR>φ : R.Hom R'<VAR>ψ : R'.Hom R''<GOAL>(φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>R : Φ.RightResolution X₂<GOAL>(CategoryTheory.CategoryStruct.id R).f = CategoryTheory.CategoryStruct.id R.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>R R' R'' : Φ.RightResolution X₂<VAR>φ : R ⟶ R'<VAR>ψ : R' ⟶ R''<GOAL>(CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>R R' : Φ.RightResolution X₂<VAR>φ₁ φ₂ : R ⟶ R'<VAR>h : φ₁.f = φ₂.f<GOAL>φ₁ = φ₂
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>L L' : Φ.LeftResolution X₂<VAR>self : L.Hom L'<GOAL>CategoryTheory.CategoryStruct.comp (Φ.functor.map self.f) L'.w = L.w
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>L L' : Φ.LeftResolution X₂<VAR>self : L.Hom L'<GOAL>W₁ self.f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.ContainsIdentities<VAR>L : Φ.LeftResolution X₂<GOAL>(CategoryTheory.LocalizerMorphism.LeftResolution.Hom.id L).f = CategoryTheory.CategoryStruct.id L.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>L L' L'' : Φ.LeftResolution X₂<VAR>φ : L.Hom L'<VAR>ψ : L'.Hom L''<GOAL>(φ.comp ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>L : Φ.LeftResolution X₂<GOAL>(CategoryTheory.CategoryStruct.id L).f = CategoryTheory.CategoryStruct.id L.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>L L' L'' : Φ.LeftResolution X₂<VAR>φ : L ⟶ L'<VAR>ψ : L' ⟶ L''<GOAL>(CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>L L' : Φ.LeftResolution X₂<VAR>φ₁ φ₂ : L ⟶ L'<VAR>h : φ₁.f = φ₂.f<GOAL>φ₁ = φ₂
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>L : Φ.LeftResolution X₂<GOAL>L.op.w = L.w.op
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>L : Φ.LeftResolution X₂<GOAL>L.op.X₁ = Opposite.op L.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂ᵒᵖ<VAR>L : Φ.op.LeftResolution X₂<GOAL>L.unop.X₁ = Opposite.unop L.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂ᵒᵖ<VAR>L : Φ.op.LeftResolution X₂<GOAL>L.unop.w = L.w.unop
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>L : Φ.RightResolution X₂<GOAL>L.op.w = L.w.op
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>L : Φ.RightResolution X₂<GOAL>L.op.X₁ = Opposite.op L.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂ᵒᵖ<VAR>L : Φ.op.RightResolution X₂<GOAL>L.unop.w = L.w.unop
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂ᵒᵖ<VAR>L : Φ.op.RightResolution X₂<GOAL>L.unop.X₁ = Opposite.unop L.X₁
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<GOAL>Nonempty (Φ.LeftResolution X₂) ↔ Nonempty (Φ.op.RightResolution (Opposite.op X₂))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_5, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<GOAL>Nonempty (Φ.RightResolution X₂) ↔ Nonempty (Φ.op.LeftResolution (Opposite.op X₂))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<GOAL>Φ.HasLeftResolutions ↔ Φ.op.HasRightResolutions
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<GOAL>Φ.HasRightResolutions ↔ Φ.op.HasLeftResolutions
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<VAR>L : (Φ.LeftResolution X₂)ᵒᵖ<GOAL>(CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂).obj L = (Opposite.unop L).op
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<GOAL>∀ {X Y : (Φ.LeftResolution X₂)ᵒᵖ} (φ : X ⟶ Y), ((CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂).map φ).f = φ.unop.f.op
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂ᵒᵖ<VAR>W₁.IsMultiplicative<GOAL>∀ {X Y : (Φ.op.RightResolution X₂)ᵒᵖ} (φ : X ⟶ Y), ((CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ X₂).map φ).f = φ.unop.f.unop
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂ᵒᵖ<VAR>W₁.IsMultiplicative<VAR>R : (Φ.op.RightResolution X₂)ᵒᵖ<GOAL>(CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ X₂).obj R = (Opposite.unop R).unop
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<GOAL>(CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).functor = CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<GOAL>(CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp.comp (CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<GOAL>(CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).inverse = (CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>X₂ : C₂<VAR>W₁.IsMultiplicative<GOAL>(CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (Φ.LeftResolution X₂)ᵒᵖ)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} 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>Φ.HasRightResolutions<GOAL>(Φ.functor.comp L₂).EssSurj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D₂<VAR>CategoryTheory.Category.{u_8, u_4} H<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>Φ.HasRightResolutions<VAR>F G : CategoryTheory.Functor D₂ H<VAR>α : F ⟶ G<GOAL>CategoryTheory.IsIso α ↔ ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} 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>Φ.HasLeftResolutions<GOAL>(Φ.functor.comp L₂).EssSurj
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C₁<VAR>CategoryTheory.Category.{u_6, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D₂<VAR>CategoryTheory.Category.{u_8, u_4} H<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>Φ.HasLeftResolutions<VAR>F G : CategoryTheory.Functor D₂ H<VAR>α : F ⟶ G<GOAL>CategoryTheory.IsIso α ↔ ∀ (X₁ : C₁), CategoryTheory.IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
<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 : Φ.IsRightDerivabilityStructure<GOAL>CategoryTheory.TwoSquare.GuitartExact (CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom
<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 : Φ.IsRightDerivabilityStructure<GOAL>Φ.HasRightResolutions
<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>D₁ : Type u_1<VAR>D₂ : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} D₁<VAR>CategoryTheory.Category.{u_3, u_2} D₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₁.IsLocalization W₁<VAR>L₂.IsLocalization W₂<VAR>F : CategoryTheory.Functor D₁ D₂<VAR>Φ.HasRightResolutions<VAR>e : Φ.functor.comp L₂ ≅ L₁.comp F<GOAL>Φ.IsRightDerivabilityStructure ↔ CategoryTheory.TwoSquare.GuitartExact e.hom