ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X Y Z : C<VAR>CategoryTheory.Preadditive C<VAR>∀ (a : M), (CategoryTheory.shiftFunctor C a).Additive<VAR>a b c : M<VAR>α : CategoryTheory.ShiftedHom X Y a<VAR>β₁ β₂ : CategoryTheory.ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X Y Z : C<VAR>CategoryTheory.Preadditive C<VAR>a b c : M<VAR>α₁ α₂ : CategoryTheory.ShiftedHom X Y a<VAR>β : CategoryTheory.ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>(α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X Y Z : C<VAR>CategoryTheory.Preadditive C<VAR>∀ (a : M), (CategoryTheory.shiftFunctor C a).Additive<VAR>a b c : M<VAR>α : CategoryTheory.ShiftedHom X Y a<VAR>β : CategoryTheory.ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>α.comp (-β) h = -α.comp β h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X Y Z : C<VAR>CategoryTheory.Preadditive C<VAR>a b c : M<VAR>α : CategoryTheory.ShiftedHom X Y a<VAR>β : CategoryTheory.ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>(-α).comp β h = -α.comp β h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X Y : C<VAR>Z : C<VAR>CategoryTheory.Preadditive C<VAR>∀ (a : M), (CategoryTheory.shiftFunctor C a).PreservesZeroMorphisms<VAR>a : M<VAR>β : CategoryTheory.ShiftedHom X Y a<VAR>b c : M<VAR>h : b + a = c<GOAL>β.comp 0 h = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X : C<VAR>Y Z : C<VAR>CategoryTheory.Preadditive C<VAR>a : M<VAR>b c : M<VAR>β : CategoryTheory.ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>CategoryTheory.ShiftedHom.comp 0 β h = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>X Y : C<VAR>a : M<VAR>f : CategoryTheory.ShiftedHom X Y a<GOAL>f.map (CategoryTheory.Functor.id C) = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_7, u_3} E<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>CategoryTheory.HasShift E M<VAR>X Y : C<VAR>a : M<VAR>f : CategoryTheory.ShiftedHom X Y a<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift M<VAR>G : CategoryTheory.Functor D E<VAR>G.CommShift M<GOAL>f.map (F.comp G) = (f.map F).map G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>X Y Z : C<VAR>a b c : M<VAR>f : CategoryTheory.ShiftedHom X Y a<VAR>g : CategoryTheory.ShiftedHom Y Z b<VAR>h : b + a = c<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift M<GOAL>(f.comp g h).map F = (f.map F).comp (g.map F) h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.PullbackCone f f<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.Mono f ↔ c.fst = c.snd
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.PullbackCone f f<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.fst
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.PullbackCone f f<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>CategoryTheory.Mono f ↔ CategoryTheory.IsIso c.snd
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X) f f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.PushoutCocone f f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Epi f ↔ c.inl = c.inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.PushoutCocone f f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inl
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CategoryTheory.Limits.PushoutCocone f f<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Epi f ↔ CategoryTheory.IsIso c.inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ CategoryTheory.IsPushout f f (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction₂ X Y<GOAL>φ.symm.add = φ.add
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction₂ X Y<VAR>F : CategoryTheory.Functor C D<VAR>hF : W.IsInvertedBy F<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<GOAL>φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction X Y<VAR>hφ : f = φ.map L ⋯<GOAL>CategoryTheory.Localization.Preadditive.neg' W f = φ.neg.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>φ : W.LeftFraction₂ X Y<VAR>hφ₁ : f₁ = φ.fst.map L ⋯<VAR>hφ₂ : f₂ = φ.snd.map L ⋯<GOAL>CategoryTheory.Localization.Preadditive.add' W f₁ f₂ = φ.add.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<GOAL>CategoryTheory.Localization.Preadditive.add' W f₁ f₂ = CategoryTheory.Localization.Preadditive.add' W f₂ f₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>CategoryTheory.Localization.Preadditive.add' W f (L.map 0) = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>CategoryTheory.Localization.Preadditive.add' W (L.map 0) f = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.Localization.Preadditive.neg' W f) f = L.map 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f₁ f₂ f₃ : L.obj X ⟶ L.obj Y<GOAL>CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.Localization.Preadditive.add' W f₁ f₂) f₃ = CategoryTheory.Localization.Preadditive.add' W f₁ (CategoryTheory.Localization.Preadditive.add' W f₂ f₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f₁ f₂ : L.obj X ⟶ L.obj Y<VAR>g : L.obj Y ⟶ L.obj Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add' W f₁ f₂) g = CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f₁ g) (CategoryTheory.CategoryStruct.comp f₂ g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>g₁ g₂ : L.obj Y ⟶ L.obj Z<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.Localization.Preadditive.add' W g₁ g₂) = CategoryTheory.Localization.Preadditive.add' W (CategoryTheory.CategoryStruct.comp f g₁) (CategoryTheory.CategoryStruct.comp f g₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f₁ f₂ : X ⟶ Y<GOAL>CategoryTheory.Localization.Preadditive.add' W (L.map f₁) (L.map f₂) = L.map (f₁ + f₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>X Y : C<VAR>X' Y' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>f : X' ⟶ Y'<GOAL>(CategoryTheory.Localization.Preadditive.homEquiv eX eY) f = CategoryTheory.CategoryStruct.comp eX.hom (CategoryTheory.CategoryStruct.comp f eY.inv)
<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>X Y : C<VAR>X' Y' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>g : L.obj X ⟶ L.obj Y<GOAL>(CategoryTheory.Localization.Preadditive.homEquiv eX eY).symm g = CategoryTheory.CategoryStruct.comp eX.inv (CategoryTheory.CategoryStruct.comp g eY.hom)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f₁ f₂ : X' ⟶ Y'<VAR>g : Y' ⟶ Z'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂) g = CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f₁ g) (CategoryTheory.CategoryStruct.comp f₂ g)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>X' Y' Z' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>eZ : L.obj Z ≅ Z'<VAR>f : X' ⟶ Y'<VAR>g₁ g₂ : Y' ⟶ Z'<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.Localization.Preadditive.add W eY eZ g₁ g₂) = CategoryTheory.Localization.Preadditive.add W eX eZ (CategoryTheory.CategoryStruct.comp f g₁) (CategoryTheory.CategoryStruct.comp f g₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>X' Y' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>X'' Y'' : C<VAR>eX' : L.obj X'' ≅ X'<VAR>eY' : L.obj Y'' ≅ Y'<VAR>f₁ f₂ : X' ⟶ Y'<GOAL>CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂ = CategoryTheory.Localization.Preadditive.add W eX' eY' f₁ f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>X' Y' : D<VAR>eX : L.obj X ≅ X'<VAR>eY : L.obj Y ≅ Y'<VAR>f₁ f₂ : X' ⟶ Y'<GOAL>f₁ + f₂ = CategoryTheory.Localization.Preadditive.add W eX eY f₁ f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f₁ f₂ : X ⟶ Y<GOAL>L.map (f₁ + f₂) = L.map f₁ + L.map f₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<GOAL>L.Additive
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} E<VAR>CategoryTheory.Preadditive E<VAR>CategoryTheory.Preadditive D<VAR>L.Additive<VAR>G : CategoryTheory.Functor D E<GOAL>G.Additive ↔ (L.comp G).Additive
<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>self : p.IsCartesian f φ<VAR>a' : 𝒳<VAR>φ' : a' ⟶ b<VAR>p.IsHomLift f φ'<GOAL>∃! χ, p.IsHomLift (𝟙 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>self : p.IsStronglyCartesian f φ<VAR>a' : 𝒳<VAR>g : p.obj a' ⟶ R<VAR>φ' : a' ⟶ b<VAR>p.IsHomLift (g ≫ f) φ'<GOAL>∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
<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.IsCartesian f φ<VAR>a' : 𝒳<VAR>φ' : a' ⟶ b<VAR>p.IsHomLift f φ'<GOAL>CategoryTheory.Functor.IsCartesian.map p 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.IsCartesian f φ<VAR>a' : 𝒳<VAR>φ' : a' ⟶ b<VAR>p.IsHomLift f φ'<VAR>ψ : a' ⟶ a<VAR>p.IsHomLift (𝟙 R) ψ<VAR>hψ : ψ ≫ φ = φ'<GOAL>ψ = CategoryTheory.Functor.IsCartesian.map p 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.IsCartesian f φ<VAR>a' : 𝒳<VAR>ψ ψ' : a' ⟶ a<VAR>p.IsHomLift (𝟙 R) ψ<VAR>p.IsHomLift (𝟙 R) ψ'<VAR>h : ψ ≫ φ = ψ' ≫ φ<GOAL>ψ = ψ'
<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.IsCartesian f φ<GOAL>CategoryTheory.Functor.IsCartesian.map p f φ φ = 𝟙 a
<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.IsStronglyCartesian f φ<VAR>R' : 𝒮<VAR>a' : 𝒳<VAR>g : R' ⟶ R<VAR>f' : R' ⟶ S<VAR>hf' : f' = g ≫ f<VAR>φ' : a' ⟶ b<VAR>p.IsHomLift f' φ'<GOAL>∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
<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.IsStronglyCartesian f φ<VAR>R' : 𝒮<VAR>a' : 𝒳<VAR>g : R' ⟶ R<VAR>f' : R' ⟶ S<VAR>hf' : f' = g ≫ f<VAR>φ' : a' ⟶ b<VAR>p.IsHomLift f' φ'<GOAL>CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ' ≫ φ = φ'
<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.IsStronglyCartesian f φ<VAR>R' : 𝒮<VAR>a' : 𝒳<VAR>g : R' ⟶ R<VAR>f' : R' ⟶ S<VAR>hf' : f' = g ≫ f<VAR>φ' : a' ⟶ b<VAR>p.IsHomLift f' φ'<VAR>ψ : a' ⟶ a<VAR>p.IsHomLift g ψ<VAR>hψ : ψ ≫ φ = φ'<GOAL>ψ = CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ'
<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.IsStronglyCartesian f φ<VAR>R' : 𝒮<VAR>a' : 𝒳<VAR>g : R' ⟶ R<VAR>ψ ψ' : a' ⟶ a<VAR>p.IsHomLift g ψ<VAR>p.IsHomLift g ψ'<VAR>h : ψ ≫ φ = ψ' ≫ φ<GOAL>ψ = ψ'
<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.IsStronglyCartesian f φ<GOAL>CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ = 𝟙 a
<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.IsStronglyCartesian f φ<VAR>R' R'' : 𝒮<VAR>a' a'' : 𝒳<VAR>f' : R' ⟶ S<VAR>f'' : R'' ⟶ S<VAR>g : R' ⟶ R<VAR>g' : R'' ⟶ R'<VAR>H : f' = g ≫ f<VAR>H' : f'' = g' ≫ f'<VAR>φ' : a' ⟶ b<VAR>φ'' : a'' ⟶ b<VAR>p.IsStronglyCartesian f' φ'<VAR>p.IsHomLift f'' φ''<GOAL>CategoryTheory.Functor.IsStronglyCartesian.map p f' φ' H' φ'' ≫ CategoryTheory.Functor.IsStronglyCartesian.map p f φ H φ' = CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ''
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} 𝒮<VAR>CategoryTheory.Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S T : 𝒮<VAR>a b c : 𝒳<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>φ : a ⟶ b<VAR>ψ : b ⟶ c<VAR>p.IsStronglyCartesian g ψ<VAR>p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)<VAR>p.IsHomLift f φ<GOAL>p.IsStronglyCartesian 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.IsStronglyCartesian f φ<VAR>CategoryTheory.IsIso f<GOAL>CategoryTheory.IsIso φ
<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>self : p.IsHomLift f φ<GOAL>CategoryTheory.IsHomLiftAux p f φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R : 𝒮<VAR>a : 𝒳<VAR>ha : p.obj a = R<GOAL>p.IsHomLift (𝟙 R) (𝟙 a)
<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 φ<GOAL>p.obj a = 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 φ<GOAL>p.obj b = 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 φ<GOAL>f = CategoryTheory.eqToHom ⋯ ≫ p.map φ ≫ CategoryTheory.eqToHom ⋯
<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 φ<GOAL>p.map φ = CategoryTheory.eqToHom ⋯ ≫ f ≫ CategoryTheory.eqToHom ⋯
<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 φ<GOAL>CategoryTheory.CommSq (p.map φ) (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯) f
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>f : p.obj a ⟶ p.obj b<VAR>φ : a ⟶ b<VAR>p.IsHomLift f φ<GOAL>f = p.map φ
<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>ha : p.obj a = R<VAR>hb : p.obj b = S<VAR>h : f = CategoryTheory.eqToHom ⋯ ≫ p.map φ ≫ CategoryTheory.eqToHom hb<GOAL>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>ha : p.obj a = R<VAR>hb : p.obj b = S<VAR>h : p.map φ = CategoryTheory.eqToHom ha ≫ f ≫ CategoryTheory.eqToHom ⋯<GOAL>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>ha : p.obj a = R<VAR>hb : p.obj b = S<VAR>h : CategoryTheory.CommSq (p.map φ) (CategoryTheory.eqToHom ha) (CategoryTheory.eqToHom hb) f<GOAL>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 c : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>p.IsHomLift f φ<VAR>T : 𝒮<VAR>ψ : b ⟶ c<VAR>p.IsHomLift (𝟙 T) ψ<GOAL>p.IsHomLift f (φ ≫ ψ)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b c : 𝒳<VAR>R : 𝒮<VAR>φ : a ⟶ b<VAR>p.IsHomLift (𝟙 R) φ<VAR>S T : 𝒮<VAR>f : S ⟶ T<VAR>ψ : b ⟶ c<VAR>p.IsHomLift f ψ<GOAL>p.IsHomLift f (φ ≫ ψ)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>hab : a = b<VAR>R : 𝒮<VAR>hR : p.obj a = R<GOAL>p.IsHomLift (𝟙 R) (CategoryTheory.eqToHom hab)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>hab : a = b<VAR>S : 𝒮<VAR>hS : p.obj b = S<GOAL>p.IsHomLift (𝟙 S) (CategoryTheory.eqToHom hab)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>hRS : R = S<VAR>a : 𝒳<VAR>ha : p.obj a = R<GOAL>p.IsHomLift (CategoryTheory.eqToHom hRS) (𝟙 a)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>hRS : R = S<VAR>b : 𝒳<VAR>hb : p.obj b = S<GOAL>p.IsHomLift (CategoryTheory.eqToHom hRS) (𝟙 b)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>CategoryTheory.Category.{v₁, u₂} 𝒳<VAR>CategoryTheory.Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a' a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>h : a' = a<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 b' : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>h : b = b'<GOAL>p.IsHomLift f (φ ≫ CategoryTheory.eqToHom h) ↔ p.IsHomLift f φ