ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<GOAL>CategoryTheory.NatTrans.app 0 X = 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 D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α β : F ⟶ G<GOAL>(α + β).app X = α.app X + β.app X
<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 D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α β : F ⟶ G<GOAL>(α - β).app X = α.app X - β.app X
<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 D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α : F ⟶ G<GOAL>(-α).app X = -α.app X
<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 D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α : F ⟶ G<VAR>n : ℕ<GOAL>(n • α).app X = n • α.app X
<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 D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α : F ⟶ G<VAR>n : ℤ<GOAL>(n • α).app X = n • α.app X
<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 D<VAR>F G : CategoryTheory.Functor C D<VAR>X : C<VAR>α : F ⟶ G<VAR>n : ℤˣ<GOAL>(n • α).app X = n • α.app X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>F G : CategoryTheory.Functor C D<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>X : C<VAR>α : ι → (F ⟶ G)<GOAL>(∑ i ∈ s, α i).app X = ∑ i ∈ s, (α i).app X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>self : CategoryTheory.Simple X<VAR>Y : C<VAR>f : Y ⟶ X<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsIso f ↔ f ≠ 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Simple Y<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>w : f ≠ 0<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Simple Y<VAR>i : X ≅ Y<GOAL>CategoryTheory.Simple X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>i : X ≅ Y<GOAL>CategoryTheory.Simple X ↔ CategoryTheory.Simple Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Simple X<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>w : f ≠ 0<GOAL>CategoryTheory.Limits.kernel.ι f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>X Y : C<VAR>CategoryTheory.Simple Y<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>w : f ≠ 0<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Simple Y<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>w : CategoryTheory.IsIso f → False<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>CategoryTheory.Simple X<GOAL>CategoryTheory.CategoryStruct.id X ≠ 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X : C<VAR>CategoryTheory.Simple X<GOAL>¬CategoryTheory.Limits.IsZero X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Simple 0<GOAL>False
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : C<VAR>h : ∀ {Z : C} (f : X ⟶ Z) [inst : CategoryTheory.Epi f], CategoryTheory.IsIso f ↔ f ≠ 0<GOAL>CategoryTheory.Simple X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>CategoryTheory.Simple X<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>w : f ≠ 0<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>CategoryTheory.Simple Y<VAR>f : X ⟶ Y<VAR>w : f ≠ 0<GOAL>CategoryTheory.Limits.cokernel.π f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X Y : C<VAR>CategoryTheory.Simple X<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>w : CategoryTheory.IsIso f → False<GOAL>f = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : C<GOAL>CategoryTheory.IsIso CategoryTheory.Limits.biprod.inl ↔ CategoryTheory.Limits.IsZero Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X : C<VAR>CategoryTheory.Simple X<GOAL>CategoryTheory.Indecomposable X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : C<VAR>IsSimpleOrder (CategoryTheory.Subobject X)<GOAL>CategoryTheory.Simple X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : C<GOAL>CategoryTheory.Simple X ↔ IsSimpleOrder (CategoryTheory.Subobject X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : C<VAR>Y : CategoryTheory.Subobject X<GOAL>CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y) ↔ IsAtom Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>CategoryTheory.Simple X<VAR>f : X ⟶ Y<VAR>w : f ≠ 0<GOAL>CategoryTheory.Mono f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>CategoryTheory.Simple X<VAR>CategoryTheory.Simple Y<VAR>f : X ⟶ Y<VAR>w : f ≠ 0<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>CategoryTheory.Simple X<VAR>CategoryTheory.Simple Y<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f ↔ f ≠ 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>DivisionRing 𝕜<VAR>CategoryTheory.Limits.HasKernels C<VAR>CategoryTheory.Linear 𝕜 C<VAR>X Y : C<VAR>CategoryTheory.Simple X<VAR>CategoryTheory.Simple Y<VAR>h : (X ≅ Y) → False<GOAL>FiniteDimensional.finrank 𝕜 (X ⟶ Y) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>IsAlgClosed 𝕜<VAR>CategoryTheory.Linear 𝕜 C<VAR>X : C<VAR>isIso_iff_nonzero : ∀ (f : X ⟶ X), CategoryTheory.IsIso f ↔ f ≠ 0<VAR>I : FiniteDimensional 𝕜 (X ⟶ X)<GOAL>FiniteDimensional.finrank 𝕜 (X ⟶ X) = 1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>IsAlgClosed 𝕜<VAR>CategoryTheory.Linear 𝕜 C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X : C<VAR>CategoryTheory.Simple X<VAR>FiniteDimensional 𝕜 (X ⟶ X)<GOAL>FiniteDimensional.finrank 𝕜 (X ⟶ X) = 1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>IsAlgClosed 𝕜<VAR>CategoryTheory.Linear 𝕜 C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X : C<VAR>CategoryTheory.Simple X<VAR>FiniteDimensional 𝕜 (X ⟶ X)<VAR>f : X ⟶ X<GOAL>∃ c, c • CategoryTheory.CategoryStruct.id X = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>IsAlgClosed 𝕜<VAR>CategoryTheory.Linear 𝕜 C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>FiniteDimensional 𝕜 (X ⟶ X)<VAR>CategoryTheory.Simple X<VAR>CategoryTheory.Simple Y<GOAL>FiniteDimensional.finrank 𝕜 (X ⟶ Y) ≤ 1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>IsAlgClosed 𝕜<VAR>CategoryTheory.Linear 𝕜 C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>FiniteDimensional 𝕜 (X ⟶ X)<VAR>FiniteDimensional 𝕜 (X ⟶ Y)<VAR>CategoryTheory.Simple X<VAR>CategoryTheory.Simple Y<GOAL>FiniteDimensional.finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>IsAlgClosed 𝕜<VAR>CategoryTheory.Linear 𝕜 C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>FiniteDimensional 𝕜 (X ⟶ X)<VAR>FiniteDimensional 𝕜 (X ⟶ Y)<VAR>CategoryTheory.Simple X<VAR>CategoryTheory.Simple Y<GOAL>FiniteDimensional.finrank 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty (X ≅ Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>𝕜 : Type u_2<VAR>Field 𝕜<VAR>IsAlgClosed 𝕜<VAR>CategoryTheory.Linear 𝕜 C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X Y : C<VAR>∀ (X Y : C), FiniteDimensional 𝕜 (X ⟶ Y)<VAR>CategoryTheory.Simple X<VAR>CategoryTheory.Simple Y<GOAL>FiniteDimensional.finrank 𝕜 (X ⟶ Y) = if Nonempty (X ≅ Y) then 1 else 0
<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 : C ⥤ D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>X Y : Cᵒᵖ<VAR>w : X ⟶ Y<VAR>hw : W.op w<GOAL>(CategoryTheory.Localization.isoOfHom L.op W.op w hw).unop = CategoryTheory.Localization.isoOfHom L W w.unop hw
<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 : C ⥤ D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L.IsLocalization W<VAR>X Y : Cᵒᵖ<VAR>w : X ⟶ Y<VAR>hw : W.op w<GOAL>(CategoryTheory.Localization.isoOfHom L.op W.op w hw).inv = (CategoryTheory.Localization.isoOfHom L W w.unop hw).inv.op
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>L₂ : CategoryTheory.Functor C₂ C₃<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>L₁.IsLocalization W₁<VAR>L₂.IsLocalization W₂<VAR>W₃ : CategoryTheory.MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁.comp L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<GOAL>(L₁.comp L₂).IsLocalization W₃
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>L₁ : CategoryTheory.Functor C₁ C₂<VAR>L₂ : CategoryTheory.Functor C₂ C₃<VAR>W₁ : CategoryTheory.MorphismProperty C₁<VAR>W₂ : CategoryTheory.MorphismProperty C₂<VAR>W₃ : CategoryTheory.MorphismProperty C₁<VAR>L₁.IsLocalization W₁<VAR>(L₁.comp L₂).IsLocalization W₃<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ = W₃.map L₁<GOAL>L₂.IsLocalization W₂
<VAR>V : Type u₁<VAR>Quiver V<GOAL>∀ {X Y : V} (f : X ⟶ Y), CategoryTheory.Paths.of.map f = f.toPath
<VAR>V : Type u₁<VAR>Quiver V<VAR>X : V<GOAL>CategoryTheory.Paths.of.obj X = X
<VAR>V : Type u₁<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>φ : V ⥤q C<VAR>X : V<GOAL>(CategoryTheory.Paths.lift φ).map Quiver.Path.nil = CategoryTheory.CategoryStruct.id (φ.obj X)
<VAR>V : Type u₁<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>φ : V ⥤q C<VAR>X Y Z : V<VAR>p : Quiver.Path X Y<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.Paths.lift φ).map (p.cons f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.lift φ).map p) (φ.map f)
<VAR>V : Type u₁<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>φ : V ⥤q C<VAR>X Y : V<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Paths.lift φ).map f.toPath = φ.map f
<VAR>V : Type u₁<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>φ : V ⥤q C<GOAL>CategoryTheory.Paths.of ⋙q (CategoryTheory.Paths.lift φ).toPrefunctor = φ
<VAR>V : Type u₁<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>φ : V ⥤q C<VAR>Φ : CategoryTheory.Functor (CategoryTheory.Paths V) C<VAR>hΦ : CategoryTheory.Paths.of ⋙q Φ.toPrefunctor = φ<GOAL>Φ = CategoryTheory.Paths.lift φ
<VAR>V : Type u₁<VAR>Quiver V<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>F G : CategoryTheory.Functor (CategoryTheory.Paths V) C<VAR>h_obj : F.obj = G.obj<VAR>h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map e.toPath) (CategoryTheory.eqToHom ⋯))<GOAL>F = G
<VAR>V : Type u₁<VAR>Quiver V<VAR>W : Type u₂<VAR>Quiver W<VAR>F : V ⥤q W<VAR>X Y Z : CategoryTheory.Paths V<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>F.mapPath (CategoryTheory.CategoryStruct.comp f g) = (F.mapPath f).comp (F.mapPath g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>CategoryTheory.composePath Quiver.Path.nil = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>p : Quiver.Path X Y<VAR>e : Y ⟶ Z<GOAL>CategoryTheory.composePath (p.cons e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.composePath f.toPath = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : Quiver.Path X Y<VAR>g : Quiver.Path Y Z<GOAL>CategoryTheory.composePath (f.comp g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath f) (CategoryTheory.composePath g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : CategoryTheory.Paths C<GOAL>CategoryTheory.composePath (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (id X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : CategoryTheory.Paths C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.composePath (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath f) (CategoryTheory.composePath g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : CategoryTheory.Paths C} (f : X ⟶ Y), (CategoryTheory.pathComposition C).map f = CategoryTheory.composePath f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : CategoryTheory.Paths C<GOAL>(CategoryTheory.pathComposition C).obj X = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>((CategoryTheory.toQuotientPaths C).obj X).as = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.toQuotientPaths C).map f = Quot.mk (CategoryTheory.Quotient.CompClosure (CategoryTheory.pathsHomRel C)) f.toPath
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>a b : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)<VAR>hf : a ⟶ b<GOAL>(CategoryTheory.quotientPathsTo C).map hf = Quot.liftOn hf (fun f => CategoryTheory.composePath f) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>a : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)<GOAL>(CategoryTheory.quotientPathsTo C).obj a = a.as
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>self : CategoryTheory.DifferentialObject S C<GOAL>CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y : CategoryTheory.DifferentialObject S C<VAR>self : X.Hom Y<GOAL>CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) = CategoryTheory.CategoryStruct.comp self.f Y.d
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>(CategoryTheory.DifferentialObject.Hom.id X).f = CategoryTheory.CategoryStruct.id X.obj
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y Z : CategoryTheory.DifferentialObject S C<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>(f.comp g).f = CategoryTheory.CategoryStruct.comp f.f g.f
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>A B : CategoryTheory.DifferentialObject S C<VAR>f g : A ⟶ B<VAR>w : f.f = g.f := by aesop_cat<GOAL>f = g
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>(CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.obj
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y Z : CategoryTheory.DifferentialObject S C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y : CategoryTheory.DifferentialObject S C<VAR>h : X = Y<GOAL>(CategoryTheory.eqToHom h).f = CategoryTheory.eqToHom ⋯
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms<VAR>P Q : CategoryTheory.DifferentialObject S C<GOAL>CategoryTheory.DifferentialObject.Hom.f 0 = 0
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y : CategoryTheory.DifferentialObject S C<VAR>f : X ≅ Y<GOAL>(CategoryTheory.DifferentialObject.isoApp f).inv = f.inv.f
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y : CategoryTheory.DifferentialObject S C<VAR>f : X ≅ Y<GOAL>(CategoryTheory.DifferentialObject.isoApp f).hom = f.hom.f
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>CategoryTheory.DifferentialObject.isoApp (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl X.obj
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y : CategoryTheory.DifferentialObject S C<VAR>f : X ≅ Y<GOAL>CategoryTheory.DifferentialObject.isoApp f.symm = (CategoryTheory.DifferentialObject.isoApp f).symm
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y Z : CategoryTheory.DifferentialObject S C<VAR>f : X ≅ Y<VAR>g : Y ≅ Z<GOAL>CategoryTheory.DifferentialObject.isoApp (f ≪≫ g) = CategoryTheory.DifferentialObject.isoApp f ≪≫ CategoryTheory.DifferentialObject.isoApp g
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y : CategoryTheory.DifferentialObject S C<VAR>f : X.obj ≅ Y.obj<VAR>hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d<GOAL>(CategoryTheory.DifferentialObject.mkIso f hf).inv.f = f.inv
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>X Y : CategoryTheory.DifferentialObject S C<VAR>f : X.obj ≅ Y.obj<VAR>hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d<GOAL>(CategoryTheory.DifferentialObject.mkIso f hf).hom.f = f.hom
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>CategoryTheory.HasShift D S<VAR>F : CategoryTheory.Functor C D<VAR>η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).obj = F.obj X.obj
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>CategoryTheory.HasShift D S<VAR>F : CategoryTheory.Functor C D<VAR>η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)<VAR>hF : ∀ (c c' : C), F.map 0 = 0<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).d = CategoryTheory.CategoryStruct.comp (F.map X.d) (η.app X.obj)
<VAR>S : Type u_1<VAR>AddMonoidWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>CategoryTheory.HasShift D S<VAR>F : CategoryTheory.Functor C D<VAR>η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)<VAR>hF : ∀ (c c' : C), F.map 0 = 0<GOAL>∀ {X Y : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y), ((CategoryTheory.Functor.mapDifferentialObject D F η hF).map f).f = F.map f.f
<VAR>S : Type u_1<VAR>AddCommGroupWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>n : S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).d = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (CategoryTheory.shiftComm X.obj 1 n).hom
<VAR>S : Type u_1<VAR>AddCommGroupWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>n : S<VAR>X : CategoryTheory.DifferentialObject S C<GOAL>((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj
<VAR>S : Type u_1<VAR>AddCommGroupWithOne S<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.HasShift C S<VAR>n : S<GOAL>∀ {X Y : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y), ((CategoryTheory.DifferentialObject.shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f