ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Z : ι → ModuleCatMax R<VAR>CategoryTheory.Limits.HasProduct Z<VAR>i : ι<GOAL>(ModuleCat.piIsoPi Z).inv ≫ CategoryTheory.Limits.Pi.π Z i = LinearMap.proj i
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>Z : ι → ModuleCatMax R<VAR>CategoryTheory.Limits.HasProduct Z<VAR>i : ι<GOAL>(ModuleCat.piIsoPi Z).hom ≫ LinearMap.proj i = CategoryTheory.Limits.Pi.π Z i
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair M N)<GOAL>(M.binaryProductLimitCone N).isLimit.lift s = LinearMap.prod (s.π.app { as := CategoryTheory.Limits.WalkingPair.left }) (s.π.app { as := CategoryTheory.Limits.WalkingPair.right })
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<GOAL>(M.binaryProductLimitCone N).cone.pt = ModuleCat.of R (↑M × ↑N)
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<GOAL>(M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = LinearMap.fst R ↑M ↑N
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<GOAL>(M.binaryProductLimitCone N).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = LinearMap.snd R ↑M ↑N
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>i : ↑(CategoryTheory.Limits.BinaryBiproduct.bicone M N).toCone.pt<GOAL>(M.biprodIsoProd N).hom i = (CategoryTheory.Limits.biprod.fst i, CategoryTheory.Limits.biprod.snd i)
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<GOAL>(M.biprodIsoProd N).inv ≫ CategoryTheory.Limits.biprod.fst = LinearMap.fst R ↑M ↑N
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<GOAL>(M.biprodIsoProd N).inv ≫ CategoryTheory.Limits.biprod.snd = LinearMap.snd R ↑M ↑N
<VAR>R : Type u<VAR>Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : CategoryTheory.Limits.Fan f<VAR>x : ↑s.pt<VAR>j : J<GOAL>(ModuleCat.HasLimit.lift f s) x j = (s.π.app { as := j }) x
<VAR>R : Type u<VAR>Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<GOAL>(ModuleCat.HasLimit.productLimitCone f).cone.pt = ModuleCat.of R ((j : J) → ↑(f j))
<VAR>R : Type u<VAR>Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<GOAL>(ModuleCat.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun j => LinearMap.proj j.as
<VAR>R : Type u<VAR>Ring R<VAR>J : Type w<VAR>f : J → ModuleCat R<VAR>s : CategoryTheory.Limits.Fan f<GOAL>(ModuleCat.HasLimit.productLimitCone f).isLimit.lift s = ModuleCat.HasLimit.lift f s
<VAR>R : Type u<VAR>Ring R<VAR>J : Type<VAR>Finite J<VAR>f : J → ModuleCat R<VAR>x : ↑(CategoryTheory.Limits.biproduct.bicone f).toCone.pt<VAR>j : J<GOAL>(ModuleCat.biproductIsoPi f).hom x j = (CategoryTheory.Limits.biproduct.π f j) x
<VAR>R : Type u<VAR>Ring R<VAR>J : Type<VAR>Finite J<VAR>f : J → ModuleCat R<VAR>j : J<GOAL>(ModuleCat.biproductIsoPi f).inv ≫ CategoryTheory.Limits.biproduct.π f j = LinearMap.proj j
<VAR>R : Type u<VAR>Ring R<GOAL>CategoryTheory.EnoughInjectives (ModuleCat R)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ AddMonCatMax<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : ∃ k f g, (F.map f) x.snd = (F.map g) y.snd<GOAL>AddMonCat.FilteredColimits.M.mk F x = AddMonCat.FilteredColimits.M.mk F y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : ∃ k f g, (F.map f) x.snd = (F.map g) y.snd<GOAL>MonCat.FilteredColimits.M.mk F x = MonCat.FilteredColimits.M.mk F y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>j : J<GOAL>1 = MonCat.FilteredColimits.M.mk F ⟨j, 1⟩
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ AddMonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>j : J<GOAL>0 = AddMonCat.FilteredColimits.M.mk F ⟨j, 0⟩
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>x x' y : (j : J) × ↑(F.obj j)<VAR>hxx' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F ⋙ CategoryTheory.forget MonCat) x x'<GOAL>MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x' y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ AddMonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>x x' y : (j : J) × ↑(F.obj j)<VAR>hxx' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F ⋙ CategoryTheory.forget AddMonCat) x x'<GOAL>AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x' y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>x y y' : (j : J) × ↑(F.obj j)<VAR>hyy' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F ⋙ CategoryTheory.forget MonCat) y y'<GOAL>MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x y'
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ AddMonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>x y y' : (j : J) × ↑(F.obj j)<VAR>hyy' : CategoryTheory.Limits.Types.FilteredColimit.Rel (F ⋙ CategoryTheory.forget AddMonCat) y y'<GOAL>AddMonCat.FilteredColimits.colimitAddAux F x y = AddMonCat.FilteredColimits.colimitAddAux F x y'
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ AddMonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<GOAL>AddMonCat.FilteredColimits.M.mk F x + AddMonCat.FilteredColimits.M.mk F y = AddMonCat.FilteredColimits.M.mk F ⟨k, (F.map f) x.snd + (F.map g) y.snd⟩
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>x y : (j : J) × ↑(F.obj j)<VAR>k : J<VAR>f : x.fst ⟶ k<VAR>g : y.fst ⟶ k<GOAL>MonCat.FilteredColimits.M.mk F x * MonCat.FilteredColimits.M.mk F y = MonCat.FilteredColimits.M.mk F ⟨k, (F.map f) x.snd * (F.map g) y.snd⟩
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ AddMonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ AddMonCat.FilteredColimits.coconeMorphism F j' = AddMonCat.FilteredColimits.coconeMorphism F j
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>CategoryTheory.IsFiltered J<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>F.map f ≫ MonCat.FilteredColimits.coconeMorphism F j' = MonCat.FilteredColimits.coconeMorphism F j
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↥(LinearMap.ker f)<GOAL>(CategoryTheory.Limits.kernelSubobject f).arrow (ModuleCat.toKernelSubobject x) = ↑x
<VAR>R : Type u<VAR>Ring R<VAR>L M N : ModuleCat R<VAR>f : L ⟶ M<VAR>CategoryTheory.Limits.HasImage f<VAR>g : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ N<VAR>CategoryTheory.Limits.HasCokernel g<VAR>x y : ↑N<VAR>l : ↑L<VAR>w : x = y + g ((CategoryTheory.Limits.factorThruImageSubobject f) l)<GOAL>(CategoryTheory.Limits.cokernel.π g) x = (CategoryTheory.Limits.cokernel.π g) y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>self : SheafOfModules R<GOAL>CategoryTheory.Presheaf.IsSheaf J self.val.presheaf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>X Y : SheafOfModules R<VAR>f g : X ⟶ Y<VAR>h : f.val = g.val<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>X : SheafOfModules R<GOAL>(𝟙 X).val = 𝟙 X.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>X Y Z : SheafOfModules R<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).val = f.val ≫ g.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<GOAL>∀ {X Y : SheafOfModules R} (φ : X ⟶ Y), (SheafOfModules.forget R).map φ = φ.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>F : SheafOfModules R<GOAL>(SheafOfModules.forget R).obj F = F.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<GOAL>∀ {X Y : SheafOfModules R} (φ : (SheafOfModules.forget R).obj X ⟶ (SheafOfModules.forget R).obj Y), ((SheafOfModules.fullyFaithfulForget R).preimage φ).val = φ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<GOAL>∀ {X Y : SheafOfModules R} (f : X ⟶ Y), ((SheafOfModules.toSheaf R).map f).val = f.val.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<GOAL>((SheafOfModules.toSheaf R).obj M).val = M.val.presheaf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>X : Cᵒᵖ<VAR>hX : CategoryTheory.Limits.IsInitial X<GOAL>∀ {X_1 Y : SheafOfModules R} (f : X_1 ⟶ Y), ((SheafOfModules.forgetToSheafModuleCat R X hX).map f).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>X : Cᵒᵖ<VAR>hX : CategoryTheory.Limits.IsInitial X<VAR>M : SheafOfModules R<GOAL>((SheafOfModules.forgetToSheafModuleCat R X hX).obj M).val = (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M N : SheafOfModules R<VAR>f g : M ⟶ N<GOAL>(f + g).val = f.val + g.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M N P : SheafOfModules R<VAR>f : M ⟶ N<VAR>g : N ⟶ P<VAR>s : M.sections<GOAL>SheafOfModules.sectionsMap (f ≫ g) s = SheafOfModules.sectionsMap g (SheafOfModules.sectionsMap f s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<VAR>s : M.sections<GOAL>SheafOfModules.sectionsMap (𝟙 M) s = s
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<GOAL>∀ {X Y : SheafOfModules R} (f : X ⟶ Y) (s : X.sections), (SheafOfModules.sectionsFunctor R).map f s = SheafOfModules.sectionsMap f s
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>M : SheafOfModules R<GOAL>(SheafOfModules.sectionsFunctor R).obj M = M.sections
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<GOAL>(SheafOfModules.unit R).val = PresheafOfModules.unit R.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M : SheafOfModules R<VAR>f : SheafOfModules.unit R ⟶ M<VAR>X : Cᵒᵖ<GOAL>↑(M.unitHomEquiv f) X = (PresheafOfModules.Hom.app f.val X) 1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>f : SheafOfModules.unit R ⟶ M<VAR>p : M ⟶ N<GOAL>N.unitHomEquiv (f ≫ p) = SheafOfModules.sectionsMap p (M.unitHomEquiv f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : CategoryTheory.Sheaf J RingCat<VAR>J.HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>s : M.sections<VAR>p : M ⟶ N<GOAL>M.unitHomEquiv.symm s ≫ p = N.unitHomEquiv.symm (SheafOfModules.sectionsMap p s)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f.hom<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f.hom<VAR>φ : M₂ ⟶ N<GOAL>(PresheafOfModules.homEquivOfIsLocallyBijective f hN) φ = f ≫ φ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>M₁ M₂ : PresheafOfModules R<VAR>f : M₁ ⟶ M₂<VAR>N : PresheafOfModules R<VAR>hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf<VAR>J.WEqualsLocallyBijective AddCommGrp<VAR>CategoryTheory.Presheaf.IsLocallySurjective J f.hom<VAR>CategoryTheory.Presheaf.IsLocallyInjective J f.hom<VAR>ψ : M₁ ⟶ N<GOAL>((PresheafOfModules.homEquivOfIsLocallyBijective f hN).symm ψ).hom = (CategoryTheory.Localization.LeftBousfield.W.homEquiv ⋯ N.presheaf hN).symm ψ.hom
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>M' : PresheafOfModules R'<VAR>α : R ⟶ R'<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>a : ↑(M'.obj X)<GOAL>((M'.restrictScalarsBundledCore α).map f) a = (M'.map f) a
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>M' : PresheafOfModules R'<VAR>α : R ⟶ R'<VAR>X : Cᵒᵖ<GOAL>(M'.restrictScalarsBundledCore α).obj X = (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>α : R ⟶ R'<VAR>M' : PresheafOfModules R'<GOAL>(PresheafOfModules.restrictScalars α).obj M' = (M'.restrictScalarsBundledCore α).toPresheafOfModules
<VAR>C : Type u'<VAR>CategoryTheory.Category.{v', u'} C<VAR>R R' : Cᵒᵖ ⥤ RingCat<VAR>α : R ⟶ R'<VAR>M₁' M₂' : PresheafOfModules R'<VAR>φ : M₁' ⟶ M₂'<GOAL>((PresheafOfModules.restrictScalars α).map φ).hom = φ.hom
<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 : Dᵒᵖ ⥤ RingCat<VAR>S : Cᵒᵖ ⥤ RingCat<VAR>φ : S ⟶ F.op ⋙ R<VAR>M : PresheafOfModules R<VAR>X : Cᵒᵖ<GOAL>((PresheafOfModules.pushforward φ).obj M).obj X = (ModuleCat.restrictScalars (φ.app X)).obj (M.obj (Opposite.op (F.obj (Opposite.unop 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 : Dᵒᵖ ⥤ RingCat<VAR>S : Cᵒᵖ ⥤ RingCat<VAR>φ : S ⟶ F.op ⋙ R<VAR>M : PresheafOfModules R<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>m : ↑((ModuleCat.restrictScalars (φ.app X)).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))<GOAL>(((PresheafOfModules.pushforward φ).obj M).map f) m = (M.map (F.map f.unop).op) m
<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 : Dᵒᵖ ⥤ RingCat<VAR>S : Cᵒᵖ ⥤ RingCat<VAR>φ : S ⟶ F.op ⋙ R<VAR>M N : PresheafOfModules R<VAR>α : M ⟶ N<VAR>X : Cᵒᵖ<VAR>m : ↑((ModuleCat.restrictScalars (φ.app X)).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))<GOAL>(PresheafOfModules.Hom.app ((PresheafOfModules.pushforward φ).map α) X) m = (PresheafOfModules.Hom.app α (Opposite.op (F.obj (Opposite.unop X)))) m
<VAR>k : Type u<VAR>Field k<VAR>A : Type w<VAR>Ring A<VAR>Algebra k A<VAR>M : ModuleCat A<GOAL>IsScalarTower k A ↑M
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 1), x ^ i = x * ∑ i ∈ Finset.range n, x ^ i + 1
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 1), x ^ i = x ^ n + ∑ i ∈ Finset.range n, x ^ i
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<GOAL>∑ i ∈ Finset.range 0, x ^ i = 0
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<GOAL>∑ i ∈ Finset.range 1, x ^ i = 1
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<GOAL>∑ i ∈ Finset.range 2, x ^ i = x + 1
<VAR>α : Type u<VAR>Semiring α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, 0 ^ i = if n = 0 then 0 else 1
<VAR>α : Type u<VAR>Semiring α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, 1 ^ i = ↑n
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<VAR>n : ℕ<GOAL>MulOpposite.op (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, MulOpposite.op x ^ i
<VAR>α : Type u<VAR>Semiring α<VAR>x y : α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, MulOpposite.op y ^ (n - 1 - i) * MulOpposite.op x ^ i = ∑ i ∈ Finset.range n, MulOpposite.op y ^ i * MulOpposite.op x ^ (n - 1 - i)
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x ^ i * 1 ^ (n - 1 - i) = ∑ i ∈ Finset.range n, x ^ i
<VAR>α : Type u<VAR>Semiring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
<VAR>α : Type u<VAR>Ring α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, (-1) ^ i = if Even n then 0 else 1
<VAR>α : Type u_1<VAR>CommRing α<VAR>x : α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x ^ i * x ^ (n - 1 - i) = ↑n * x ^ (n - 1)
<VAR>α : Type u<VAR>CommSemiring α<VAR>x y : α<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
<VAR>α : Type u<VAR>Semiring α<VAR>x : α<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(y - x) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>(x - y) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
<VAR>α : Type u<VAR>CommRing α<VAR>x y : α<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>x - y ∣ x ^ n - y ^ n
<VAR>α : Type u<VAR>CommRing α<VAR>x y : α<VAR>n : ℕ<GOAL>x - y ∣ x ^ n - y ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>n : ℕ<GOAL>1 - x ∣ 1 - x ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>n : ℕ<GOAL>x - 1 ∣ x ^ n - 1
<VAR>x y n : ℕ<GOAL>x - y ∣ x ^ n - y ^ n
<VAR>α : Type u<VAR>CommRing α<VAR>x y : α<VAR>n : ℕ<VAR>h : Odd n<GOAL>x + y ∣ x ^ n + y ^ n
<VAR>x y : ℕ<VAR>n : ℕ<VAR>h : Odd n<GOAL>x + y ∣ x ^ n + y ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, x ^ i) * (x - 1) = x ^ n - 1
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>n : ℕ<GOAL>(x - 1) * ∑ i ∈ Finset.range n, x ^ i = x ^ n - 1
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>n : ℕ<GOAL>(1 - x) * ∑ i ∈ Finset.range n, x ^ i = 1 - x ^ n
<VAR>α : Type u<VAR>Semiring α<VAR>x y : α<VAR>n : ℕ<VAR>h : Commute x y<GOAL>∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
<VAR>α : Type u<VAR>CommSemiring α<VAR>x y : α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
<VAR>α : Type u<VAR>DivisionRing α<VAR>x y : α<VAR>h' : Commute x y<VAR>h : x ≠ y<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
<VAR>α : Type u<VAR>Field α<VAR>x y : α<VAR>h : x ≠ y<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ n) / (x - y)
<VAR>α : Type u<VAR>DivisionRing α<VAR>x : α<VAR>h : x ≠ 1<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
<VAR>α : Type u<VAR>CommRing α<VAR>x y : α<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
<VAR>α : Type u<VAR>CommRing α<VAR>x y : α<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
<VAR>α : Type u<VAR>Ring α<VAR>x y : α<VAR>h : Commute x y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∑ i ∈ Finset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
<VAR>α : Type u<VAR>Ring α<VAR>x : α<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(∑ i ∈ Finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
<VAR>α : Type u<VAR>DivisionRing α<VAR>x y : α<VAR>h : Commute x y<VAR>hxy : x ≠ y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
<VAR>α : Type u<VAR>Field α<VAR>x y : α<VAR>hxy : x ≠ y<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
<VAR>α : Type u<VAR>DivisionRing α<VAR>x : α<VAR>hx : x ≠ 1<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Finset.Ico m n, x ^ i = (x ^ n - x ^ m) / (x - 1)
<VAR>α : Type u<VAR>DivisionRing α<VAR>x : α<VAR>hx : x ≠ 1<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>∑ i ∈ Finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
<VAR>α : Type u<VAR>LinearOrderedField α<VAR>x : α<VAR>hx : 0 ≤ x<VAR>h'x : x < 1<VAR>m n : ℕ<GOAL>∑ i ∈ Finset.Ico m n, x ^ i ≤ x ^ m / (1 - x)
<VAR>α : Type u<VAR>DivisionRing α<VAR>x : α<VAR>hx1 : x ≠ 1<VAR>hx0 : x ≠ 0<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Semiring β<VAR>x : α<VAR>n : ℕ<VAR>f : α →+* β<GOAL>f (∑ i ∈ Finset.range n, x ^ i) = ∑ i ∈ Finset.range n, f x ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>Semiring α<VAR>Semiring β<VAR>x y : α<VAR>n : ℕ<VAR>f : α →+* β<GOAL>f (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) = ∑ i ∈ Finset.range n, f x ^ i * f y ^ (n - 1 - i)
<VAR>a b n : ℕ<GOAL>(b - 1) * ∑ i ∈ Finset.range n.succ, a / b ^ i ≤ a * b - a / b ^ n
<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>∑ i ∈ Finset.range n, a / b ^ i ≤ a * b / (b - 1)
<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>∑ i ∈ Finset.Ico 1 n, a / b ^ i ≤ a / (b - 1)
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>StrictOrderedSemiring α<VAR>hx : 0 ≤ x<VAR>hn : n ≠ 0<GOAL>0 < ∑ i ∈ Finset.range n, x ^ i
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>StrictOrderedRing α<VAR>hx : x < 0<VAR>hx' : 0 < x + 1<VAR>hn : 1 < n<GOAL>0 < ∑ i ∈ Finset.range n, x ^ i ∧ ∑ i ∈ Finset.range n, x ^ i < 1
<VAR>α : Type u<VAR>x : α<VAR>StrictOrderedRing α<VAR>hx : x + 1 ≤ 0<VAR>n : ℕ<GOAL>if Even n then ∑ i ∈ Finset.range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ Finset.range n, x ^ i
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>StrictOrderedRing α<VAR>hx : x + 1 < 0<VAR>hn : 1 < n<GOAL>if Even n then ∑ i ∈ Finset.range n, x ^ i < 0 else 1 < ∑ i ∈ Finset.range n, x ^ i
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>LinearOrderedRing α<VAR>hx : 0 < x + 1<VAR>hn : n ≠ 0<GOAL>0 < ∑ i ∈ Finset.range n, x ^ i
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>LinearOrderedRing α<VAR>h : Odd n<GOAL>0 < ∑ i ∈ Finset.range n, x ^ i
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>LinearOrderedRing α<VAR>hn : n ≠ 0<GOAL>0 < ∑ i ∈ Finset.range n, x ^ i ↔ Odd n ∨ 0 < x + 1
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>LinearOrderedRing α<VAR>hx : x ≠ -1<VAR>hn : n ≠ 0<GOAL>∑ i ∈ Finset.range n, x ^ i ≠ 0
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>LinearOrderedRing α<VAR>hn : n ≠ 0<GOAL>∑ i ∈ Finset.range n, x ^ i = 0 ↔ x = -1 ∧ Even n
<VAR>α : Type u<VAR>n : ℕ<VAR>x : α<VAR>LinearOrderedRing α<VAR>hn : n ≠ 0<GOAL>∑ i ∈ Finset.range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0
<VAR>m : ℕ<VAR>hm : 2 ≤ m<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, m ^ k = (m ^ n - 1) / (m - 1)
<VAR>m n : ℕ<VAR>s : Finset ℕ<VAR>hm : 2 ≤ m<VAR>hs : ∀ k ∈ s, k < n<GOAL>∑ k ∈ s, m ^ k < m ^ n
<VAR>R : Type u<VAR>Ring R<GOAL>CategoryTheory.Limits.HasKernels (ModuleCat R)
<VAR>R : Type u<VAR>Ring R<GOAL>CategoryTheory.Limits.HasCokernels (ModuleCat R)
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>(ModuleCat.kernelIsoKer f).inv ≫ CategoryTheory.Limits.kernel.ι f = (LinearMap.ker f).subtype