ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R' R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>h : R' = R<GOAL>p.IsHomLift (CategoryTheory.eqToHom h ≫ f) φ ↔ p.IsHomLift f φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S S' : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>h : S = S'<GOAL>p.IsHomLift (f ≫ CategoryTheory.eqToHom h) φ ↔ p.IsHomLift f φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ≅ b<VAR>p.IsHomLift f φ.hom<GOAL>(CategoryTheory.IsHomLift.isoOfIsoLift p f φ).hom = f
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ≅ b<VAR>p.IsHomLift f φ.hom<GOAL>(CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv ≫ f = 𝟙 S
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ≅ b<VAR>p.IsHomLift f φ.hom<GOAL>f ≫ (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv = 𝟙 R
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>p.IsHomLift f φ<VAR>CategoryTheory.IsIso φ<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>self : F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>CategoryTheory.Functor.ShiftSequence.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha') ≪≫ CategoryTheory.Functor.ShiftSequence.shiftIso m a' a'' ha''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>self : F.ShiftSequence M<VAR>a : M<GOAL>CategoryTheory.Functor.ShiftSequence.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫ (CategoryTheory.Functor.ShiftSequence.sequence F a).leftUnitor
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>X Y : C<VAR>n a a' : M<VAR>ha' : n + a = a'<VAR>f : X ⟶ Y<GOAL>(F.shift a).map ((CategoryTheory.shiftFunctor C n).map f) ≫ (F.shiftIso n a a' ha').hom.app Y = (F.shiftIso n a a' ha').hom.app X ≫ (F.shift a').map f
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>X Y : C<VAR>n a a' : M<VAR>ha' : n + a = a'<VAR>f : X ⟶ Y<GOAL>(F.shift a').map f ≫ (F.shiftIso n a a' ha').inv.app Y = (F.shiftIso n a a' ha').inv.app X ≫ (F.shift a).map ((CategoryTheory.shiftFunctor C n).map f)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n : M<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.map ((CategoryTheory.shiftFunctor C n).map f) ≫ (F.isoShift n).hom.app Y = (F.isoShift n).hom.app X ≫ (F.shift n).map f
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n : M<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(F.shift n).map f ≫ (F.isoShift n).inv.app Y = (F.isoShift n).inv.app X ≫ F.map ((CategoryTheory.shiftFunctor C n).map f)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>a : M<GOAL>F.shiftIso 0 a a ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C M) (F.shift a) ≪≫ (F.shift a).leftUnitor
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>a : M<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).hom.app X = (F.shift a).map ((CategoryTheory.shiftFunctorZero C M).hom.app X)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>a : M<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).inv.app X = (F.shift a).map ((CategoryTheory.shiftFunctorZero C M).inv.app X)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>F.shiftIso (m + n) a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n) (F.shift a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (F.shift a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).hom.app X = (F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X) ≫ (F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).inv.app X = (F.shiftIso m a' a'' ha'').inv.app X ≫ (F.shiftIso n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X) ≫ (F.shift a).map ((CategoryTheory.shiftFunctorAdd C m n).inv.app X)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>F.shiftIso mn a a'' ⋯ = CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C m n mn hnm) (F.shift a) ≪≫ (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n) (F.shift a) ≪≫ CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C m) (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso mn a a'' ⋯).hom.app X = (F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).hom.app X) ≫ (F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso mn a a'' ⋯).inv.app X = (F.shiftIso m a' a'' ha'').inv.app X ≫ (F.shiftIso n a a' ha').inv.app ((CategoryTheory.shiftFunctor C m).obj X) ≫ (F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso n a a' ha').hom.app ((CategoryTheory.shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X = (F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app X) ≫ (F.shiftIso mn a a'' ⋯).hom.app X
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>X Y Z : C<VAR>n : M<VAR>f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y<VAR>g : Y ⟶ Z<VAR>a a' : M<VAR>ha' : n + a = a'<GOAL>F.shiftMap (f ≫ (CategoryTheory.shiftFunctor C n).map g) a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>X Y Z : C<VAR>n : M<VAR>f : X ⟶ Y<VAR>g : Y ⟶ (CategoryTheory.shiftFunctor C n).obj Z<VAR>a a' : M<VAR>ha' : n + a = a'<GOAL>F.shiftMap (f ≫ g) a a' ha' = (F.shift a).map f ≫ F.shiftMap g a a' ha'
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>X Y : C<VAR>m : M<VAR>f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y<VAR>n mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>(F.shiftIso n a a' ha').hom.app X ≫ F.shiftMap f a' a'' ha'' = (F.shift a).map ((CategoryTheory.shiftFunctor C n).map f) ≫ (F.shift a).map ((CategoryTheory.shiftFunctorAdd' C m n mn hnm).inv.app Y) ≫ (F.shiftIso mn a a'' ⋯).hom.app Y
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>G : Type u_4<VAR>AddGroup G<VAR>CategoryTheory.HasShift C G<VAR>F.ShiftSequence G<VAR>X Y : C<VAR>m : G<VAR>f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y<VAR>n : G<VAR>hnm : n + m = 0<VAR>a a' : G<VAR>ha' : m + a = a'<GOAL>(F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' = (F.shift a').map ((CategoryTheory.shiftFunctor C n).map f ≫ (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app Y)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>F.ShiftSequence M<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroMorphisms A<VAR>F.PreservesZeroMorphisms<VAR>∀ (n : M), (CategoryTheory.shiftFunctor C n).PreservesZeroMorphisms<VAR>X Y : C<VAR>n a a' : M<VAR>ha' : n + a = a'<GOAL>F.shiftMap 0 a a' ha' = 0
<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>self : L.IsLocalization W<GOAL>W.IsInvertedBy L
<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>self : L.IsLocalization W<GOAL>(CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence
<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>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E<GOAL>W.IsInvertedBy L
<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>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E<VAR>F : CategoryTheory.Functor C E<VAR>hF : W.IsInvertedBy F<GOAL>L.comp (self.lift F hF) = 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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E<VAR>F₁ F₂ : CategoryTheory.Functor D E<GOAL>L.comp F₁ = L.comp F₂ → F₁ = F₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>G : CategoryTheory.Functor C E<VAR>hG : W.IsInvertedBy G<GOAL>(CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ W E).lift G hG = CategoryTheory.Localization.Construction.lift G hG
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>hW : W ≤ CategoryTheory.MorphismProperty.isomorphisms C<VAR>F : CategoryTheory.Functor C E<GOAL>∀ (x : W.IsInvertedBy F), (CategoryTheory.Localization.strictUniversalPropertyFixedTargetId W E hW).lift F x = 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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>h₁ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W D<VAR>h₂ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W W.Localization<GOAL>L.IsLocalization W
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>hW : W ≤ CategoryTheory.MorphismProperty.isomorphisms C<GOAL>(CategoryTheory.Functor.id C).IsLocalization W
<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<GOAL>W.IsInvertedBy L
<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 Y : C<VAR>f : X ⟶ Y<VAR>hf : W f<GOAL>(CategoryTheory.Localization.isoOfHom L W f hf).hom = L.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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : W f<GOAL>CategoryTheory.CategoryStruct.comp (L.map f) (CategoryTheory.Localization.isoOfHom L W f hf).inv = CategoryTheory.CategoryStruct.id (L.obj X)
<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 Y : C<VAR>f : X ⟶ Y<VAR>hf : W f<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W f hf).inv (L.map f) = CategoryTheory.CategoryStruct.id (L.obj Y)
<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>hX : W (CategoryTheory.CategoryStruct.id X)<GOAL>(CategoryTheory.Localization.isoOfHom L W (CategoryTheory.CategoryStruct.id X) hX).inv = CategoryTheory.CategoryStruct.id (L.obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : W f<GOAL>CategoryTheory.Localization.Construction.wIso f hf = CategoryTheory.Localization.isoOfHom W.Q W f hf
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : W f<GOAL>CategoryTheory.Localization.Construction.wInv f hf = (CategoryTheory.Localization.isoOfHom W.Q W f hf).inv
<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<GOAL>L.EssSurj
<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>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>L.IsLocalization W<GOAL>CategoryTheory.Localization.whiskeringLeftFunctor' L W E = (CategoryTheory.Localization.whiskeringLeftFunctor L W E).comp (CategoryTheory.inducedFunctor CategoryTheory.FullSubcategory.obj)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>L.IsLocalization W<VAR>F : CategoryTheory.Functor D E<GOAL>(CategoryTheory.Localization.whiskeringLeftFunctor' L W E).obj F = L.comp 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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>E : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} E<GOAL>((CategoryTheory.whiskeringLeft C D E).obj L).Full
<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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>E : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} E<GOAL>((CategoryTheory.whiskeringLeft C D E).obj L).Faithful
<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>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>F₁ F₂ : CategoryTheory.Functor D E<VAR>τ τ' : F₁ ⟶ F₂<VAR>h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)<GOAL>τ = τ'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>L.IsLocalization W<VAR>F₁ F₂ : CategoryTheory.Functor C E<VAR>F₁' F₂' : CategoryTheory.Functor D E<VAR>CategoryTheory.Localization.Lifting L W F₁ F₁'<VAR>CategoryTheory.Localization.Lifting L W F₂ F₂'<VAR>τ : F₁ ⟶ F₂<VAR>X : C<GOAL>(CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ).app (L.obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F₁ F₁').hom.app X) (CategoryTheory.CategoryStruct.comp (τ.app X) ((CategoryTheory.Localization.Lifting.iso L W F₂ F₂').inv.app X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>L.IsLocalization W<VAR>F₁ F₂ F₃ : CategoryTheory.Functor C E<VAR>F₁' F₂' F₃' : CategoryTheory.Functor D E<VAR>h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'<VAR>h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'<VAR>h₃ : CategoryTheory.Localization.Lifting L W F₃ F₃'<VAR>τ : F₁ ⟶ F₂<VAR>τ' : F₂ ⟶ F₃<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ) (CategoryTheory.Localization.liftNatTrans L W F₂ F₃ F₂' F₃' τ') = CategoryTheory.Localization.liftNatTrans L W F₁ F₃ F₁' F₃' (CategoryTheory.CategoryStruct.comp τ τ')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} E<VAR>L.IsLocalization W<VAR>F : CategoryTheory.Functor C E<VAR>F' : CategoryTheory.Functor D E<VAR>h : CategoryTheory.Localization.Lifting L W F F'<GOAL>CategoryTheory.Localization.liftNatTrans L W F F F' F' (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id 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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>L.IsLocalization W<VAR>F₁ F₂ : CategoryTheory.Functor C E<VAR>F₁' F₂' : CategoryTheory.Functor D E<VAR>h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'<VAR>h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'<VAR>e : F₁ ≅ F₂<GOAL>(CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).inv = CategoryTheory.Localization.liftNatTrans L W F₂ F₁ F₂' F₁' e.inv
<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>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>L.IsLocalization W<VAR>F₁ F₂ : CategoryTheory.Functor C E<VAR>F₁' F₂' : CategoryTheory.Functor D E<VAR>h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'<VAR>h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂'<VAR>e : F₁ ≅ F₂<GOAL>(CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).hom = CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' e.hom
<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>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_7, u_3} E<VAR>E' : Type u_4<VAR>CategoryTheory.Category.{u_8, u_4} E'<VAR>F : CategoryTheory.Functor C E<VAR>F' : CategoryTheory.Functor D E<VAR>CategoryTheory.Localization.Lifting L W F F'<VAR>G : CategoryTheory.Functor E E'<GOAL>CategoryTheory.Localization.Lifting.iso' W = CategoryTheory.isoWhiskerRight (CategoryTheory.Localization.Lifting.iso L W F F') 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<GOAL>CategoryTheory.Localization.Lifting.iso' W = L.rightUnitor
<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>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>F : CategoryTheory.Functor D E<GOAL>CategoryTheory.Localization.Lifting.iso' W = CategoryTheory.Iso.refl (L.comp F)