ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G H K : Type u_1<VAR>Group G<VAR>Group H<VAR>Group K<VAR>f : G →* H<VAR>g : H →* K<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>G H K : Type u_1<VAR>AddGroup G<VAR>AddGroup H<VAR>AddGroup K<VAR>f : G →+ H<VAR>g : H →+ K<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>G : Type u_1<VAR>Group G<GOAL>⇑(𝟙 (Grp.of G)) = id
<VAR>G : Type u_1<VAR>AddGroup G<GOAL>⇑(𝟙 (AddGrp.of G)) = id
<VAR>G H : AddGrp<VAR>g : ↑G<GOAL>0 g = 0
<VAR>G H : Grp<VAR>g : ↑G<GOAL>1 g = 1
<VAR>X Y : Type u_1<VAR>Group X<VAR>Group Y<VAR>f : X →* Y<VAR>x : X<GOAL>(Grp.ofHom f) x = f x
<VAR>X Y : Type u_1<VAR>AddGroup X<VAR>AddGroup Y<VAR>f : X →+ Y<VAR>x : X<GOAL>(AddGrp.ofHom f) x = f x
<VAR>X Y : Grp<VAR>f : X ⟶ Y<GOAL>Grp.uliftFunctor.map f = Grp.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))
<VAR>X : Grp<GOAL>Grp.uliftFunctor.obj X = Grp.of (ULift.{v, u} ↑X)
<VAR>X Y : AddGrp<VAR>f : X ⟶ Y<GOAL>AddGrp.uliftFunctor.map f = AddGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))
<VAR>X : AddGrp<GOAL>AddGrp.uliftFunctor.obj X = AddGrp.of (ULift.{v, u} ↑X)
<VAR>X : CommGrp<GOAL>⇑(𝟙 X) = id
<VAR>X : AddCommGrp<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : AddCommGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y Z : CommGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y Z : CommGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>f ≫ g = MonoidHom.comp g f
<VAR>X Y Z : AddCommGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>f ≫ g = AddMonoidHom.comp g f
<VAR>X Y : AddCommGrp<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget AddCommGrp).map f = ⇑f
<VAR>X Y : CommGrp<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget CommGrp).map f = ⇑f
<VAR>X Y : CommGrp<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>X Y : AddCommGrp<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : ↑X), f x = g x<GOAL>f = g
<VAR>R : Type u<VAR>AddCommGroup R<GOAL>↑(AddCommGrp.of R) = R
<VAR>R : Type u<VAR>CommGroup R<GOAL>↑(CommGrp.of R) = R
<VAR>G H K : Type u_1<VAR>CommGroup G<VAR>CommGroup H<VAR>CommGroup K<VAR>f : G →* H<VAR>g : H →* K<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>G H K : Type u_1<VAR>AddCommGroup G<VAR>AddCommGroup H<VAR>AddCommGroup K<VAR>f : G →+ H<VAR>g : H →+ K<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>G : Type u_1<VAR>AddCommGroup G<GOAL>⇑(𝟙 (AddCommGrp.of G)) = id
<VAR>G : Type u_1<VAR>CommGroup G<GOAL>⇑(𝟙 (CommGrp.of G)) = id
<VAR>G H : AddCommGrp<VAR>g : ↑G<GOAL>0 g = 0
<VAR>G H : CommGrp<VAR>g : ↑G<GOAL>1 g = 1
<VAR>X Y : Type u_1<VAR>CommGroup X<VAR>CommGroup Y<VAR>f : X →* Y<VAR>x : X<GOAL>(CommGrp.ofHom f) x = f x
<VAR>X Y : Type u_1<VAR>AddCommGroup X<VAR>AddCommGroup Y<VAR>f : X →+ Y<VAR>x : X<GOAL>(AddCommGrp.ofHom f) x = f x
<VAR>X Y : CommGrp<VAR>f : X ⟶ Y<GOAL>CommGrp.uliftFunctor.map f = CommGrp.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp (MonoidHom.comp f MulEquiv.ulift.toMonoidHom))
<VAR>X : CommGrp<GOAL>CommGrp.uliftFunctor.obj X = CommGrp.of (ULift.{v, u} ↑X)
<VAR>X Y : AddCommGrp<VAR>f : X ⟶ Y<GOAL>AddCommGrp.uliftFunctor.map f = AddCommGrp.ofHom (AddEquiv.ulift.symm.toAddMonoidHom.comp (AddMonoidHom.comp f AddEquiv.ulift.toAddMonoidHom))
<VAR>X : AddCommGrp<GOAL>AddCommGrp.uliftFunctor.obj X = AddCommGrp.of (ULift.{v, u} ↑X)
<VAR>G : AddCommGrp<VAR>g : ↑G<VAR>i : ℤ<GOAL>(AddCommGrp.asHom g) i = i • g
<VAR>G : AddCommGrp<GOAL>Function.Injective AddCommGrp.asHom
<VAR>G : AddCommGrp<VAR>f g : AddCommGrp.of ℤ ⟶ G<VAR>w : f 1 = g 1<GOAL>f = g
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<VAR>CategoryTheory.Mono f<GOAL>Function.Injective ⇑f
<VAR>X Y : AddGrp<VAR>e : ↑X ≃+ ↑Y<GOAL>e.toAddGrpIso.hom = e.toAddMonoidHom
<VAR>X Y : Grp<VAR>e : ↑X ≃* ↑Y<GOAL>e.toGrpIso.inv = e.symm.toMonoidHom
<VAR>X Y : Grp<VAR>e : ↑X ≃* ↑Y<GOAL>e.toGrpIso.hom = e.toMonoidHom
<VAR>X Y : AddGrp<VAR>e : ↑X ≃+ ↑Y<GOAL>e.toAddGrpIso.inv = e.symm.toAddMonoidHom
<VAR>X Y : CommGrp<VAR>e : ↑X ≃* ↑Y<GOAL>e.toCommGrpIso.inv = e.symm.toMonoidHom
<VAR>X Y : AddCommGrp<VAR>e : ↑X ≃+ ↑Y<GOAL>e.toAddCommGrpIso.hom = e.toAddMonoidHom
<VAR>X Y : CommGrp<VAR>e : ↑X ≃* ↑Y<GOAL>e.toCommGrpIso.hom = e.toMonoidHom
<VAR>X Y : AddCommGrp<VAR>e : ↑X ≃+ ↑Y<GOAL>e.toAddCommGrpIso.inv = e.symm.toAddMonoidHom
<VAR>X Y : CommGrp<VAR>i : X ≅ Y<VAR>a : ↑Y<GOAL>i.commGroupIsoToMulEquiv.symm a = i.inv a
<VAR>X Y : CommGrp<VAR>i : X ≅ Y<VAR>a : ↑X<GOAL>i.commGroupIsoToMulEquiv a = i.hom a
<VAR>X Y : AddCommGrp<VAR>i : X ≅ Y<VAR>a : ↑Y<GOAL>i.addCommGroupIsoToAddEquiv.symm a = i.inv a
<VAR>X Y : AddCommGrp<VAR>i : X ≅ Y<VAR>a : ↑X<GOAL>i.addCommGroupIsoToAddEquiv a = i.hom a
<VAR>G : AddGrp<VAR>H : Type u<VAR>AddGroup H<VAR>f : ↑G →+ H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Grp<VAR>H : Type u<VAR>Group H<VAR>f : ↑G →* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>AddGroup G<VAR>H : AddGrp<VAR>f : G →+ ↑H<GOAL>AddMonoidHom.comp (𝟙 H) f = f
<VAR>G : Type u<VAR>Group G<VAR>H : Grp<VAR>f : G →* ↑H<GOAL>MonoidHom.comp (𝟙 H) f = f
<VAR>G : AddCommGrp<VAR>H : Type u<VAR>AddCommGroup H<VAR>f : ↑G →+ H<GOAL>f.comp (𝟙 G) = f
<VAR>G : CommGrp<VAR>H : Type u<VAR>CommGroup H<VAR>f : ↑G →* H<GOAL>f.comp (𝟙 G) = f
<VAR>G : Type u<VAR>CommGroup G<VAR>H : CommGrp<VAR>f : G →* ↑H<GOAL>MonoidHom.comp (𝟙 H) f = f
<VAR>G : Type u<VAR>AddCommGroup G<VAR>H : AddCommGrp<VAR>f : G →+ ↑H<GOAL>AddMonoidHom.comp (𝟙 H) f = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>self : M.Derivation φ<VAR>X : Cᵒᵖ<VAR>a : ↑(S.obj X)<GOAL>self.d ((φ.app X) a) = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>self : M.Derivation φ<VAR>X Y : Dᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ↑(R.obj X)<GOAL>self.d ((R.map f) x) = (M.map f) (self.d x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>self : M.Derivation φ<VAR>X : Dᵒᵖ<VAR>a b : ↑(R.obj X)<GOAL>self.d (a * b) = a • self.d b + b • self.d a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>d d' : M.Derivation φ<VAR>h : d = d'<VAR>X : Dᵒᵖ<VAR>b : ↑(R.obj X)<GOAL>d.d b = d'.d b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>d : M.Derivation φ<VAR>X : Dᵒᵖ<GOAL>d.d 1 = 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M N : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>d : M.Derivation φ<VAR>f : M ⟶ N<GOAL>∀ {X : Dᵒᵖ} (a : ↑(R.obj X)), (d.postcomp f).d a = (PresheafOfModules.Hom.app f X) (d.d a)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>d : M.Derivation φ<VAR>self : d.Universal<VAR>M' : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<GOAL>∀ (φ_1 φ' : M ⟶ M'), d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>d : M.Derivation φ<VAR>self : d.Universal<VAR>M' : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>d' : M'.Derivation φ<GOAL>d.postcomp (self.desc d') = d'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>R : Dᵒᵖ ⥤ CommRingCat<VAR>φ : S ⟶ F.op ⋙ R<VAR>self : PresheafOfModules.HasDifferentials φ<GOAL>∃ M d, Nonempty d.Universal
<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ' : S' ⟶ R<VAR>d : M.Derivation' φ'<VAR>X : Dᵒᵖ<VAR>a : ↑(S'.obj X)<GOAL>d.d ((φ'.app X) a) = 0
<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ' : S' ⟶ R<VAR>d : M.Derivation' φ'<VAR>X : Dᵒᵖ<VAR>b : ↑(R.obj X)<GOAL>(d.app X).d b = d.d b
<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>M : PresheafOfModules (R ⋙ CategoryTheory.forget₂ CommRingCat RingCat)<VAR>φ' : S' ⟶ R<VAR>d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)<VAR>d_map : ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(R.obj X)), (d Y).d ((R.map f) x) = (M.map f) ((d X).d x)<VAR>X : Dᵒᵖ<GOAL>(PresheafOfModules.Derivation'.mk d d_map).app X = d X
<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>φ' : S' ⟶ R<VAR>X : Dᵒᵖ<GOAL>(PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').obj X = CommRingCat.KaehlerDifferential (φ'.app X)
<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>φ' : S' ⟶ R<VAR>X Y : Dᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ↑(CommRingCat.KaehlerDifferential (φ'.app X))<GOAL>((PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f) x = (CommRingCat.KaehlerDifferential.map ⋯) x
<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>φ' : S' ⟶ R<VAR>X Y : Dᵒᵖ<VAR>f : X ⟶ Y<VAR>x : ↑(R.obj X)<GOAL>((PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f) (CommRingCat.KaehlerDifferential.d x) = CommRingCat.KaehlerDifferential.d ((R.map f) x)
<VAR>G : AddGrp<VAR>Subsingleton ↑G<GOAL>CategoryTheory.Limits.IsZero G
<VAR>G : Grp<VAR>Subsingleton ↑G<GOAL>CategoryTheory.Limits.IsZero G
<VAR>G : CommGrp<VAR>Subsingleton ↑G<GOAL>CategoryTheory.Limits.IsZero G
<VAR>G : AddCommGrp<VAR>Subsingleton ↑G<GOAL>CategoryTheory.Limits.IsZero G
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>N : ModuleCat R<GOAL>ModuleCat.MonoidalCategory.tensorHom (𝟙 M) (𝟙 N) = 𝟙 (ModuleCat.of R (TensorProduct R ↑M ↑N))
<VAR>R : Type u<VAR>CommRing R<VAR>X₁ Y₁ Z₁ : ModuleCat R<VAR>X₂ Y₂ Z₂ : ModuleCat R<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>ModuleCat.MonoidalCategory.tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = ModuleCat.MonoidalCategory.tensorHom f₁ f₂ ≫ ModuleCat.MonoidalCategory.tensorHom g₁ g₂
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<GOAL>CategoryTheory.MonoidalCategory.tensorObj M N = ModuleCat.MonoidalCategory.tensorObj M N
<VAR>R : Type u<VAR>CommRing R<GOAL>𝟙_ (ModuleCat R) = ModuleCat.of R R
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<GOAL>CategoryTheory.MonoidalCategory.rightUnitor M = ModuleCat.MonoidalCategory.rightUnitor M
<VAR>R : Type u<VAR>CommRing R<GOAL>∀ {X₁ Y₁ X₂ Y₂ : ModuleCat R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), CategoryTheory.MonoidalCategory.tensorHom f g = TensorProduct.map f g
<VAR>R : Type u<VAR>CommRing R<GOAL>∀ {X₁ X₂ : ModuleCat R} (f : X₁ ⟶ X₂) (N : ModuleCat R), CategoryTheory.MonoidalCategory.whiskerRight f N = ModuleCat.MonoidalCategory.whiskerRight f N
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>N₁ N₂ : ModuleCat R<VAR>f : N₁ ⟶ N₂<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft M f = ModuleCat.MonoidalCategory.whiskerLeft M f
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<GOAL>CategoryTheory.MonoidalCategory.leftUnitor M = ModuleCat.MonoidalCategory.leftUnitor M
<VAR>R : Type u<VAR>CommRing R<VAR>M N K : ModuleCat R<GOAL>CategoryTheory.MonoidalCategory.associator M N K = ModuleCat.MonoidalCategory.associator M N K
<VAR>R : Type u<VAR>CommRing R<VAR>X₁ : Type u_1<VAR>X₂ : Type u_2<VAR>X₃ : Type u_3<VAR>AddCommMonoid X₁<VAR>AddCommMonoid X₂<VAR>AddCommMonoid X₃<VAR>Module R X₁<VAR>Module R X₂<VAR>Module R X₃<VAR>Y₁ : Type u_4<VAR>Y₂ : Type u_5<VAR>Y₃ : Type u_6<VAR>AddCommMonoid Y₁<VAR>AddCommMonoid Y₂<VAR>AddCommMonoid Y₃<VAR>Module R Y₁<VAR>Module R Y₂<VAR>Module R Y₃<VAR>f₁ : X₁ →ₗ[R] Y₁<VAR>f₂ : X₂ →ₗ[R] Y₂<VAR>f₃ : X₃ →ₗ[R] Y₃<GOAL>↑(TensorProduct.assoc R Y₁ Y₂ Y₃) ∘ₗ TensorProduct.map (TensorProduct.map f₁ f₂) f₃ = TensorProduct.map f₁ (TensorProduct.map f₂ f₃) ∘ₗ ↑(TensorProduct.assoc R X₁ X₂ X₃)
<VAR>R : Type u<VAR>CommRing R<VAR>W : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>AddCommMonoid W<VAR>AddCommMonoid X<VAR>AddCommMonoid Y<VAR>AddCommMonoid Z<VAR>Module R W<VAR>Module R X<VAR>Module R Y<VAR>Module R Z<GOAL>(LinearMap.lTensor W ↑(TensorProduct.assoc R X Y Z) ∘ₗ ↑(TensorProduct.assoc R W (TensorProduct R X Y) Z)) ∘ₗ LinearMap.rTensor Z ↑(TensorProduct.assoc R W X Y) = ↑(TensorProduct.assoc R W X (TensorProduct R Y Z)) ∘ₗ ↑(TensorProduct.assoc R (TensorProduct R W X) Y Z)
<VAR>R : Type u<VAR>CommRing R<VAR>X₁ : ModuleCat R<VAR>X₂ : ModuleCat R<VAR>X₃ : ModuleCat R<VAR>Y₁ : ModuleCat R<VAR>Y₂ : ModuleCat R<VAR>Y₃ : ModuleCat R<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>f₃ : X₃ ⟶ Y₃<GOAL>ModuleCat.MonoidalCategory.tensorHom (ModuleCat.MonoidalCategory.tensorHom f₁ f₂) f₃ ≫ (ModuleCat.MonoidalCategory.associator Y₁ Y₂ Y₃).hom = (ModuleCat.MonoidalCategory.associator X₁ X₂ X₃).hom ≫ ModuleCat.MonoidalCategory.tensorHom f₁ (ModuleCat.MonoidalCategory.tensorHom f₂ f₃)
<VAR>R : Type u<VAR>CommRing R<VAR>W : ModuleCat R<VAR>X : ModuleCat R<VAR>Y : ModuleCat R<VAR>Z : ModuleCat R<GOAL>ModuleCat.MonoidalCategory.whiskerRight (ModuleCat.MonoidalCategory.associator W X Y).hom Z ≫ (ModuleCat.MonoidalCategory.associator W (ModuleCat.MonoidalCategory.tensorObj X Y) Z).hom ≫ ModuleCat.MonoidalCategory.whiskerLeft W (ModuleCat.MonoidalCategory.associator X Y Z).hom = (ModuleCat.MonoidalCategory.associator (ModuleCat.MonoidalCategory.tensorObj W X) Y Z).hom ≫ (ModuleCat.MonoidalCategory.associator W X (ModuleCat.MonoidalCategory.tensorObj Y Z)).hom
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>ModuleCat.MonoidalCategory.tensorHom (𝟙 (ModuleCat.of R R)) f ≫ (ModuleCat.MonoidalCategory.leftUnitor N).hom = (ModuleCat.MonoidalCategory.leftUnitor M).hom ≫ f
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<GOAL>ModuleCat.MonoidalCategory.tensorHom f (𝟙 (ModuleCat.of R R)) ≫ (ModuleCat.MonoidalCategory.rightUnitor N).hom = (ModuleCat.MonoidalCategory.rightUnitor M).hom ≫ f
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<GOAL>(ModuleCat.MonoidalCategory.associator M (ModuleCat.of R R) N).hom ≫ ModuleCat.MonoidalCategory.tensorHom (𝟙 M) (ModuleCat.MonoidalCategory.leftUnitor N).hom = ModuleCat.MonoidalCategory.tensorHom (ModuleCat.MonoidalCategory.rightUnitor M).hom (𝟙 N)
<VAR>R : Type u<VAR>CommRing R<VAR>K L M N : ModuleCat R<VAR>f : K ⟶ L<VAR>g : M ⟶ N<VAR>k : ↑K<VAR>m : ↑M<GOAL>(CategoryTheory.MonoidalCategory.tensorHom f g) (k ⊗ₜ[R] m) = f k ⊗ₜ[R] g m
<VAR>R : Type u<VAR>CommRing R<VAR>L : ModuleCat R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>l : ↑L<VAR>m : ↑M<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft L f) (l ⊗ₜ[R] m) = l ⊗ₜ[R] f m
<VAR>R : Type u<VAR>CommRing R<VAR>L M : ModuleCat R<VAR>f : L ⟶ M<VAR>N : ModuleCat R<VAR>l : ↑L<VAR>n : ↑N<GOAL>(CategoryTheory.MonoidalCategory.whiskerRight f N) (l ⊗ₜ[R] n) = f l ⊗ₜ[R] n
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>r : R<VAR>m : ↑M<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor M).hom (r ⊗ₜ[R] m) = r • m
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>m : ↑M<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor M).inv m = 1 ⊗ₜ[R] m
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>m : ↑M<VAR>r : R<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor M).hom (m ⊗ₜ[R] r) = r • m
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>m : ↑M<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor M).inv m = m ⊗ₜ[R] 1
<VAR>R : Type u<VAR>CommRing R<VAR>M N K : ModuleCat R<VAR>m : ↑M<VAR>n : ↑N<VAR>k : ↑K<GOAL>(CategoryTheory.MonoidalCategory.associator M N K).hom ((m ⊗ₜ[R] n) ⊗ₜ[R] k) = m ⊗ₜ[R] n ⊗ₜ[R] k
<VAR>R : Type u<VAR>CommRing R<VAR>M N K : ModuleCat R<VAR>m : ↑M<VAR>n : ↑N<VAR>k : ↑K<GOAL>(CategoryTheory.MonoidalCategory.associator M N K).inv (m ⊗ₜ[R] n ⊗ₜ[R] k) = (m ⊗ₜ[R] n) ⊗ₜ[R] k
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>v : ι → ↑S.X₁<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>Disjoint (Submodule.span R (Set.range (u ∘ Sum.inl))) (Submodule.span R (Set.range (u ∘ Sum.inr)))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : CategoryTheory.Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>LinearIndependent R u
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>w : ι' → ↑S.X₃<VAR>hw : LinearIndependent R w<GOAL>LinearIndependent R (Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w))
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>v : ι → ↑S.X₁<VAR>β : Type u_4<VAR>u : ι ⊕ β → ↑S.X₂<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<VAR>hv : ⊤ ≤ Submodule.span R (Set.range v)<VAR>hw : ⊤ ≤ Submodule.span R (Set.range (⇑S.g ∘ u ∘ Sum.inr))<GOAL>⊤ ≤ Submodule.span R (Set.range u)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>v : ι → ↑S.X₁<VAR>w : ι' → ↑S.X₃<VAR>hv : ⊤ ≤ Submodule.span R (Set.range v)<VAR>hw : ⊤ ≤ Submodule.span R (Set.range w)<VAR>hE : CategoryTheory.Epi S.g<GOAL>⊤ ≤ Submodule.span R (Set.range (Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w)))
<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS' : S.ShortExact<VAR>Module.Free R ↑S.X₁<VAR>Module.Free R ↑S.X₃<GOAL>Module.Free R ↑S.X₂
<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS' : S.ShortExact<VAR>Module.Free R ↑S.X₁<VAR>Module.Free R ↑S.X₃<VAR>StrongRankCondition R<GOAL>Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃
<VAR>R : Type u_3<VAR>Ring R<VAR>S : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hS' : S.ShortExact<VAR>n p : ℕ<VAR>Module.Free R ↑S.X₁<VAR>Module.Free R ↑S.X₃<VAR>Module.Finite R ↑S.X₁<VAR>Module.Finite R ↑S.X₃<VAR>hN : FiniteDimensional.finrank R ↑S.X₁ = n<VAR>hP : FiniteDimensional.finrank R ↑S.X₃ = p<VAR>StrongRankCondition R<GOAL>FiniteDimensional.finrank R ↑S.X₂ = n + p
<VAR>A : Type u<VAR>AddCommGroup A<VAR>DivisibleBy A ℤ<GOAL>Module.Baer ℤ A
<VAR>A : Type u<VAR>AddCommGroup A<GOAL>CategoryTheory.Injective (ModuleCat.mk A) ↔ CategoryTheory.Injective { α := A, str := inferInstance }
<VAR>X : GrpWithZero<GOAL>⇑(𝟙 X) = id
<VAR>X Y Z : GrpWithZero<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(f ≫ g) = ⇑g ∘ ⇑f
<VAR>X Y : GrpWithZero<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget GrpWithZero).map f = ⇑f
<VAR>α β : GrpWithZero<VAR>e : ↑α ≃* ↑β<GOAL>(GrpWithZero.Iso.mk e).inv = ↑e.symm
<VAR>α β : GrpWithZero<VAR>e : ↑α ≃* ↑β<GOAL>(GrpWithZero.Iso.mk e).hom = ↑e
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ Grp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : ∃ k f g, (F.map f) x.snd = (F.map g) y.snd<GOAL>Grp.FilteredColimits.G.mk F x = Grp.FilteredColimits.G.mk F y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ AddGrp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : ∃ k f g, (F.map f) x.snd = (F.map g) y.snd<GOAL>AddGrp.FilteredColimits.G.mk F x = AddGrp.FilteredColimits.G.mk F y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ Grp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : CategoryTheory.Limits.Types.FilteredColimit.Rel (F ⋙ CategoryTheory.forget Grp) x y<GOAL>Grp.FilteredColimits.colimitInvAux F x = Grp.FilteredColimits.colimitInvAux F y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ AddGrp<VAR>x y : (j : J) × ↑(F.obj j)<VAR>h : CategoryTheory.Limits.Types.FilteredColimit.Rel (F ⋙ CategoryTheory.forget AddGrp) x y<GOAL>AddGrp.FilteredColimits.colimitNegAux F x = AddGrp.FilteredColimits.colimitNegAux F y
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ Grp<VAR>x : (j : J) × ↑(F.obj j)<GOAL>(Grp.FilteredColimits.G.mk F x)⁻¹ = Grp.FilteredColimits.G.mk F ⟨x.fst, x.snd⁻¹⟩
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsFiltered J<VAR>F : J ⥤ AddGrp<VAR>x : (j : J) × ↑(F.obj j)<GOAL>-AddGrp.FilteredColimits.G.mk F x = AddGrp.FilteredColimits.G.mk F ⟨x.fst, -x.snd⟩
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<GOAL>AddCommGrp.factorThruImage f ≫ AddCommGrp.image.ι f = f
<VAR>G H : AddCommGrp<VAR>f : G ⟶ H<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>AddCommGrp.image.lift F' ≫ F'.m = AddCommGrp.image.ι f
<VAR>R : Type u<VAR>CommRing R<VAR>M N P : ModuleCat R<VAR>f : N ⟶ P<VAR>g : ↑(ModuleCat.of R (M ⟶ N))<GOAL>((CategoryTheory.ihom M).map f) g = g ≫ f
<VAR>R : Type u<VAR>CommRing R<VAR>M N P : ModuleCat R<VAR>f : CategoryTheory.MonoidalCategory.tensorObj M N ⟶ P<VAR>x : ↑M<VAR>y : ↑N<GOAL>((CategoryTheory.MonoidalClosed.curry f) y) x = f (x ⊗ₜ[R] y)
<VAR>R : Type u<VAR>CommRing R<VAR>M N P : ModuleCat R<VAR>f : N ⟶ (CategoryTheory.ihom M).obj P<VAR>x : ↑M<VAR>y : ↑N<GOAL>(CategoryTheory.MonoidalClosed.uncurry f) (x ⊗ₜ[R] y) = (f y) x
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<GOAL>(CategoryTheory.ihom.ev M).app N = (TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) LinearMap.id.flip
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<GOAL>(CategoryTheory.ihom.coev M).app N = (TensorProduct.mk R ↑(Opposite.unop (Opposite.op M)) ↑((𝟭 (ModuleCat R)).obj N)).flip
<VAR>R : Type u<VAR>CommRing R<VAR>M N : ModuleCat R<VAR>P : ModuleCat R<VAR>f : N ⟶ M<GOAL>(CategoryTheory.MonoidalClosed.pre f).app P = LinearMap.lcomp R (↑P) f
<VAR>R : Type u_1<VAR>Zero R<VAR>n : R<VAR>self : NeZero n<GOAL>n ≠ 0
<VAR>R : Type u_1<VAR>Zero R<VAR>n : R<VAR>h : NeZero n<GOAL>n ≠ 0
<VAR>R : Type u_1<VAR>Zero R<VAR>n : R<VAR>h : NeZero n<GOAL>0 ≠ n
<VAR>R : Type u_1<VAR>Zero R<VAR>n : R<GOAL>NeZero n ↔ n ≠ 0
<VAR>α : Type u_2<VAR>Zero α<GOAL>NeZero 0 ↔ False
<VAR>R : Type u_1<VAR>Zero R<VAR>n : R<GOAL>¬NeZero n ↔ n = 0
<VAR>R : Type u_1<VAR>Zero R<VAR>a : R<GOAL>a = 0 ∨ NeZero a
<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>NeZero 1<GOAL>0 ≠ 1
<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>NeZero 1<GOAL>1 ≠ 0
<VAR>α : Type u_2<VAR>Zero α<VAR>One α<VAR>NeZero 1<VAR>a : α<VAR>h : a = 1<GOAL>a ≠ 0
<VAR>α : Type u_2<VAR>Zero α<VAR>OfNat α 2<VAR>NeZero 2<GOAL>2 ≠ 0
<VAR>α : Type u_2<VAR>Zero α<VAR>OfNat α 3<VAR>NeZero 3<GOAL>3 ≠ 0
<VAR>α : Type u_2<VAR>Zero α<VAR>OfNat α 4<VAR>NeZero 4<GOAL>4 ≠ 0
<VAR>M : Type u_2<VAR>x : M<VAR>Preorder M<VAR>Zero M<VAR>h : 0 < x<GOAL>NeZero x
<VAR>n : ℕ<VAR>NeZero n<GOAL>0 < n
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ RingCat<GOAL>Quot.mk Setoid.r RingCat.Colimits.Prequotient.zero = 0
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ RingCat<GOAL>Quot.mk Setoid.r RingCat.Colimits.Prequotient.one = 1
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ RingCat<VAR>x : RingCat.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r x.neg = -Quot.mk Setoid.r x
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ RingCat<VAR>x y : RingCat.Colimits.Prequotient F<GOAL>Quot.mk Setoid.r (x.add y) = Quot.mk Setoid.r x + Quot.mk Setoid.r y