ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>M N : PresheafOfModules R<VAR>φ : M ⟶ N<GOAL>PresheafOfModules.restrictionApp f M ≫ (ModuleCat.restrictScalars (R.map f)).map (PresheafOfModules.Hom.app φ Y) = ModuleCat.ofHom (PresheafOfModules.Hom.app φ X) ≫ PresheafOfModules.restrictionApp f N
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>PresheafOfModules.restrictionApp (𝟙 X) M = (ModuleCat.restrictScalarsId' (R.map (𝟙 X)) ⋯).inv.app (M.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>PresheafOfModules.restrictionApp (f ≫ g) M = PresheafOfModules.restrictionApp f M ≫ (ModuleCat.restrictScalars (R.map f)).map (PresheafOfModules.restrictionApp g M) ≫ (ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (f ≫ g)) ⋯).inv.app (M.obj Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P Q : PresheafOfModules R<VAR>app : (X : Cᵒᵖ) → ↑(P.obj X) →ₗ[↑(R.obj X)] ↑(Q.obj X)<VAR>naturality : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(P.obj X)), (app Y) ((P.map f) x) = (Q.map f) ((app X) x)<GOAL>PresheafOfModules.Hom.app (PresheafOfModules.Hom.mk' app naturality) = app
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>self : CorePresheafOfModules R<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : self.obj X<GOAL>(self.map (f ≫ g)) x = (self.map g) ((self.map f) x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>self : CorePresheafOfModules R<VAR>X : Cᵒᵖ<VAR>x : self.obj X<GOAL>(self.map (𝟙 X)) x = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : CorePresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>M.presheaf.obj X = AddCommGrp.of (M.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : CorePresheafOfModules R<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), M.presheaf.map f = AddCommGrp.ofHom (M.map f).toAddMonoidHom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : CorePresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>M.toPresheafOfModules.obj X = ModuleCat.of (↑(R.obj X)) (M.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : CorePresheafOfModules R<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>x : M.obj X<GOAL>(M.toPresheafOfModules.presheaf.map f) x = (M.map f) x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>self : BundledCorePresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>self.map (𝟙 X) = (ModuleCat.restrictScalarsId' (R.map (𝟙 X)) ⋯).inv.app (self.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>self : BundledCorePresheafOfModules R<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>self.map (f ≫ g) = self.map f ≫ (ModuleCat.restrictScalars (R.map f)).map (self.map g) ≫ (ModuleCat.restrictScalarsComp' (R.map f) (R.map g) (R.map (f ≫ g)) ⋯).inv.app (self.obj Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : BundledCorePresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>↑(M.toPresheafOfModules.obj X) = ↑(M.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : BundledCorePresheafOfModules R<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ↑(M.obj X)<GOAL>(M.toPresheafOfModules.presheaf.map f) x = (M.map f) x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : BundledCorePresheafOfModules R<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>PresheafOfModules.restrictionApp f M.toPresheafOfModules = M.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>((PresheafOfModules.unit R).map f) 1 = 1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>s : M.sections<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>(M.map f) (↑s X) = ↑s Y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>s : (X : Cᵒᵖ) → ↑(M.obj X)<VAR>hs : ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), (M.map f) (s X) = s Y<VAR>X : Cᵒᵖ<GOAL>↑(PresheafOfModules.sectionsMk s hs) X = s X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>s t : M.sections<VAR>h : ∀ (X : Cᵒᵖ), ↑s X = ↑t X<GOAL>s = t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M N : PresheafOfModules R<VAR>f : M ⟶ N<VAR>s : M.sections<VAR>X : Cᵒᵖ<GOAL>↑(PresheafOfModules.sectionsMap f s) X = (PresheafOfModules.Hom.app f X) (↑s X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M N P : PresheafOfModules R<VAR>f : M ⟶ N<VAR>g : N ⟶ P<VAR>s : M.sections<GOAL>PresheafOfModules.sectionsMap (f ≫ g) s = PresheafOfModules.sectionsMap g (PresheafOfModules.sectionsMap f s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>s : M.sections<GOAL>PresheafOfModules.sectionsMap (𝟙 M) s = s
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M : PresheafOfModules R<VAR>f : PresheafOfModules.unit R ⟶ M<VAR>X : Cᵒᵖ<GOAL>↑(M.unitHomEquiv f) X = (PresheafOfModules.Hom.app f X) 1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : CategoryTheory.Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c₁ c₂ : Cᵒᵖ<VAR>f : c₁ ⟶ c₂<VAR>x : ↑((fun c => (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c)) c₁)<GOAL>((PresheafOfModules.forgetToPresheafModuleCatObj X hX M).map f) x = (M.presheaf.map f) x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : CategoryTheory.Limits.IsInitial X<VAR>M : PresheafOfModules R<VAR>c : Cᵒᵖ<GOAL>(PresheafOfModules.forgetToPresheafModuleCatObj X hX M).obj c = (ModuleCat.restrictScalars (R.map (hX.to c))).obj (M.obj c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : CategoryTheory.Limits.IsInitial X<VAR>M : PresheafOfModules R<GOAL>(PresheafOfModules.forgetToPresheafModuleCat X hX).obj M = PresheafOfModules.forgetToPresheafModuleCatObj X hX M
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X : Cᵒᵖ<VAR>hX : CategoryTheory.Limits.IsInitial X<GOAL>∀ {X_1 Y : PresheafOfModules R} (f : X_1 ⟶ Y), (PresheafOfModules.forgetToPresheafModuleCat X hX).map f = PresheafOfModules.forgetToPresheafModuleCatMap X hX f
<VAR>R : Type u<VAR>CommRing R<VAR>X : AlgebraCat R<GOAL>(CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj X = ModuleCat.of R ↑X
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : AlgebraCat R<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).map f = ModuleCat.ofHom (AlgHom.toLinearMap f)
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type v<VAR>Ring X<VAR>Algebra R X<VAR>Ring Y<VAR>Algebra R Y<VAR>f : X →ₐ[R] Y<VAR>x : X<GOAL>(AlgebraCat.ofHom f) x = f x
<VAR>R : Type u<VAR>CommRing R<VAR>X : Type u<VAR>Ring X<VAR>Algebra R X<GOAL>↑(AlgebraCat.of R X) = X
<VAR>R : Type u<VAR>CommRing R<VAR>M : AlgebraCat R<GOAL>M.ofSelfIso.inv = 𝟙 M
<VAR>R : Type u<VAR>CommRing R<VAR>M : AlgebraCat R<GOAL>M.ofSelfIso.hom = 𝟙 M
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>m : ↑M<GOAL>(𝟙 M) m = m
<VAR>R : Type u<VAR>CommRing R<VAR>M N U : ModuleCat R<VAR>f : M ⟶ N<VAR>g : N ⟶ U<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>R : Type u<VAR>CommRing R<GOAL>∀ {X Y : Type u} (f : X ⟶ Y), (AlgebraCat.free R).map f = (FreeAlgebra.lift R) (FreeAlgebra.ι R ∘ f)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u<GOAL>↑((AlgebraCat.free R).obj S) = FreeAlgebra R S
<VAR>R : Type u<VAR>CommRing R<VAR>X₁ X₂ : Type u<VAR>g₁ : Ring X₁<VAR>g₂ : Ring X₂<VAR>m₁ : Algebra R X₁<VAR>m₂ : Algebra R X₂<VAR>e : X₁ ≃ₐ[R] X₂<GOAL>e.toAlgebraIso.hom = ↑e
<VAR>R : Type u<VAR>CommRing R<VAR>X₁ X₂ : Type u<VAR>g₁ : Ring X₁<VAR>g₂ : Ring X₂<VAR>m₁ : Algebra R X₁<VAR>m₂ : Algebra R X₂<VAR>e : X₁ ≃ₐ[R] X₂<GOAL>e.toAlgebraIso.inv = ↑e.symm
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : AlgebraCat R<VAR>i : X ≅ Y<VAR>a : ↑X<GOAL>i.toAlgEquiv a = i.hom a
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : AlgebraCat R<VAR>i : X ≅ Y<VAR>a : ↑Y<GOAL>i.toAlgEquiv.symm a = i.inv a
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type u<VAR>Ring X<VAR>Ring Y<VAR>Algebra R X<VAR>Algebra R Y<VAR>i : AlgebraCat.of R X ≅ AlgebraCat.of R Y<GOAL>algEquivIsoAlgebraIso.inv i = i.toAlgEquiv
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : Type u<VAR>Ring X<VAR>Ring Y<VAR>Algebra R X<VAR>Algebra R Y<VAR>e : X ≃ₐ[R] Y<GOAL>algEquivIsoAlgebraIso.hom e = e.toAlgebraIso
<VAR>R : Type u_1<VAR>CommRing R<VAR>G : AlgebraCat R<VAR>H : Type u<VAR>Ring H<VAR>Algebra R H<VAR>f : ↑G →ₐ[R] H<GOAL>f.comp (𝟙 G) = f
<VAR>R : Type u_1<VAR>CommRing R<VAR>G : Type u<VAR>Ring G<VAR>Algebra R G<VAR>H : AlgebraCat R<VAR>f : G →ₐ[R] ↑H<GOAL>AlgHom.comp (𝟙 H) f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : HomotopyCategory C (ComplexShape.up ℤ)<GOAL>(HomotopyCategory.subcategoryAcyclic C).P X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>K : CochainComplex C ℤ<GOAL>(HomotopyCategory.subcategoryAcyclic C).P ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<GOAL>HomotopyCategory.quasiIso C (ComplexShape.up ℤ) = (HomotopyCategory.subcategoryAcyclic C).W
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<GOAL>T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ X Y f, Nonempty (T ≅ DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>(DerivedCategory.triangleOfSES hS).obj₃ = DerivedCategory.Q.obj S.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>(DerivedCategory.triangleOfSES hS).mor₃ = DerivedCategory.triangleOfSESδ hS
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>(DerivedCategory.triangleOfSES hS).mor₂ = DerivedCategory.Q.map S.g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>(DerivedCategory.triangleOfSES hS).obj₁ = DerivedCategory.Q.obj S.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>(DerivedCategory.triangleOfSES hS).mor₁ = DerivedCategory.Q.map S.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>(DerivedCategory.triangleOfSES hS).obj₂ = DerivedCategory.Q.obj S.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex (CochainComplex C ℤ)<VAR>hS : S.ShortExact<GOAL>DerivedCategory.triangleOfSES hS ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C₁ : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Abelian C₁<VAR>HasDerivedCategory C₁<VAR>C₂ : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Abelian C₂<VAR>HasDerivedCategory C₂<VAR>F : C₁ ⥤ C₂<VAR>F.Additive<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<VAR>CategoryTheory.Limits.PreservesFiniteColimits F<VAR>K : CochainComplex C₁ ℤ<GOAL>F.mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K) = F.mapDerivedCategory.map ((DerivedCategory.quotientCompQhIso C₁).hom.app K) ≫ F.mapDerivedCategoryFactors.hom.app K ≫ (DerivedCategory.quotientCompQhIso C₂).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) ≫ DerivedCategory.Qh.map ((F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).inv.app K)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(DerivedCategory.homologyFunctor C n₀).map T.mor₂ ≫ DerivedCategory.HomologySequence.δ T n₀ n₁ h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>DerivedCategory.HomologySequence.δ T n₀ n₁ h ≫ (DerivedCategory.homologyFunctor C n₁).map T.mor₁ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ : ℤ<GOAL>(CategoryTheory.ShortComplex.mk ((DerivedCategory.homologyFunctor C n₀).map T.mor₁) ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(CategoryTheory.ShortComplex.mk ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) (DerivedCategory.HomologySequence.δ T n₀ n₁ h) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(CategoryTheory.ShortComplex.mk (DerivedCategory.HomologySequence.δ T n₀ n₁ h) ((DerivedCategory.homologyFunctor C n₁).map T.mor₁) ⋯).Exact
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ : ℤ<GOAL>CategoryTheory.Epi ((DerivedCategory.homologyFunctor C n₀).map T.mor₁) ↔ (DerivedCategory.homologyFunctor C n₀).map T.mor₂ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>CategoryTheory.Mono ((DerivedCategory.homologyFunctor C n₁).map T.mor₁) ↔ DerivedCategory.HomologySequence.δ T n₀ n₁ h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>CategoryTheory.Epi ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ↔ DerivedCategory.HomologySequence.δ T n₀ n₁ h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)<VAR>hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles<VAR>n₀ : ℤ<GOAL>CategoryTheory.Mono ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ↔ (DerivedCategory.homologyFunctor C n₀).map T.mor₁ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangle.obj₃ = (DerivedCategory.singleFunctor C 0).obj S.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangle.mor₁ = (DerivedCategory.singleFunctor C 0).map S.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangle.obj₂ = (DerivedCategory.singleFunctor C 0).obj S.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangle.mor₂ = (DerivedCategory.singleFunctor C 0).map S.g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangle.mor₃ = hS.singleδ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangle.obj₁ = (DerivedCategory.singleFunctor C 0).obj S.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangleIso.hom.hom₁ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangleIso.hom.hom₃ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangleIso.inv.hom₃ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangleIso.hom.hom₂ = ((DerivedCategory.singleFunctorsPostcompQIso C).hom.hom 0).app S.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangleIso.inv.hom₂ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangleIso.inv.hom₁ = ((DerivedCategory.singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>HasDerivedCategory C<VAR>S : CategoryTheory.ShortComplex C<VAR>hS : S.ShortExact<GOAL>hS.singleTriangle ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ AddGrp<GOAL>CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ CategoryTheory.forget AddGrp).sections
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Grp<GOAL>CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ CategoryTheory.forget Grp).sections
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ CommGrp<GOAL>CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ CategoryTheory.forget CommGrp).sections
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ AddCommGrp<GOAL>CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ CategoryTheory.forget AddCommGrp).sections
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<GOAL>(AddCommGrp.kernelIsoKer f).hom ≫ (AddMonoidHom.ker f).subtype = CategoryTheory.Limits.kernel.ι f
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<GOAL>(AddCommGrp.kernelIsoKer f).inv ≫ CategoryTheory.Limits.kernel.ι f = (AddMonoidHom.ker f).subtype
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<GOAL>∀ (a : ↑(CategoryTheory.Limits.KernelFork.ofι (AddMonoidHom.ker f).subtype ⋯).pt), (AddCommGrp.kernelIsoKerOver f).inv.left a = (CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair f 0) (CategoryTheory.Limits.KernelFork.ofι (AddMonoidHom.ker f).subtype ⋯)) a
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<VAR>g : ↑(CategoryTheory.Limits.kernel f)<GOAL>↑((AddCommGrp.kernelIsoKerOver f).hom.left g) = (CategoryTheory.Limits.kernel.ι f) g
<VAR>ι : Type u_1<VAR>self : ComplexShape ι<VAR>i j j' : ι<GOAL>self.Rel i j → self.Rel i j' → j = j'
<VAR>ι : Type u_1<VAR>self : ComplexShape ι<VAR>i i' j : ι<GOAL>self.Rel i j → self.Rel i' j → i = i'
<VAR>ι : Type u_2<VAR>i j : ι<GOAL>(ComplexShape.refl ι).Rel i j = (i = j)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>i j : ι<GOAL>c.symm.Rel i j = c.Rel j i
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<GOAL>c.symm.symm = c
<VAR>ι : Type u_1<GOAL>Function.Bijective ComplexShape.symm
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>j : ι<VAR>hj : ∀ (k : ι), ¬c.Rel j k<GOAL>c.next j = j
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>j : ι<VAR>hj : ∀ (i : ι), ¬c.Rel i j<GOAL>c.prev j = j
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>j : ι<VAR>hj : ¬c.Rel j (c.next j)<GOAL>c.next j = j
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>j : ι<VAR>hj : ¬c.Rel (c.prev j) j<GOAL>c.prev j = j
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>a i j : α<GOAL>(ComplexShape.up' a).Rel i j = (i + a = j)
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>a i j : α<GOAL>(ComplexShape.down' a).Rel i j = (j + a = i)
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>a i j : α<VAR>h : j + a = i<GOAL>(ComplexShape.down' a).Rel i j
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>i j : α<GOAL>(ComplexShape.up α).Rel i j = (i + 1 = j)
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>i j : α<GOAL>(ComplexShape.down α).Rel i j = (j + 1 = i)
<VAR>α : Type u_2<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>i j : α<VAR>h : j + 1 = i<GOAL>(ComplexShape.down α).Rel i j
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>Module R A<VAR>S : Type w''<VAR>SetLike S A<VAR>NonUnitalSubsemiringClass S A<VAR>hSR : SMulMemClass S R A<VAR>StarMemClass S A<VAR>s : S<GOAL>⇑(NonUnitalStarSubalgebraClass.subtype s) = Subtype.val
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>self : NonUnitalStarSubalgebra R A<VAR>a : A<VAR>_ha : a ∈ self.carrier<GOAL>star a ∈ self.carrier
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>s : NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>h : ∀ (x : A), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<VAR>x : A<GOAL>x ∈ S.toNonUnitalSubalgebra ↔ x ∈ S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>↑S.toNonUnitalSubalgebra = ↑S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<GOAL>Function.Injective NonUnitalStarSubalgebra.toNonUnitalSubalgebra
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>NonUnitalNonAssocSemiring A<VAR>Module R A<VAR>Star A<VAR>S U : NonUnitalStarSubalgebra R A<GOAL>S.toNonUnitalSubalgebra = U.toNonUnitalSubalgebra ↔ S = U