ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>h : Φ.IsRightDerivabilityStructure<VAR>e : Φ.functor.comp L₂ ≅ L₁.comp F<GOAL>CategoryTheory.TwoSquare.GuitartExact e.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>D₁ : Type u_1<VAR>D₂ : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} D₁<VAR>CategoryTheory.Category.{u_4, u_2} D₂<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₁.IsLocalization W₁<VAR>L₂.IsLocalization W₂<VAR>Φ.IsRightDerivabilityStructure<GOAL>CategoryTheory.TwoSquare.GuitartExact (CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C<GOAL>F = G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : CategoryTheory.OppositeShift C A<GOAL>(CategoryTheory.shiftFunctorZero (CategoryTheory.OppositeShift C A) A).inv.app X = ((CategoryTheory.shiftFunctorZero C A).hom.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : CategoryTheory.OppositeShift C A<GOAL>(CategoryTheory.shiftFunctorZero (CategoryTheory.OppositeShift C A) A).hom.app X = ((CategoryTheory.shiftFunctorZero C A).inv.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : CategoryTheory.OppositeShift C A<VAR>a b : A<GOAL>(CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).inv.app X = ((CategoryTheory.shiftFunctorAdd C a b).hom.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : CategoryTheory.OppositeShift C A<VAR>a b : A<GOAL>(CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).hom.app X = ((CategoryTheory.shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : CategoryTheory.OppositeShift C A<VAR>a b c : A<VAR>h : a + b = c<GOAL>(CategoryTheory.shiftFunctorAdd' (CategoryTheory.OppositeShift C A) a b c h).inv.app X = ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : CategoryTheory.OppositeShift C A<VAR>a b c : A<VAR>h : a + b = c<GOAL>(CategoryTheory.shiftFunctorAdd' (CategoryTheory.OppositeShift C A) a b c h).hom.app X = ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app (Opposite.unop X)).op
<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_8, u_2} C₁<VAR>CategoryTheory.Category.{u_10, u_3} C₂<VAR>CategoryTheory.Category.{u_11, u_5} D₁<VAR>CategoryTheory.Category.{u_9, u_6} 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>X Y : C₁<VAR>f : X ⟶ Y<GOAL>Φ.homMap L₁ L₂ (L₁.map f) = L₂.map (Φ.functor.map f)
<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_10, u_2} C₁<VAR>CategoryTheory.Category.{u_9, u_3} C₂<VAR>CategoryTheory.Category.{u_11, u_5} D₁<VAR>CategoryTheory.Category.{u_8, u_6} 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>X : C₁<GOAL>Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.id (L₁.obj X)) = CategoryTheory.CategoryStruct.id (L₂.obj (Φ.functor.obj X))
<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_9, u_2} C₁<VAR>CategoryTheory.Category.{u_11, u_3} C₂<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>CategoryTheory.Category.{u_10, u_6} 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>X Y Z : C₁<VAR>f : L₁.obj X ⟶ L₁.obj Y<VAR>g : L₁.obj Y ⟶ L₁.obj Z<GOAL>Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ f) (Φ.homMap L₁ L₂ g)
<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_10, u_2} C₁<VAR>CategoryTheory.Category.{u_11, u_3} C₂<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>CategoryTheory.Category.{u_9, u_6} 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>X Y : C₁<VAR>G : CategoryTheory.Functor D₁ D₂<VAR>e : Φ.functor.comp L₂ ≅ L₁.comp G<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>Φ.homMap L₁ L₂ f = CategoryTheory.CategoryStruct.comp (e.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.inv.app Y))
<VAR>C₁ : Type u_2<VAR>D₁ : Type u_5<VAR>CategoryTheory.Category.{u_9, u_2} C₁<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁.IsLocalization W₁<VAR>X Y : C₁<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(CategoryTheory.LocalizerMorphism.id W₁).homMap L₁ L₁ f = f
<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>CategoryTheory.Category.{u_9, u_2} C₁<VAR>CategoryTheory.Category.{u_12, u_3} C₂<VAR>CategoryTheory.Category.{u_11, u_4} C₃<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>CategoryTheory.Category.{u_13, u_6} D₂<VAR>CategoryTheory.Category.{u_10, u_7} D₃<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₃<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>L₂.IsLocalization W₂<VAR>L₃ : CategoryTheory.Functor C₃ D₃<VAR>L₃.IsLocalization W₃<VAR>X Y : C₁<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>CategoryTheory.Category.{u_9, u_5} D₁<VAR>CategoryTheory.Category.{u_10, u_6} D₂<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>X Y : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₂) f = (CategoryTheory.LocalizerMorphism.id W).homMap L₁ L₂ f
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_10, u_5} D₁<VAR>CategoryTheory.Category.{u_8, u_6} D₂<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>X Y : C<VAR>g : L₂.obj X ⟶ L₂.obj Y<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₂).symm g = (CategoryTheory.Localization.homEquiv W L₂ L₁) g
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_10, u_1} C<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>CategoryTheory.Category.{u_9, u_6} D₂<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>X Y : C<VAR>G : CategoryTheory.Functor D₁ D₂<VAR>e : L₁.comp G ≅ L₂<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₂) f = CategoryTheory.CategoryStruct.comp (e.inv.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.hom.app Y))
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>X Y : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₁) f = f
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>CategoryTheory.Category.{u_11, u_6} D₂<VAR>CategoryTheory.Category.{u_10, u_7} D₃<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>L₃ : CategoryTheory.Functor C D₃<VAR>L₃.IsLocalization W<VAR>X Y : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(CategoryTheory.Localization.homEquiv W L₂ L₃) ((CategoryTheory.Localization.homEquiv W L₁ L₂) f) = (CategoryTheory.Localization.homEquiv W L₁ L₃) f
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_8, u_5} D₁<VAR>CategoryTheory.Category.{u_10, u_6} D₂<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>X Y Z : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<VAR>g : L₁.obj Y ⟶ L₁.obj Z<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.homEquiv W L₁ L₂) f) ((CategoryTheory.Localization.homEquiv W L₁ L₂) g)
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>CategoryTheory.Category.{u_10, u_5} D₁<VAR>CategoryTheory.Category.{u_9, u_6} D₂<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₂) (L₁.map f) = L₂.map f
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_9, u_1} C<VAR>CategoryTheory.Category.{u_10, u_5} D₁<VAR>CategoryTheory.Category.{u_8, u_6} D₂<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>X : C<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.CategoryStruct.id (L₁.obj X)) = CategoryTheory.CategoryStruct.id (L₂.obj X)
<VAR>C : Type u_1<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>CategoryTheory.Category.{u_10, u_5} D₁<VAR>CategoryTheory.Category.{u_9, u_6} D₂<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₁.IsLocalization W<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>L₂.IsLocalization W<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>hf : W f<GOAL>(CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.Localization.isoOfHom L₁ W f hf).inv = (CategoryTheory.Localization.isoOfHom L₂ W f hf).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>L.CommShift M<VAR>X Y : C<GOAL>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔ ∀ (a b : M), Small.{w, v₂} ((CategoryTheory.shiftFunctor D a).obj (L.obj X) ⟶ (CategoryTheory.shiftFunctor D b).obj (L.obj Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y<GOAL>CategoryTheory.Localization.HasSmallLocalizedHom W X Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>W.IsCompatibleWithShift M<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>L.CommShift M<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W X Y<VAR>f : CategoryTheory.Localization.SmallHom W X Y<VAR>a : M<VAR>CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C a).obj X) ((CategoryTheory.shiftFunctor C a).obj Y)<GOAL>(CategoryTheory.Localization.SmallHom.equiv W L) (f.shift a) = CategoryTheory.CategoryStruct.comp ((L.commShiftIso a).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.Localization.SmallHom.equiv W L) f)) ((L.commShiftIso a).inv.app Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>W.IsCompatibleWithShift M<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>X Y : C<VAR>a : M<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y<VAR>f : CategoryTheory.Localization.SmallShiftedHom W X Y a<VAR>n a' : M<VAR>h : a + n = a'<GOAL>(CategoryTheory.Localization.SmallHom.equiv W L) (f.shift n a' h) = CategoryTheory.CategoryStruct.comp ((L.commShiftIso n).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Localization.SmallHom.equiv W L) f)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((L.commShiftIso a).hom.app Y)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)) ((L.commShiftIso a').inv.app Y))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>W.IsCompatibleWithShift M<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>X Y : C<VAR>a : M<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y<VAR>f : CategoryTheory.Localization.SmallShiftedHom W X Y a<VAR>n a' : M<VAR>h : a + n = a'<GOAL>(CategoryTheory.Localization.SmallShiftedHom.equiv W L) (f.shift n a' h) = CategoryTheory.CategoryStruct.comp ((L.commShiftIso n).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) f)) ((CategoryTheory.shiftFunctorAdd' D a n a' h).inv.app (L.obj Y)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>W.IsCompatibleWithShift M<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>X Y Z : C<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z<VAR>a b c : M<VAR>f : CategoryTheory.Localization.SmallShiftedHom W X Y a<VAR>g : CategoryTheory.Localization.SmallShiftedHom W Y Z b<VAR>h : b + a = c<GOAL>(CategoryTheory.Localization.SmallShiftedHom.equiv W L) (f.comp g h) = ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) f).comp ((CategoryTheory.Localization.SmallShiftedHom.equiv W L) g) h
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>X Y : C<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Localization.SmallShiftedHom.equiv W L) (CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f) = CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (L.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>M : Type w'<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>W.IsCompatibleWithShift M<VAR>X Y Z T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : M<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X T<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y T<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z T<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z<VAR>CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M T T<VAR>α : CategoryTheory.Localization.SmallShiftedHom W X Y a₁<VAR>β : CategoryTheory.Localization.SmallShiftedHom W Y Z a₂<VAR>γ : CategoryTheory.Localization.SmallShiftedHom W Z T a₃<VAR>h₁₂ : a₂ + a₁ = a₁₂<VAR>h₂₃ : a₃ + a₂ = a₂₃<VAR>h : a₃ + a₂ + a₁ = a<GOAL>(α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_5, u_3} D₁<VAR>CategoryTheory.Category.{u_7, u_4} D₂<VAR>G : CategoryTheory.Functor C₁ C₂<VAR>F : CategoryTheory.Functor C₂ C₁<VAR>adj : G ⊣ F<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>L₁.IsLocalization W₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>G' : CategoryTheory.Functor D₁ D₂<VAR>F' : CategoryTheory.Functor D₂ D₁<VAR>CategoryTheory.CatCommSq G L₁ L₂ G'<VAR>CategoryTheory.CatCommSq F L₂ L₁ F'<VAR>X₁ : C₁<GOAL>(CategoryTheory.Adjunction.Localization.ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) = CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) (F'.map ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').hom.app X₁)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} D₁<VAR>CategoryTheory.Category.{u_5, u_4} D₂<VAR>G : CategoryTheory.Functor C₁ C₂<VAR>F : CategoryTheory.Functor C₂ C₁<VAR>adj : G ⊣ F<VAR>L₁ : CategoryTheory.Functor C₁ D₁<VAR>L₂ : CategoryTheory.Functor C₂ D₂<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>L₂.IsLocalization W₂<VAR>G' : CategoryTheory.Functor D₁ D₂<VAR>F' : CategoryTheory.Functor D₂ D₁<VAR>CategoryTheory.CatCommSq G L₁ L₂ G'<VAR>CategoryTheory.CatCommSq F L₂ L₁ F'<VAR>X₂ : C₂<GOAL>(CategoryTheory.Adjunction.Localization.η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) = CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').inv.app X₂)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>CategoryTheory.Category.{u_6, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_5, u_3} D₁<VAR>CategoryTheory.Category.{u_7, u_4} D₂<VAR>G : CategoryTheory.Functor C₁ C₂<VAR>F : CategoryTheory.Functor C₂ C₁<VAR>adj : G ⊣ F<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 D₁ D₂<VAR>F' : CategoryTheory.Functor D₂ D₁<VAR>CategoryTheory.CatCommSq G L₁ L₂ G'<VAR>CategoryTheory.CatCommSq F L₂ L₁ F'<VAR>X₁ : C₁<GOAL>(adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) = CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) (F'.map ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').hom.app X₁)))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₁ : Type u_3<VAR>D₂ : Type u_4<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_7, u_2} C₂<VAR>CategoryTheory.Category.{u_6, u_3} D₁<VAR>CategoryTheory.Category.{u_5, u_4} D₂<VAR>G : CategoryTheory.Functor C₁ C₂<VAR>F : CategoryTheory.Functor C₂ C₁<VAR>adj : G ⊣ F<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 D₁ D₂<VAR>F' : CategoryTheory.Functor D₂ D₁<VAR>CategoryTheory.CatCommSq G L₁ L₂ G'<VAR>CategoryTheory.CatCommSq F L₂ L₁ F'<VAR>X₂ : C₂<GOAL>(adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) = CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').inv.app X₂)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) (L₂.map (adj.counit.app 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>G : CategoryTheory.Functor C₁ C₂<VAR>F : CategoryTheory.Functor C₂ C₁<VAR>adj : G ⊣ F<VAR>F.Full<VAR>F.Faithful<GOAL>G.IsLocalization ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<GOAL>W.IsInvertedBy W.Q
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G : CategoryTheory.Functor C D<VAR>hG : W.IsInvertedBy G<GOAL>∀ {X Y : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)} (f : X ⟶ Y), (CategoryTheory.Localization.Construction.liftToPathCategory G hG).map f = CategoryTheory.composePath ({ obj := fun X => G.obj X.obj, map := fun {X Y} a => Sum.rec (fun val => G.map val) (fun val => CategoryTheory.inv (G.map ↑val)) a }.mapPath f)
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G : CategoryTheory.Functor C D<VAR>hG : W.IsInvertedBy G<VAR>X : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)<GOAL>(CategoryTheory.Localization.Construction.liftToPathCategory G hG).obj X = G.obj X.obj
<VAR>C : Type uC<VAR>CategoryTheory.Category.{uC', uC} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>D : Type uD<VAR>CategoryTheory.Category.{uD', uD} D<VAR>G : CategoryTheory.Functor C D<VAR>hG : W.IsInvertedBy G<VAR>a : CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)<GOAL>(CategoryTheory.Localization.Construction.lift G hG).obj a = G.obj a.as.obj