ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ K₁' : HomologicalComplex C₁ c₁<VAR>f : K₁ ⟶ K₁'<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>((((F.mapBifunctorHomologicalComplex c₁ c₂).map f).app K₂).f i₁).f i₂ = (F.map (f.f i₁)).app (K₂.X i₂)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<GOAL>((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>i₁ i₁' : I₁<VAR>i₂ : I₂<GOAL>((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ K₂' : HomologicalComplex C₂ c₂<VAR>φ : K₂ ⟶ K₂'<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_7, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_9, u_3} D<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Limits.HasZeroMorphisms D<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<GOAL>(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).toGradedObject = ((CategoryTheory.GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_9, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>K₁.HasMapBifunctor K₂ F c<VAR>DecidableEq J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>j : J<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = K₁.ιMapBifunctor K₂ F c i₁ i₂ j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_9, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ : HomologicalComplex C₁ c₁<VAR>K₂ : HomologicalComplex C₂ c₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>K₁.HasMapBifunctor K₂ F c<VAR>DecidableEq J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>j : J<VAR>h : c₁.π c₂ c (i₁, i₂) ≠ j<GOAL>K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = 0
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_9, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>CategoryTheory.Limits.HasZeroMorphisms C₁<VAR>CategoryTheory.Limits.HasZeroMorphisms C₂<VAR>CategoryTheory.Preadditive D<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₁ : K₁ ⟶ L₁<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.PreservesZeroMorphisms<VAR>∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>K₁.HasMapBifunctor K₂ F c<VAR>L₁.HasMapBifunctor L₂ F c<VAR>DecidableEq J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>j : J<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ (HomologicalComplex.mapBifunctorMap f₁ f₂ F c).f j = (F.map (f₁.f i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h
<VAR>M : Type uM<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>m : M<GOAL>↑n m = n • m
<VAR>M : Type uM<VAR>AddCommMonoid M<VAR>n : ℕ<VAR>n.AtLeastTwo<VAR>m : M<GOAL>(OfNat.ofNat n) m = n • m
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>x y : R<GOAL>(AddMonoidHom.mul x) y = x * y
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<GOAL>⇑AddMonoidHom.mul = AddMonoidHom.mulLeft
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<GOAL>⇑AddMonoidHom.mul.flip = AddMonoidHom.mulRight
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R →+ S<GOAL>(∀ (x y : R), f (x * y) = f x * f y) ↔ AddMonoidHom.mul.compr₂ f = (AddMonoidHom.mul.comp f).compl₂ f
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>a : R<GOAL>AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ↔ ∀ (b : R), Commute a b
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>b : R<GOAL>AddMonoidHom.mulRight b = AddMonoidHom.mulLeft b ↔ ∀ (a : R), Commute a b
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>r : R<GOAL>∀ (x : R), (AddMonoid.End.mulLeft r) x = r * x
<VAR>R : Type u_1<VAR>NonUnitalNonAssocSemiring R<VAR>y x : R<GOAL>(AddMonoid.End.mulRight y) x = x * y
<VAR>R : Type u_1<VAR>NonUnitalNonAssocCommSemiring R<GOAL>AddMonoid.End.mulRight = AddMonoid.End.mulLeft
<VAR>ι : Type u_1<VAR>S : Type u_3<VAR>R : Type u_4<VAR>Zero ι<VAR>CommSemiring S<VAR>Semiring R<VAR>Algebra S R<VAR>A : ι → Submodule S R<VAR>SetLike.GradedOne A<VAR>s : S<GOAL>(algebraMap S R) s ∈ A 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>Zero ι<VAR>AddMonoidWithOne R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>SetLike.GradedOne A<VAR>n : ℕ<GOAL>↑n ∈ A 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>Zero ι<VAR>AddGroupWithOne R<VAR>SetLike σ R<VAR>AddSubgroupClass σ R<VAR>A : ι → σ<VAR>SetLike.GradedOne A<VAR>z : ℤ<GOAL>↑z ∈ A 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>AddMonoid ι<VAR>SetLike.GradedMonoid A<VAR>i : ι<VAR>x : ↥(A i)<GOAL>(DirectSum.coeRingHom A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>AddMonoid ι<VAR>SetLike.GradedMonoid A<VAR>(i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)<VAR>r r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<GOAL>↑((r * r') n) = ∑ ij ∈ Finset.filter (fun ij => ij.1 + ij.2 = n) (DFinsupp.support r ×ˢ DFinsupp.support r'), ↑(r ij.1) * ↑(r' ij.2)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>AddMonoid ι<VAR>SetLike.GradedMonoid A<VAR>(i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)<VAR>r r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<GOAL>↑((r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>AddMonoid ι<VAR>SetLike.GradedMonoid A<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>j n : ι<VAR>H : ∀ (x : ι), i + x = n ↔ x = j<GOAL>↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' j)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>AddMonoid ι<VAR>SetLike.GradedMonoid A<VAR>r : ⨁ (i : ι), ↥(A i)<VAR>i : ι<VAR>r' : ↥(A i)<VAR>j n : ι<VAR>H : ∀ (x : ι), x + i = n ↔ x = j<GOAL>↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = ↑(r j) * ↑r'
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>AddLeftCancelMonoid ι<VAR>SetLike.GradedMonoid A<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>j : ι<GOAL>↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') (i + j)) = ↑r * ↑(r' j)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>AddRightCancelMonoid ι<VAR>SetLike.GradedMonoid A<VAR>r : ⨁ (i : ι), ↥(A i)<VAR>i : ι<VAR>r' : ↥(A i)<VAR>j : ι<GOAL>↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') (j + i)) = ↑(r j) * ↑r'
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike.GradedMonoid A<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<VAR>h : ¬i ≤ n<GOAL>↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike.GradedMonoid A<VAR>r : ⨁ (i : ι), ↥(A i)<VAR>i : ι<VAR>r' : ↥(A i)<VAR>n : ι<VAR>h : ¬i ≤ n<GOAL>↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike.GradedMonoid A<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>r : ⨁ (i : ι), ↥(A i)<VAR>i : ι<VAR>r' : ↥(A i)<VAR>n : ι<VAR>h : i ≤ n<GOAL>↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = ↑(r (n - i)) * ↑r'
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike.GradedMonoid A<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<VAR>h : i ≤ n<GOAL>↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = ↑r * ↑(r' (n - i))
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike.GradedMonoid A<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>r : ⨁ (i : ι), ↥(A i)<VAR>i : ι<VAR>r' : ↥(A i)<VAR>n : ι<VAR>Decidable (i ≤ n)<GOAL>↑((r * (DirectSum.of (fun i => ↥(A i)) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>Semiring R<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike.GradedMonoid A<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>i : ι<VAR>r : ↥(A i)<VAR>r' : ⨁ (i : ι), ↥(A i)<VAR>n : ι<VAR>Decidable (i ≤ n)<GOAL>↑(((DirectSum.of (fun i => ↥(A i)) i) r * r') n) = if i ≤ n then ↑r * ↑(r' (n - i)) else 0
<VAR>ι : Type u_1<VAR>S : Type u_3<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring S<VAR>Semiring R<VAR>Algebra S R<VAR>A : ι → Submodule S R<VAR>SetLike.GradedMonoid A<VAR>s : S<GOAL>↑(DirectSum.GAlgebra.toFun s) = (algebraMap S R) s
<VAR>ι : Type u_1<VAR>S : Type u_3<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring S<VAR>Semiring R<VAR>Algebra S R<VAR>A : ι → Submodule S R<VAR>SetLike.GradedMonoid A<GOAL>⨆ i, A i = Subalgebra.toSubmodule (DirectSum.coeAlgHom A).range
<VAR>ι : Type u_1<VAR>S : Type u_3<VAR>R : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring S<VAR>Semiring R<VAR>Algebra S R<VAR>A : ι → Submodule S R<VAR>SetLike.GradedMonoid A<VAR>i : ι<VAR>x : ↥(A i)<GOAL>(DirectSum.coeAlgHom A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>AddMonoid ι<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>SetLike.GradedMonoid A<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>Semiring R<VAR>AddMonoid ι<VAR>SetLike σ R<VAR>AddSubmonoidClass σ R<VAR>A : ι → σ<VAR>SetLike.GradedMonoid A<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>↑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_4<VAR>Ring R<VAR>AddMonoid ι<VAR>SetLike σ R<VAR>AddSubgroupClass σ R<VAR>A : ι → σ<VAR>SetLike.GradedMonoid A<VAR>z : ℤ<GOAL>↑↑z = ↑z
<VAR>ι : Type u_1<VAR>S : Type u_3<VAR>R : Type u_4<VAR>CommSemiring S<VAR>Semiring R<VAR>Algebra S R<VAR>AddMonoid ι<VAR>A : ι → Submodule S R<VAR>SetLike.GradedMonoid A<VAR>s : S<GOAL>↑((algebraMap S ↥(A 0)) s) = (algebraMap S R) s
<VAR>ι : Type u_1<VAR>S : Type u_3<VAR>R : Type u_4<VAR>Zero ι<VAR>Semiring S<VAR>AddCommMonoid R<VAR>Module S R<VAR>A : ι → Submodule S R<GOAL>SetLike.Homogeneous A 0
<VAR>ι : Type u_1<VAR>S : Type u_3<VAR>R : Type u_4<VAR>CommSemiring S<VAR>Semiring R<VAR>Algebra S R<VAR>A : ι → Submodule S R<VAR>s : S<VAR>r : R<VAR>hr : SetLike.Homogeneous A r<GOAL>SetLike.Homogeneous A (s • r)
<VAR>M : Type uM<VAR>AddCommMonoid M<VAR>m : M<GOAL>0 m = 0
<VAR>M : Type uM<VAR>AddCommMonoid M<VAR>m : M<GOAL>1 m = m
<VAR>M : Type uM<VAR>AddCommGroup M<VAR>z : ℤ<VAR>m : M<GOAL>↑z m = z • m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>f : M →+ N<VAR>n : ℕ<VAR>x : M<GOAL>(n • f) x = n • f x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>MulOneClass M<VAR>CommMonoid N<VAR>f : M →* N<VAR>n : ℕ<VAR>x : M<GOAL>(f ^ n) x = f x ^ n
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} {f g : M →+ N →+ P}, f = g ↔ ∀ (x_3 : M) (y : N), (f x_3) y = (g x_3) y
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} {f g : M →* N →* P}, f = g ↔ ∀ (x_3 : M) (y : N), (f x_3) y = (g x_3) y
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (x_3 : M) (y : N), (f.flip y) x_3 = (f x_3) y
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (x_3 : M) (y : N), (f.flip y) x_3 = (f x_3) y
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (n : N), (f 0) n = 0
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (n : N), (f 1) n = 1
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (m₁ m₂ : M) (n : N), (f (m₁ * m₂)) n = (f m₁) n * (f m₂) n
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), (f (m₁ + m₂)) n = (f m₁) n + (f m₂) n
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : Group M} {x_1 : MulOneClass N} {x_2 : CommGroup P} (f : M →* N →* P) (m : M) (n : N), (f m⁻¹) n = ((f m) n)⁻¹
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P} (f : M →+ N →+ P) (m : M) (n : N), (f (-m)) n = -(f m) n
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), (f (m₁ - m₂)) n = (f m₁) n - (f m₂) n
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : Group M} {x_1 : MulOneClass N} {x_2 : CommGroup P} (f : M →* N →* P) (m₁ m₂ : M) (n : N), (f (m₁ / m₂)) n = (f m₁) n / (f m₂) n
<VAR>M : Type uM<VAR>N : Type uN<VAR>MulOneClass M<VAR>CommMonoid N<VAR>y : M<VAR>x : M →* N<GOAL>(MonoidHom.eval y) x = x y
<VAR>M : Type uM<VAR>N : Type uN<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>y : M<VAR>x : M →+ N<GOAL>(AddMonoidHom.eval y) x = x y
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>f : M →* N<VAR>y : N →* P<VAR>x : M<GOAL>(f.compHom' y) x = y (f x)
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>f : M →+ N<VAR>y : N →+ P<VAR>x : M<GOAL>(f.compHom' y) x = y (f x)
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>g : N →+ P<VAR>hmn : M →+ N<GOAL>(AddMonoidHom.compHom g) hmn = g.comp hmn
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>MulOneClass M<VAR>CommMonoid N<VAR>CommMonoid P<VAR>g : N →* P<VAR>hmn : M →* N<GOAL>(MonoidHom.compHom g) hmn = g.comp hmn
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P), MonoidHom.flipHom f = f.flip
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<GOAL>∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P), AddMonoidHom.flipHom f = f.flip
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>AddZeroClass Q<VAR>f : M →+ N →+ P<VAR>g : Q →+ N<VAR>m : M<VAR>q : Q<GOAL>((f.compl₂ g) m) q = (f m) (g q)
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>MulOneClass Q<VAR>f : M →* N →* P<VAR>g : Q →* N<VAR>m : M<VAR>q : Q<GOAL>((f.compl₂ g) m) q = (f m) (g q)
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>AddZeroClass M<VAR>AddZeroClass N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>f : M →+ N →+ P<VAR>g : P →+ Q<VAR>m : M<VAR>n : N<GOAL>((f.compr₂ g) m) n = g ((f m) n)
<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>MulOneClass M<VAR>MulOneClass N<VAR>CommMonoid P<VAR>CommMonoid Q<VAR>f : M →* N →* P<VAR>g : P →* Q<VAR>m : M<VAR>n : N<GOAL>((f.compr₂ g) m) n = g ((f m) n)
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Subsemigroup M<GOAL>↑(Subsemigroup.toAddSubsemigroup S) = ⇑Additive.toMul ⁻¹' ↑S
<VAR>M : Type u_1<VAR>Mul M<VAR>S : AddSubsemigroup (Additive M)<GOAL>↑((RelIso.symm Subsemigroup.toAddSubsemigroup) S) = ⇑Additive.ofMul ⁻¹' ↑S
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set M<GOAL>Subsemigroup.toAddSubsemigroup (Subsemigroup.closure S) = AddSubsemigroup.closure (⇑Additive.toMul ⁻¹' S)
<VAR>M : Type u_1<VAR>Mul M<VAR>S : Set (Additive M)<GOAL>AddSubsemigroup.toSubsemigroup' (AddSubsemigroup.closure S) = Subsemigroup.closure (⇑Additive.ofMul ⁻¹' S)
<VAR>A : Type u_5<VAR>Add A<VAR>S : AddSubsemigroup A<GOAL>↑(AddSubsemigroup.toSubsemigroup S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
<VAR>A : Type u_5<VAR>Add A<VAR>S : Subsemigroup (Multiplicative A)<GOAL>↑((RelIso.symm AddSubsemigroup.toSubsemigroup) S) = ⇑Multiplicative.ofAdd ⁻¹' ↑S
<VAR>A : Type u_5<VAR>Add A<VAR>S : Set A<GOAL>AddSubsemigroup.toSubsemigroup (AddSubsemigroup.closure S) = Subsemigroup.closure (⇑Multiplicative.toAdd ⁻¹' S)
<VAR>A : Type u_5<VAR>Add A<VAR>S : Set (Multiplicative A)<GOAL>Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) = AddSubsemigroup.closure (⇑Multiplicative.ofAdd ⁻¹' S)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup N<VAR>f : AddHom M N<GOAL>↑(AddSubsemigroup.comap f S) = ⇑f ⁻¹' ↑S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup N<VAR>f : M →ₙ* N<GOAL>↑(Subsemigroup.comap f S) = ⇑f ⁻¹' ↑S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>S : Subsemigroup N<VAR>f : M →ₙ* N<VAR>x : M<GOAL>x ∈ Subsemigroup.comap f S ↔ f x ∈ S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>S : AddSubsemigroup N<VAR>f : AddHom M N<VAR>x : M<GOAL>x ∈ AddSubsemigroup.comap f S ↔ f x ∈ S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Add M<VAR>Add N<VAR>Add P<VAR>S : AddSubsemigroup P<VAR>g : AddHom N P<VAR>f : AddHom M N<GOAL>AddSubsemigroup.comap f (AddSubsemigroup.comap g S) = AddSubsemigroup.comap (g.comp f) S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Mul M<VAR>Mul N<VAR>Mul P<VAR>S : Subsemigroup P<VAR>g : N →ₙ* P<VAR>f : M →ₙ* N<GOAL>Subsemigroup.comap f (Subsemigroup.comap g S) = Subsemigroup.comap (g.comp f) S
<VAR>P : Type u_3<VAR>Mul P<VAR>S : Subsemigroup P<GOAL>Subsemigroup.comap (MulHom.id P) S = S
<VAR>P : Type u_3<VAR>Add P<VAR>S : AddSubsemigroup P<GOAL>AddSubsemigroup.comap (AddHom.id P) S = S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup M<GOAL>↑(Subsemigroup.map f S) = ⇑f '' ↑S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>S : AddSubsemigroup M<GOAL>↑(AddSubsemigroup.map f S) = ⇑f '' ↑S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup M<VAR>y : N<GOAL>y ∈ Subsemigroup.map f S ↔ ∃ x ∈ S, f x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>S : AddSubsemigroup M<VAR>y : N<GOAL>y ∈ AddSubsemigroup.map f S ↔ ∃ x ∈ S, f x = y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup M<VAR>x : M<VAR>hx : x ∈ S<GOAL>f x ∈ Subsemigroup.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>S : AddSubsemigroup M<VAR>x : M<VAR>hx : x ∈ S<GOAL>f x ∈ AddSubsemigroup.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Mul M<VAR>Mul N<VAR>f : M →ₙ* N<VAR>S : Subsemigroup M<VAR>x : ↥S<GOAL>f ↑x ∈ Subsemigroup.map f S
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>Add M<VAR>Add N<VAR>f : AddHom M N<VAR>S : AddSubsemigroup M<VAR>x : ↥S<GOAL>f ↑x ∈ AddSubsemigroup.map f S