ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>Ring R<VAR>X : ModuleCat R<GOAL>(CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj X = AddCommGrp.of ↑X
<VAR>R : Type u<VAR>Ring R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<GOAL>(CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj (ModuleCat.of R X) = AddCommGrp.of X
<VAR>R : Type u<VAR>Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).map f = LinearMap.toAddMonoidHom f
<VAR>R : Type u<VAR>Ring R<VAR>X Y : Type v<VAR>AddCommGroup X<VAR>Module R X<VAR>AddCommGroup Y<VAR>Module R Y<VAR>f : X →ₗ[R] Y<VAR>x : X<GOAL>(ModuleCat.ofHom f) x = f x
<VAR>R : Type u<VAR>Ring R<VAR>X : ModuleCat R<GOAL>ModuleCat.of R ↑X = X
<VAR>R : Type u<VAR>Ring R<VAR>X : Type v<VAR>AddCommGroup X<VAR>Module R X<GOAL>↑(ModuleCat.of R X) = X
<VAR>R : Type u<VAR>Ring R<VAR>M : ModuleCat R<GOAL>M.ofSelfIso.hom = 𝟙 M
<VAR>R : Type u<VAR>Ring R<VAR>M : ModuleCat R<GOAL>M.ofSelfIso.inv = 𝟙 M
<VAR>R : Type u<VAR>Ring R<VAR>M : ModuleCat R<VAR>Subsingleton ↑M<GOAL>CategoryTheory.Limits.IsZero M
<VAR>R : Type u<VAR>Ring R<VAR>M : ModuleCat R<VAR>m : ↑M<GOAL>(𝟙 M) m = m
<VAR>R : Type u<VAR>Ring 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>Ring 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>Ring R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>(CategoryTheory.forget (ModuleCat R)).map f = ⇑f
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ : Type v<VAR>g₁ : AddCommGroup X₁<VAR>g₂ : AddCommGroup X₂<VAR>m₁ : Module R X₁<VAR>m₂ : Module R X₂<VAR>e : X₁ ≃ₗ[R] X₂<GOAL>e.toModuleIso.inv = ↑e.symm
<VAR>R : Type u<VAR>Ring R<VAR>X₁ X₂ : Type v<VAR>g₁ : AddCommGroup X₁<VAR>g₂ : AddCommGroup X₂<VAR>m₁ : Module R X₁<VAR>m₂ : Module R X₂<VAR>e : X₁ ≃ₗ[R] X₂<GOAL>e.toModuleIso.hom = ↑e
<VAR>R : Type u<VAR>Ring R<VAR>X Y : Type u<VAR>AddCommGroup X<VAR>AddCommGroup Y<VAR>Module R X<VAR>Module R Y<VAR>e : X ≃ₗ[R] Y<GOAL>linearEquivIsoModuleIso.hom e = e.toModuleIso
<VAR>R : Type u<VAR>Ring R<VAR>X Y : Type u<VAR>AddCommGroup X<VAR>AddCommGroup Y<VAR>Module R X<VAR>Module R Y<VAR>i : ModuleCat.of R X ≅ ModuleCat.of R Y<GOAL>linearEquivIsoModuleIso.inv i = i.toLinearEquiv
<VAR>S : Type u<VAR>CommRing S<VAR>X Y X' Y' : ModuleCat S<VAR>i : X ≅ X'<VAR>j : Y ≅ Y'<VAR>f : X ⟶ Y<GOAL>(i.homCongr j) f = (i.toLinearEquiv.arrowCongr j.toLinearEquiv) f
<VAR>S : Type u<VAR>CommRing S<VAR>X X' : ModuleCat S<VAR>i : X ≅ X'<VAR>f : CategoryTheory.End X<GOAL>i.conj f = i.toLinearEquiv.conj f
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>r : R<GOAL>(CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).map f ≫ N.smul r = M.smul r ≫ (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).map f
<VAR>R : Type u<VAR>Ring R<VAR>r : R<VAR>M : ModuleCat R<GOAL>((ModuleCat.smulNatTrans R) r).app M = M.smul r
<VAR>R : Type u<VAR>Ring R<VAR>A : AddCommGrp<VAR>φ : R →+* CategoryTheory.End A<VAR>r : R<VAR>x : ↑(ModuleCat.mkOfSMul' φ)<GOAL>r • x = (let_fun this := φ r; this) x
<VAR>R : Type u<VAR>Ring R<VAR>A : AddCommGrp<VAR>φ : R →+* CategoryTheory.End A<VAR>r : R<GOAL>(ModuleCat.mkOfSMul φ).smul r = φ r
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj N<VAR>hφ : ∀ (r : R), φ ≫ N.smul r = M.smul r ≫ φ<VAR>a : ↑((CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj M)<GOAL>(ModuleCat.homMk φ hφ) a = φ a
<VAR>R : Type u<VAR>Ring R<VAR>M N : ModuleCat R<VAR>φ : (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj M ⟶ (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).obj N<VAR>hφ : ∀ (r : R), φ ≫ N.smul r = M.smul r ≫ φ<GOAL>(CategoryTheory.forget₂ (ModuleCat R) AddCommGrp).map (ModuleCat.homMk φ hφ) = φ
<VAR>R : Type u_1<VAR>Ring R<VAR>G : ModuleCat R<VAR>H : Type u<VAR>AddCommGroup H<VAR>Module R H<VAR>f : ↑G →ₗ[R] H<GOAL>f ∘ₗ 𝟙 G = f
<VAR>R : Type u_1<VAR>Ring R<VAR>G : Type u<VAR>AddCommGroup G<VAR>Module R G<VAR>H : ModuleCat R<VAR>f : G →ₗ[R] ↑H<GOAL>𝟙 H ∘ₗ f = f
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>ModuleCat.factorThruImage f ≫ ModuleCat.image.ι f = f
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>ModuleCat.image.lift F' ≫ F'.m = ModuleCat.image.ι f
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>(ModuleCat.imageIsoRange f).inv ≫ CategoryTheory.Limits.image.ι f = ModuleCat.ofHom (LinearMap.range f).subtype
<VAR>R : Type u<VAR>Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<GOAL>(ModuleCat.imageIsoRange f).hom ≫ ModuleCat.ofHom (LinearMap.range f).subtype = CategoryTheory.Limits.image.ι f
<VAR>R : Type w<VAR>Ring R<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>CategoryTheory.Limits.HasColimit (F ⋙ CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)<VAR>r : R<GOAL>(ModuleCat.HasColimit.coconePointSMul F) r = CategoryTheory.Limits.colimMap { app := fun j => (F.obj j).smul r, naturality := ⋯ }
<VAR>R : Type w<VAR>Ring R<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>CategoryTheory.Limits.HasColimit (F ⋙ CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)<GOAL>(ModuleCat.HasColimit.colimitCocone F).pt = ModuleCat.mkOfSMul (ModuleCat.HasColimit.coconePointSMul F)
<VAR>R : Type w<VAR>Ring R<VAR>J : Type u<VAR>CategoryTheory.Category.{v, u} J<VAR>F : J ⥤ ModuleCat R<VAR>CategoryTheory.Limits.HasColimit (F ⋙ CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)<VAR>j : J<GOAL>(ModuleCat.HasColimit.colimitCocone F).ι.app j = ModuleCat.homMk (CategoryTheory.Limits.colimit.ι (F ⋙ CategoryTheory.forget₂ (ModuleCat R) AddCommGrp) j) ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>X₁ X₂ Y₁ Y₂ : ModuleCat R<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(f ⊗ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ f)
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>Z : ModuleCat R<GOAL>f ▷ Z ≫ (Y.braiding Z).hom = (X.braiding Z).hom ≫ Z ◁ f
<VAR>R : Type u<VAR>CommRing R<VAR>X : ModuleCat R<VAR>Y Z : ModuleCat R<VAR>f : Y ⟶ Z<GOAL>X ◁ f ≫ (X.braiding Z).hom = (X.braiding Y).hom ≫ f ▷ X
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : ModuleCat R<GOAL>(α_ X Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (X.braiding Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (X.braiding Z).hom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : ModuleCat R<GOAL>(α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv = X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<VAR>m : ↑M<VAR>n : ↑N<GOAL>(β_ M N).hom (m ⊗ₜ[R] n) = n ⊗ₜ[R] m
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<VAR>m : ↑M<VAR>n : ↑N<GOAL>(β_ M N).inv (n ⊗ₜ[R] m) = m ⊗ₜ[R] n
<VAR>R : Type u<VAR>CommRing R<VAR>A B C D : ModuleCat R<GOAL>CategoryTheory.tensor_μ (ModuleCat R) (A, B) (C, D) = ↑(TensorProduct.tensorTensorTensorComm R ↑A ↑B ↑C ↑D)
<VAR>R : Type u<VAR>CommRing R<VAR>A B C D : ModuleCat R<VAR>x : ↑A<VAR>y : ↑B<VAR>z : ↑C<VAR>w : ↑D<GOAL>(CategoryTheory.tensor_μ (ModuleCat R) (A, B) (C, D)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z ⊗ₜ[R] w) = (x ⊗ₜ[R] z) ⊗ₜ[R] y ⊗ₜ[R] w
<VAR>α : Type u<GOAL>↑(CommRingCat.free.obj α) = MvPolynomial α ℤ
<VAR>α β : Type u<VAR>f : α → β<GOAL>⇑(CommRingCat.free.map f) = ⇑(MvPolynomial.rename f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_1<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<GOAL>CategoryTheory.Epi (CommRingCat.ofHom (algebraMap R S))
<VAR>R S : CommRingCat<VAR>f : R ≅ S<GOAL>IsLocalRingHom f.hom
<VAR>P Q : AddCommGrp<VAR>f g : P ⟶ Q<VAR>x : ↑P<GOAL>(f + g) x = f x + g x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>{X Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F ⋙ PresheafOfModules.evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F ⋙ PresheafOfModules.evaluation R X)<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>(PresheafOfModules.colimitBundledCore F).map f = CategoryTheory.Limits.colimMap (CategoryTheory.whiskerLeft F (PresheafOfModules.restriction R f)) ≫ (CategoryTheory.preservesColimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ PresheafOfModules.evaluation R Y)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>{X Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F ⋙ PresheafOfModules.evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F ⋙ PresheafOfModules.evaluation R X)<VAR>X : Cᵒᵖ<GOAL>(PresheafOfModules.colimitBundledCore F).obj X = CategoryTheory.Limits.colimit (F ⋙ PresheafOfModules.evaluation R X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>{X Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F ⋙ PresheafOfModules.evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F ⋙ PresheafOfModules.evaluation R X)<VAR>i j : J<VAR>f : i ⟶ j<GOAL>F.map f ≫ PresheafOfModules.colimitCoconeιApp F j = PresheafOfModules.colimitCoconeιApp F i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>{X Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F ⋙ PresheafOfModules.evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F ⋙ PresheafOfModules.evaluation R X)<GOAL>(PresheafOfModules.colimitCocone F).pt = (PresheafOfModules.colimitBundledCore F).toPresheafOfModules
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>{X Y : Cᵒᵖ} → (f : X ⟶ Y) → CategoryTheory.Limits.PreservesColimit (F ⋙ PresheafOfModules.evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F ⋙ PresheafOfModules.evaluation R X)<VAR>j : J<GOAL>(PresheafOfModules.colimitCocone F).ι.app j = PresheafOfModules.colimitCoconeιApp F j
<VAR>R : Type u<VAR>Ring R<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : ∃ k f g, (F.map f) x.snd = (F.map g) y.snd<GOAL>ModuleCat.FilteredColimits.M.mk F x = ModuleCat.FilteredColimits.M.mk F y
<VAR>R : Type u<VAR>Ring R<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r : R<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : CategoryTheory.Limits.Types.FilteredColimit.Rel (F ⋙ CategoryTheory.forget (ModuleCat R)) x y<GOAL>ModuleCat.FilteredColimits.colimitSMulAux F r x = ModuleCat.FilteredColimits.colimitSMulAux F r y
<VAR>R : Type u<VAR>Ring R<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r : R<VAR>x : (j : J) × ↑(F.obj j)<GOAL>r • ModuleCat.FilteredColimits.M.mk F x = ModuleCat.FilteredColimits.M.mk F ⟨x.fst, r • x.snd⟩
<VAR>R : Type u<VAR>Ring R<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>x : ↑(ModuleCat.FilteredColimits.M F)<GOAL>1 • x = x
<VAR>R : Type u<VAR>Ring R<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ ModuleCatMax R<VAR>r s : R<VAR>x : ↑(ModuleCat.FilteredColimits.M F)<GOAL>(r + s) • x = r • x + s • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>Monoid β<VAR>e : α ≃* β<VAR>γ : Type u_3<VAR>Monoid γ<VAR>f : β →* γ<GOAL>(MonoidHom.precompEquiv e γ) f = f.comp ↑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>Monoid β<VAR>e : α ≃* β<VAR>γ : Type u_3<VAR>Monoid γ<VAR>g : α →* γ<GOAL>(MonoidHom.precompEquiv e γ).symm g = g.comp ↑e.symm
<VAR>α : Type u<VAR>Group α<VAR>φ : Multiplicative ℤ →* α<GOAL>(MonoidHom.fromMultiplicativeIntEquiv α) φ = φ (Multiplicative.ofAdd 1)
<VAR>α : Type u<VAR>Group α<VAR>x : α<GOAL>(MonoidHom.fromMultiplicativeIntEquiv α).symm x = (zpowersHom α) x
<VAR>α : Type u<VAR>Group α<GOAL>∀ (a : α) (a_1 : ULift.{u, 0} (Multiplicative ℤ)), ((MonoidHom.fromULiftMultiplicativeIntEquiv α).symm a) a_1 = a ^ Multiplicative.toAdd (MulEquiv.ulift a_1)
<VAR>α : Type u<VAR>Group α<GOAL>∀ (a : ULift.{u, 0} (Multiplicative ℤ) →* α), (MonoidHom.fromULiftMultiplicativeIntEquiv α) a = a (MulEquiv.ulift.symm (Multiplicative.ofAdd 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoid α<VAR>AddMonoid β<VAR>e : α ≃+ β<VAR>γ : Type u_3<VAR>AddMonoid γ<VAR>g : α →+ γ<GOAL>(AddMonoidHom.precompEquiv e γ).symm g = g.comp ↑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddMonoid α<VAR>AddMonoid β<VAR>e : α ≃+ β<VAR>γ : Type u_3<VAR>AddMonoid γ<VAR>f : β →+ γ<GOAL>(AddMonoidHom.precompEquiv e γ) f = f.comp ↑e
<VAR>α : Type u<VAR>AddGroup α<VAR>φ : ℤ →+ α<GOAL>(AddMonoidHom.fromIntEquiv α) φ = φ 1
<VAR>α : Type u<VAR>AddGroup α<VAR>x : α<GOAL>(AddMonoidHom.fromIntEquiv α).symm x = (zmultiplesHom α) x
<VAR>α : Type u<VAR>AddGroup α<GOAL>∀ (a : α) (a_1 : ULift.{u, 0} ℤ), ((AddMonoidHom.fromULiftIntEquiv α).symm a) a_1 = AddEquiv.ulift a_1 • a
<VAR>α : Type u<VAR>AddGroup α<GOAL>∀ (a : ULift.{u, 0} ℤ →+ α), (AddMonoidHom.fromULiftIntEquiv α) a = a (AddEquiv.ulift.symm 1)
<VAR>G H : AddCommGrp<GOAL>(G.binaryProductLimitCone H).cone.pt = AddCommGrp.of (↑G × ↑H)
<VAR>G H : AddCommGrp<VAR>s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair G H)<GOAL>(G.binaryProductLimitCone H).isLimit.lift s = AddMonoidHom.prod (s.π.app { as := CategoryTheory.Limits.WalkingPair.left }) (s.π.app { as := CategoryTheory.Limits.WalkingPair.right })
<VAR>G H : AddCommGrp<GOAL>(G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = AddMonoidHom.fst ↑G ↑H
<VAR>G H : AddCommGrp<GOAL>(G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = AddMonoidHom.snd ↑G ↑H
<VAR>G H : AddCommGrp<VAR>i : ↑(CategoryTheory.Limits.BinaryBiproduct.bicone G H).toCone.pt<GOAL>(G.biprodIsoProd H).hom i = (CategoryTheory.Limits.biprod.fst i, CategoryTheory.Limits.biprod.snd i)
<VAR>G H : AddCommGrp<GOAL>(G.biprodIsoProd H).inv ≫ CategoryTheory.Limits.biprod.fst = AddMonoidHom.fst ↑G ↑H
<VAR>G H : AddCommGrp<GOAL>(G.biprodIsoProd H).inv ≫ CategoryTheory.Limits.biprod.snd = AddMonoidHom.snd ↑G ↑H
<VAR>J : Type w<VAR>f : J → AddCommGrp<GOAL>(AddCommGrp.HasLimit.productLimitCone f).cone.π = CategoryTheory.Discrete.natTrans fun j => Pi.evalAddMonoidHom (fun j => ↑(f j)) j.as
<VAR>J : Type w<VAR>f : J → AddCommGrp<GOAL>(AddCommGrp.HasLimit.productLimitCone f).cone.pt = AddCommGrp.of ((j : J) → ↑(f j))
<VAR>J : Type w<VAR>f : J → AddCommGrp<VAR>s : CategoryTheory.Limits.Fan f<GOAL>(AddCommGrp.HasLimit.productLimitCone f).isLimit.lift s = AddCommGrp.HasLimit.lift f s
<VAR>J : Type<VAR>Finite J<VAR>f : J → AddCommGrp<VAR>x : ↑(CategoryTheory.Limits.biproduct.bicone f).toCone.pt<VAR>j : J<GOAL>(AddCommGrp.biproductIsoPi f).hom x j = (CategoryTheory.Limits.biproduct.π f j) x
<VAR>J : Type<VAR>Finite J<VAR>f : J → AddCommGrp<VAR>j : J<GOAL>(AddCommGrp.biproductIsoPi f).inv ≫ CategoryTheory.Limits.biproduct.π f j = Pi.evalAddMonoidHom (fun j => ↑(f j)) j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ PresheafOfModules.evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj X))).sections<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>(PresheafOfModules.limitBundledCore F).map f = CategoryTheory.Limits.limMap (CategoryTheory.whiskerLeft F (PresheafOfModules.restriction R f)) ≫ (CategoryTheory.preservesLimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ PresheafOfModules.evaluation R Y)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ PresheafOfModules.evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj X))).sections<VAR>X : Cᵒᵖ<GOAL>(PresheafOfModules.limitBundledCore F).obj X = CategoryTheory.Limits.limit (F ⋙ PresheafOfModules.evaluation R X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ PresheafOfModules.evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj X))).sections<VAR>i j : J<VAR>f : i ⟶ j<GOAL>PresheafOfModules.limitConeπApp F i ≫ F.map f = PresheafOfModules.limitConeπApp F j
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ PresheafOfModules.evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj X))).sections<GOAL>(PresheafOfModules.limitCone F).pt = (PresheafOfModules.limitBundledCore F).toPresheafOfModules
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ PresheafOfModules.evaluation R X) ⋙ CategoryTheory.forget (ModuleCat ↑(R.obj X))).sections<VAR>j : J<GOAL>(PresheafOfModules.limitCone F).π.app j = PresheafOfModules.limitConeπApp F j
<VAR>X : SemiRingCat<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : SemiRingCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y : SemiRingCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget SemiRingCat).map f = ⇑f
<VAR>X Y : SemiRingCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>Semiring R<GOAL>↑(SemiRingCat.of R) = R
<VAR>X : Type u<VAR>Semiring X<GOAL>⇑(𝟙 (SemiRingCat.of X)) = ⇑(RingHom.id X)
<VAR>X Y Z : Type u<VAR>Semiring X<VAR>Semiring Y<VAR>Semiring Z<VAR>f : X →+* Y<VAR>g : Y →+* Z<GOAL>⇑(f ≫ g) = ⇑(g.comp f)
<VAR>X Y : Type u<VAR>Semiring X<VAR>Semiring Y<VAR>f g : X →+* Y<VAR>h : ∀ (x : X), f x = g x<GOAL>f = g
<VAR>X Y : Type u_1<VAR>Semiring X<VAR>Semiring Y<VAR>e : X ≃+* Y<GOAL>⇑↑e = ⇑e
<VAR>R S : Type u<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>x : R<GOAL>(SemiRingCat.ofHom f) x = f x
<VAR>X Y : Type u<VAR>Semiring X<VAR>Semiring Y<VAR>e : X ≃+* Y<GOAL>e.toSemiRingCatIso.inv = e.symm.toRingHom
<VAR>X Y : Type u<VAR>Semiring X<VAR>Semiring Y<VAR>e : X ≃+* Y<GOAL>e.toSemiRingCatIso.hom = e.toRingHom
<VAR>X : RingCat<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : RingCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y : RingCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget RingCat).map f = ⇑f
<VAR>X Y : RingCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>Ring R<GOAL>↑(RingCat.of R) = R
<VAR>X : Type u<VAR>Ring X<GOAL>⇑(𝟙 (RingCat.of X)) = ⇑(RingHom.id X)
<VAR>X Y Z : Type u<VAR>Ring X<VAR>Ring Y<VAR>Ring Z<VAR>f : X →+* Y<VAR>g : Y →+* Z<GOAL>⇑(f ≫ g) = ⇑(g.comp f)
<VAR>X Y : Type u<VAR>Ring X<VAR>Ring Y<VAR>f g : X →+* Y<VAR>h : ∀ (x : X), f x = g x<GOAL>f = g
<VAR>X Y : Type u_1<VAR>Ring X<VAR>Ring Y<VAR>e : X ≃+* Y<GOAL>⇑↑e = ⇑e
<VAR>X : CommSemiRingCat<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : CommSemiRingCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y : CommSemiRingCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget CommSemiRingCat).map f = ⇑f
<VAR>X Y : CommSemiRingCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>X Y : Type u_1<VAR>CommSemiring X<VAR>CommSemiring Y<VAR>e : X ≃+* Y<GOAL>⇑↑e = ⇑e
<VAR>R : Type u<VAR>CommSemiring R<GOAL>↑(CommSemiRingCat.of R) = R
<VAR>X : Type u<VAR>CommSemiring X<GOAL>⇑(𝟙 (CommSemiRingCat.of X)) = ⇑(RingHom.id X)
<VAR>X Y Z : Type u<VAR>CommSemiring X<VAR>CommSemiring Y<VAR>CommSemiring Z<VAR>f : X →+* Y<VAR>g : Y →+* Z<GOAL>⇑(f ≫ g) = ⇑(g.comp f)
<VAR>X Y : Type u<VAR>CommSemiring X<VAR>CommSemiring Y<VAR>f g : X →+* Y<VAR>h : ∀ (x : X), f x = g x<GOAL>f = g
<VAR>X Y : Type u<VAR>CommSemiring X<VAR>CommSemiring Y<VAR>e : X ≃+* Y<GOAL>e.toCommSemiRingCatIso.hom = e.toRingHom
<VAR>X Y : Type u<VAR>CommSemiring X<VAR>CommSemiring Y<VAR>e : X ≃+* Y<GOAL>e.toCommSemiRingCatIso.inv = e.symm.toRingHom
<VAR>X : CommRingCat<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : CommRingCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>R : CommRingCat<VAR>x : ↑R<GOAL>(𝟙 R) x = x
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>x : ↑R<GOAL>(f ≫ g) x = g (f x)
<VAR>R : CommRingCat<GOAL>(CategoryTheory.forget CommRingCat).obj R = ↑R
<VAR>X Y : CommRingCat<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget CommRingCat).map f = ⇑f
<VAR>X Y : CommRingCat<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>X Y : Type u_1<VAR>CommRing X<VAR>CommRing Y<VAR>e : X ≃+* Y<GOAL>⇑↑e = ⇑e
<VAR>R : Type u<VAR>CommRing R<GOAL>↑(CommRingCat.of R) = R
<VAR>X : Type u<VAR>CommRing X<GOAL>⇑(𝟙 (CommRingCat.of X)) = ⇑(RingHom.id X)
<VAR>X Y Z : Type u<VAR>CommRing X<VAR>CommRing Y<VAR>CommRing Z<VAR>f : X →+* Y<VAR>g : Y →+* Z<GOAL>⇑(f ≫ g) = ⇑(g.comp f)
<VAR>X Y : Type u<VAR>CommRing X<VAR>CommRing Y<VAR>f g : X →+* Y<VAR>h : ∀ (x : X), f x = g x<GOAL>f = g
<VAR>X Y : Type u<VAR>Ring X<VAR>Ring Y<VAR>e : X ≃+* Y<GOAL>e.toRingCatIso.inv = e.symm.toRingHom
<VAR>X Y : Type u<VAR>Ring X<VAR>Ring Y<VAR>e : X ≃+* Y<GOAL>e.toRingCatIso.hom = e.toRingHom
<VAR>X Y : Type u<VAR>CommRing X<VAR>CommRing Y<VAR>e : X ≃+* Y<GOAL>e.toCommRingCatIso.hom = e.toRingHom
<VAR>X Y : Type u<VAR>CommRing X<VAR>CommRing Y<VAR>e : X ≃+* Y<GOAL>e.toCommRingCatIso.inv = e.symm.toRingHom
<VAR>X Y : CommRingCat<VAR>i : X ≅ Y<GOAL>i.commRingCatIsoToRingEquiv.toRingHom = i.hom
<VAR>X Y : CommRingCat<VAR>i : X ≅ Y<GOAL>i.commRingCatIsoToRingEquiv.symm.toRingHom = i.inv
<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<GOAL>f ≫ g = RingHom.comp g f
<VAR>R S T : Type u_1<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<GOAL>g.comp f = CommRingCat.ofHom f ≫ CommRingCat.ofHom g
<VAR>G : SemiRingCat<VAR>H : Type u<VAR>Semiring H<VAR>f : ↑G →+* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>Semiring G<VAR>H : SemiRingCat<VAR>f : G →+* ↑H<GOAL>RingHom.comp (𝟙 H) f = f
<VAR>G : CommSemiRingCat<VAR>H : Type u<VAR>CommSemiring H<VAR>f : ↑G →+* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>CommSemiring G<VAR>H : CommSemiRingCat<VAR>f : G →+* ↑H<GOAL>RingHom.comp (𝟙 H) f = f
<VAR>G : RingCat<VAR>H : Type u<VAR>Ring H<VAR>f : ↑G →+* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>Ring G<VAR>H : RingCat<VAR>f : G →+* ↑H<GOAL>RingHom.comp (𝟙 H) f = f
<VAR>G : CommRingCat<VAR>H : Type u<VAR>CommRing H<VAR>f : ↑G →+* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>CommRing G<VAR>H : CommRingCat<VAR>f : G →+* ↑H<GOAL>RingHom.comp (𝟙 H) f = f
<VAR>X : Grp<GOAL>Grp.toAddGrp.obj X = AddGrp.of (Additive ↑X)
<VAR>X Y : Grp<VAR>a : ↑X →* ↑Y<GOAL>Grp.toAddGrp.map a = MonoidHom.toAdditive a
<VAR>X : CommGrp<GOAL>CommGrp.toAddCommGrp.obj X = AddCommGrp.of (Additive ↑X)
<VAR>X Y : CommGrp<VAR>a : ↑X →* ↑Y<GOAL>CommGrp.toAddCommGrp.map a = MonoidHom.toAdditive a
<VAR>X Y : AddGrp<VAR>a : ↑X →+ ↑Y<GOAL>AddGrp.toGrp.map a = AddMonoidHom.toMultiplicative a
<VAR>X : AddGrp<GOAL>AddGrp.toGrp.obj X = Grp.of (Multiplicative ↑X)
<VAR>X : AddCommGrp<GOAL>AddCommGrp.toCommGrp.obj X = CommGrp.of (Multiplicative ↑X)
<VAR>X Y : AddCommGrp<VAR>a : ↑X →+ ↑Y<GOAL>AddCommGrp.toCommGrp.map a = AddMonoidHom.toMultiplicative a
<VAR>X : AddGrp<GOAL>⇑(𝟙 X) = id
<VAR>X : Grp<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : Grp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y Z : AddGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y Z : Grp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>f ≫ g = MonoidHom.comp g f
<VAR>X Y Z : AddGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>f ≫ g = AddMonoidHom.comp g f
<VAR>X Y : Grp<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget Grp).map f = ⇑f
<VAR>X Y : AddGrp<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>X Y : Grp<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>AddGroup R<GOAL>↑(AddGrp.of R) = R
<VAR>R : Type u<VAR>Group R<GOAL>↑(Grp.of R) = R