ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>M : CategoryTheory.Mat_ C<GOAL>M.isoBiproductEmbedding.inv = CategoryTheory.Limits.biproduct.desc fun i j k => if h : i = k then CategoryTheory.eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Mat_ C ⥤ D<VAR>F.Additive<VAR>M : CategoryTheory.Mat_ C<VAR>i : M.ι<GOAL>(CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom ≫ CategoryTheory.Limits.biproduct.π (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i = F.map (M.isoBiproductEmbedding.hom ≫ CategoryTheory.Limits.biproduct.π (fun i => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>F : CategoryTheory.Mat_ C ⥤ D<VAR>F.Additive<VAR>M : CategoryTheory.Mat_ C<VAR>i : M.ι<GOAL>CategoryTheory.Limits.biproduct.ι (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i ≫ (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv = F.map (CategoryTheory.Limits.biproduct.ι (fun i => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i ≫ M.isoBiproductEmbedding.inv)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasFiniteBiproducts D<VAR>F : CategoryTheory.Mat_ C ⥤ D<VAR>F.Additive<VAR>M N : CategoryTheory.Mat_ C<VAR>f : M ⟶ N<GOAL>F.map f ≫ (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).hom = (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom ≫ CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasFiniteBiproducts D<VAR>F : CategoryTheory.Mat_ C ⥤ D<VAR>F.Additive<VAR>M N : CategoryTheory.Mat_ C<VAR>f : M ⟶ N<GOAL>(CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv ≫ F.map f = (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) ≫ (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasFiniteBiproducts D<VAR>F : C ⥤ D<VAR>F.Additive<GOAL>∀ {X Y : CategoryTheory.Mat_ C} (f : X ⟶ Y), (CategoryTheory.Mat_.lift F).map f = CategoryTheory.Limits.biproduct.matrix fun i j => F.map (f i j)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasFiniteBiproducts D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>X : CategoryTheory.Mat_ C<GOAL>(CategoryTheory.Mat_.lift F).obj X = ⨁ fun i => F.obj (X.X i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasFiniteBiproducts D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>X : C<GOAL>(CategoryTheory.Mat_.embeddingLiftIso F).hom.app X = CategoryTheory.Limits.biproduct.desc fun x => 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Limits.HasFiniteBiproducts D<VAR>F : C ⥤ D<VAR>F.Additive<VAR>X : C<GOAL>(CategoryTheory.Mat_.embeddingLiftIso F).inv.app X = CategoryTheory.Limits.biproduct.lift fun x => 𝟙 (F.obj X)
<VAR>C : Type (u₁ + 1)<VAR>CategoryTheory.LargeCategory C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<GOAL>(CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).functor = CategoryTheory.Mat_.lift (𝟭 C)
<VAR>C : Type (u₁ + 1)<VAR>CategoryTheory.LargeCategory C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteBiproducts C<GOAL>(CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).inverse = CategoryTheory.Mat_.embedding C
<VAR>R : Type u<VAR>Semiring R<VAR>X Y : CategoryTheory.Mat R<VAR>f g : X ⟶ Y<VAR>h : ∀ (i : ↑X) (j : ↑Y), f i j = g i j<GOAL>f = g
<VAR>R : Type u<VAR>Semiring R<VAR>M : CategoryTheory.Mat R<GOAL>𝟙 M = fun i j => if i = j then 1 else 0
<VAR>R : Type u<VAR>Semiring R<VAR>M : CategoryTheory.Mat R<VAR>i j : ↑M<GOAL>𝟙 M i j = if i = j then 1 else 0
<VAR>R : Type u<VAR>Semiring R<VAR>M : CategoryTheory.Mat R<VAR>i : ↑M<GOAL>𝟙 M i i = 1
<VAR>R : Type u<VAR>Semiring R<VAR>M : CategoryTheory.Mat R<VAR>i j : ↑M<VAR>h : i ≠ j<GOAL>𝟙 M i j = 0
<VAR>R : Type u<VAR>Semiring R<VAR>M N K : CategoryTheory.Mat R<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>f ≫ g = fun i k => ∑ j : ↑N, f i j * g j k
<VAR>R : Type u<VAR>Semiring R<VAR>M N K : CategoryTheory.Mat R<VAR>f : M ⟶ N<VAR>g : N ⟶ K<VAR>i : ↑M<VAR>k : ↑K<GOAL>(f ≫ g) i k = ∑ j : ↑N, f i j * g j k
<VAR>R : Type<VAR>Ring R<GOAL>∀ {X Y : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)} (f : X ⟶ Y) (i : ↑((fun X => FintypeCat.of X.ι) X)) (j : ↑((fun X => FintypeCat.of X.ι) Y)), (CategoryTheory.Mat.equivalenceSingleObjInverse R).map f i j = MulOpposite.unop (f i j)
<VAR>R : Type<VAR>Ring R<VAR>X : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)<GOAL>(CategoryTheory.Mat.equivalenceSingleObjInverse R).obj X = FintypeCat.of X.ι
<VAR>R : Type<VAR>Ring R<VAR>M N : CategoryTheory.Mat R<VAR>f g : M ⟶ N<VAR>i : ↑M<VAR>j : ↑N<GOAL>(f + g) i j = f i j + g i j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>r : HomRel C<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>self : r.IsCompatibleWithShift A<VAR>a : A<VAR>X Y : C<VAR>f g : X ⟶ Y<GOAL>r f g → r ((CategoryTheory.shiftFunctor C a).map f) ((CategoryTheory.shiftFunctor C a).map g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ⥤ D<VAR>r : HomRel C<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>r.IsCompatibleWithShift A<VAR>F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.Quotient.LiftCommShift.iso F r hF a).hom.app ((CategoryTheory.Quotient.functor r).obj X) = (CategoryTheory.Quotient.lift r F hF).map (((CategoryTheory.Quotient.functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>F : C ⥤ D<VAR>r : HomRel C<VAR>A : Type w<VAR>AddMonoid A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.HasShift D A<VAR>r.IsCompatibleWithShift A<VAR>F.CommShift A<VAR>hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>a : A<VAR>X : C<GOAL>(CategoryTheory.Quotient.LiftCommShift.iso F r hF a).inv.app ((CategoryTheory.Quotient.functor r).obj X) = (F.commShiftIso a).inv.app X ≫ (CategoryTheory.Quotient.lift r F hF).map (((CategoryTheory.Quotient.functor r).commShiftIso a).hom.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>self : W.LeftFraction₂ X Y<GOAL>W self.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>self : W.LeftFraction₃ X Y<GOAL>W self.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>self : W.RightFraction₂ X Y<GOAL>W self.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction₂ X Y<VAR>h : CategoryTheory.MorphismProperty.LeftFraction₂Rel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z₁.fst z₂.fst
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction₂ X Y<VAR>h : CategoryTheory.MorphismProperty.LeftFraction₂Rel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z₁.snd z₂.snd
<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>X Y : C<VAR>φ ψ : W.LeftFraction₂ X Y<GOAL>φ.fst.map L ⋯ = ψ.fst.map L ⋯ ∧ φ.snd.map L ⋯ = ψ.snd.map L ⋯ ↔ CategoryTheory.MorphismProperty.LeftFraction₂Rel φ ψ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction₂ X Y<VAR>W.HasLeftCalculusOfFractions<GOAL>∃ ψ, CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f ∧ CategoryTheory.CategoryStruct.comp φ.f' ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.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>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>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.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>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>∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<VAR>α β : A₁ ⟶ A₂<GOAL>(α - β).f = α.f - β.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<VAR>α β : A₁ ⟶ A₂<GOAL>(α + β).f = α.f + β.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<VAR>r : ℤ<VAR>α : A₁ ⟶ A₂<GOAL>(r • α).f = r • α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<VAR>α : A₁ ⟶ A₂<GOAL>(-α).f = -α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<VAR>n : ℕ<VAR>α : A₁ ⟶ A₂<GOAL>(n • α).f = n • α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Algebra F<GOAL>CategoryTheory.Endofunctor.Algebra.Hom.f 0 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F<VAR>α β : A₁ ⟶ A₂<GOAL>(α + β).f = α.f + β.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F<VAR>α β : A₁ ⟶ A₂<GOAL>(α - β).f = α.f - β.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F<GOAL>CategoryTheory.Endofunctor.Coalgebra.Hom.f 0 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F<VAR>n : ℕ<VAR>α : A₁ ⟶ A₂<GOAL>(n • α).f = n • α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F<VAR>α : A₁ ⟶ A₂<GOAL>(-α).f = -α.f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Preadditive C<VAR>F : CategoryTheory.Functor C C<VAR>F.Additive<VAR>A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F<VAR>r : ℤ<VAR>α : A₁ ⟶ A₂<GOAL>(r • α).f = r • α.f
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_4, 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>W₁.IsMultiplicative<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} D<VAR>L : CategoryTheory.Functor C₂ D<VAR>L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>R R' : Φ.RightResolution X₂<VAR>φ : R ⟶ R'<GOAL>(CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y).map φ = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.homMk φ.f ⋯) ⋯
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_4, 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>W₁.IsMultiplicative<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} D<VAR>L : CategoryTheory.Functor C₂ D<VAR>L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>R : Φ.RightResolution X₂<GOAL>(CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution Φ L y).obj R = CategoryTheory.CostructuredArrow.mk (CategoryTheory.StructuredArrow.homMk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.isoOfHom L W₂ R.w ⋯).inv y) ⋯)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_4, 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>W₁.IsMultiplicative<VAR>∀ (X₂ : C₂), CategoryTheory.IsConnected (Φ.RightResolution X₂)<VAR>Φ.arrow.HasRightResolutions<VAR>W₂.ContainsIdentities<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} D<VAR>L : CategoryTheory.Functor C₂ D<VAR>L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<GOAL>CategoryTheory.IsConnected ((CategoryTheory.TwoSquare.mk Φ.functor (Φ.functor.comp L) L (CategoryTheory.Functor.id D) (Φ.functor.comp L).rightUnitor.inv).CostructuredArrowDownwards y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C₁<VAR>CategoryTheory.Category.{u_4, u_2} C₂<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>Φ : CategoryTheory.LocalizerMorphism W₁ W₂<VAR>Φ.IsLocalizedEquivalence<VAR>W₁.IsMultiplicative<VAR>∀ (X₂ : C₂), CategoryTheory.IsConnected (Φ.RightResolution X₂)<VAR>Φ.arrow.HasRightResolutions<VAR>W₂.ContainsIdentities<GOAL>Φ.IsRightDerivabilityStructure
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>P : C → Prop<VAR>h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasLimit F<GOAL>(∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.limit F)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>P : C → Prop<VAR>h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P<VAR>F : J ⥤ C<VAR>CategoryTheory.Limits.HasColimit F<GOAL>(∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.colimit F)
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C → Prop<VAR>h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P<VAR>F : J ⥤ CategoryTheory.FullSubcategory P<VAR>CategoryTheory.Limits.HasLimit (F ⋙ CategoryTheory.fullSubcategoryInclusion P)<GOAL>CategoryTheory.Limits.HasLimit F
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C → Prop<VAR>h : CategoryTheory.Limits.ClosedUnderLimitsOfShape J P<VAR>CategoryTheory.Limits.HasLimitsOfShape J C<GOAL>CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.FullSubcategory P)
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C → Prop<VAR>h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P<VAR>F : J ⥤ CategoryTheory.FullSubcategory P<VAR>CategoryTheory.Limits.HasColimit (F ⋙ CategoryTheory.fullSubcategoryInclusion P)<GOAL>CategoryTheory.Limits.HasColimit F
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : C → Prop<VAR>h : CategoryTheory.Limits.ClosedUnderColimitsOfShape J P<VAR>CategoryTheory.Limits.HasColimitsOfShape J C<GOAL>CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.FullSubcategory P)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Full<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Faithful<VAR>X : C<GOAL>(CategoryTheory.Functor.ShiftSequence.induced.isoZero e M F' e').hom.app (L.obj X) = (e' 0).hom.app X ≫ (G.isoShiftZero M).hom.app X ≫ e.inv.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>L : C ⥤ D<VAR>G : C ⥤ A<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Full<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Faithful<VAR>n a a' : M<VAR>ha' : n + a = a'<VAR>X : C<GOAL>(CategoryTheory.Functor.ShiftSequence.induced.shiftIso L G M F' e' n a a' ha').hom.app (L.obj X) = (F' a).map ((L.commShiftIso n).inv.app X) ≫ (e' a).hom.app ((CategoryTheory.shiftFunctor C n).obj X) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Full<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Faithful<VAR>X : C<GOAL>(F.isoShiftZero M).hom.app (L.obj X) = (e' 0).hom.app X ≫ (G.isoShiftZero M).hom.app X ≫ e.inv.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Full<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Faithful<VAR>n a a' : M<VAR>ha' : n + a = a'<VAR>X : C<GOAL>(F.shiftIso n a a' ha').hom.app (L.obj X) = (F.shift a).map ((L.commShiftIso n).inv.app X) ≫ (e' a).hom.app ((CategoryTheory.shiftFunctor C n).obj X) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>L : C ⥤ D<VAR>F : D ⥤ A<VAR>G : C ⥤ A<VAR>e : L ⋙ F ≅ G<VAR>M : Type u_4<VAR>AddMonoid M<VAR>CategoryTheory.HasShift C M<VAR>CategoryTheory.HasShift D M<VAR>L.CommShift M<VAR>G.ShiftSequence M<VAR>F' : M → D ⥤ A<VAR>e' : (m : M) → L ⋙ F' m ≅ G.shift m<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Full<VAR>((CategoryTheory.whiskeringLeft C D A).obj L).Faithful<VAR>n : M<VAR>X Y : C<VAR>f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y<VAR>a a' : M<VAR>h : n + a = a'<GOAL>F.shiftMap (L.map f ≫ (L.commShiftIso n).hom.app Y) a a' h = (e' a).hom.app X ≫ G.shiftMap f a a' h ≫ (e' a').inv.app Y
<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 T : C<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a : M<VAR>α : CategoryTheory.ShiftedHom X Y a₁<VAR>β : CategoryTheory.ShiftedHom Y Z a₂<VAR>γ : CategoryTheory.ShiftedHom 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>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>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.ShiftedHom.homEquiv m₀ hm₀) f = CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f
<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>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>f : X ⟶ Y<VAR>a : M<VAR>g : CategoryTheory.ShiftedHom Y Z a<GOAL>(CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f).comp g ⋯ = CategoryTheory.CategoryStruct.comp f g
<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>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>a : M<VAR>f : CategoryTheory.ShiftedHom X Y a<GOAL>(CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (CategoryTheory.CategoryStruct.id X)).comp f ⋯ = f
<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>a : M<VAR>f : CategoryTheory.ShiftedHom X Y a<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>g : Y ⟶ Z<GOAL>f.comp (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ g) ⋯ = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C a).map g)
<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<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<GOAL>f.comp (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (CategoryTheory.CategoryStruct.id Y)) ⋯ = f
<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>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>a b c : M<VAR>h : b + a = c<VAR>ha : a = 0<VAR>hb : b = 0<GOAL>(CategoryTheory.ShiftedHom.mk₀ a ha f).comp (CategoryTheory.ShiftedHom.mk₀ b hb g) h = CategoryTheory.ShiftedHom.mk₀ c ⋯ (CategoryTheory.CategoryStruct.comp f g)
<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 T : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>a : M<VAR>ha : a = 0<VAR>d : M<VAR>h : CategoryTheory.ShiftedHom Z T d<GOAL>(CategoryTheory.ShiftedHom.mk₀ a ha f).comp ((CategoryTheory.ShiftedHom.mk₀ a ha g).comp h ⋯) ⋯ = (CategoryTheory.ShiftedHom.mk₀ a ha (CategoryTheory.CategoryStruct.comp f g)).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>CategoryTheory.Preadditive C<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<GOAL>CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ 0 = 0