ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Add α<VAR>Mul α<VAR>Add β<VAR>Mul β<VAR>f : αᵐᵒᵖ ≃+* βᵐᵒᵖ<GOAL>∀ (a : α), (RingEquiv.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>Add α<VAR>Mul α<VAR>Add β<VAR>Mul β<VAR>f : α ≃+* β<GOAL>∀ (a : αᵐᵒᵖ), (RingEquiv.op f) a = MulOpposite.op (f (MulOpposite.unop a))
<VAR>R : Type u_7<VAR>Add R<VAR>Mul R<GOAL>∀ (a : R), (RingEquiv.opOp R) a = MulOpposite.op (MulOpposite.op a)
<VAR>R : Type u_7<VAR>Add R<VAR>Mul R<GOAL>∀ (a : Rᵐᵒᵖᵐᵒᵖ), (RingEquiv.opOp R).symm a = MulOpposite.unop (MulOpposite.unop a)
<VAR>R : Type u_4<VAR>NonUnitalCommSemiring R<VAR>r : R<GOAL>(RingEquiv.toOpposite R) r = MulOpposite.op r
<VAR>R : Type u_4<VAR>NonUnitalCommSemiring R<VAR>r : Rᵐᵒᵖ<GOAL>(RingEquiv.toOpposite R).symm r = MulOpposite.unop r
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<GOAL>f 0 = 0
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<VAR>x : R<GOAL>f x = 0 ↔ x = 0
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<VAR>x : R<GOAL>f x ≠ 0 ↔ x ≠ 0
<VAR>F : Type u_1<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>hf : Function.Bijective ⇑f<GOAL>⇑(RingEquiv.ofBijective f hf) = ⇑f
<VAR>F : Type u_1<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>x : R<GOAL>(RingEquiv.ofBijective f hf) x = f x
<VAR>ι : Type u_7<VAR>R : ι → Type u_8<VAR>S : ι → Type u_9<VAR>(i : ι) → NonUnitalNonAssocSemiring (R i)<VAR>(i : ι) → NonUnitalNonAssocSemiring (S i)<VAR>e : (i : ι) → R i ≃+* S i<VAR>x : (i : ι) → R i<VAR>j : ι<GOAL>(RingEquiv.piCongrRight e) x j = (e j) (x j)
<VAR>ι : Type u_7<VAR>R : ι → Type u_8<VAR>(i : ι) → NonUnitalNonAssocSemiring (R i)<GOAL>(RingEquiv.piCongrRight fun i => RingEquiv.refl (R i)) = RingEquiv.refl ((i : ι) → R i)
<VAR>ι : Type u_7<VAR>R : ι → Type u_8<VAR>S : ι → Type u_9<VAR>(i : ι) → NonUnitalNonAssocSemiring (R i)<VAR>(i : ι) → NonUnitalNonAssocSemiring (S i)<VAR>e : (i : ι) → R i ≃+* S i<GOAL>(RingEquiv.piCongrRight e).symm = RingEquiv.piCongrRight fun i => (e i).symm
<VAR>ι : Type u_7<VAR>R : ι → Type u_8<VAR>S : ι → Type u_9<VAR>T : ι → Type u_10<VAR>(i : ι) → NonUnitalNonAssocSemiring (R i)<VAR>(i : ι) → NonUnitalNonAssocSemiring (S i)<VAR>(i : ι) → NonUnitalNonAssocSemiring (T i)<VAR>e : (i : ι) → R i ≃+* S i<VAR>f : (i : ι) → S i ≃+* T i<GOAL>(RingEquiv.piCongrRight e).trans (RingEquiv.piCongrRight f) = RingEquiv.piCongrRight fun i => (e i).trans (f i)
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<GOAL>f 1 = 1
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<VAR>x : R<GOAL>f x = 1 ↔ x = 1
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<VAR>x : R<GOAL>f x ≠ 1 ↔ x ≠ 1
<VAR>R : Type u_4<VAR>NonAssocSemiring R<GOAL>↑(RingEquiv.refl R) = MonoidHom.id R
<VAR>R : Type u_4<VAR>NonAssocSemiring R<GOAL>↑(RingEquiv.refl R) = AddMonoidHom.id R
<VAR>R : Type u_4<VAR>NonAssocSemiring R<GOAL>↑(RingEquiv.refl R) = RingHom.id R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<GOAL>↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<GOAL>(↑e).comp ↑e.symm = RingHom.id S
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<GOAL>(↑e.symm).comp ↑e = RingHom.id R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R ≃+* S<VAR>x : R<GOAL>f (-x) = -f x
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R ≃+* S<VAR>x y : R<GOAL>f (x - y) = f x - f y
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocRing R<VAR>NonAssocRing S<VAR>f : R ≃+* S<GOAL>f (-1) = -1
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocRing R<VAR>NonAssocRing S<VAR>f : R ≃+* S<VAR>x : R<GOAL>f x = -1 ↔ x = -1
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<GOAL>Function.Injective RingEquiv.toNonUnitalRingHom
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<GOAL>f.toNonUnitalRingHom = ↑f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_7<VAR>S : Type u_8<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f g : R ≃+* S<GOAL>f = g ↔ ↑f = ↑g
<VAR>R : Type u_4<VAR>NonUnitalNonAssocSemiring R<GOAL>(RingEquiv.refl R).toNonUnitalRingHom = NonUnitalRingHom.id R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>e : R ≃+* S<VAR>y : S<GOAL>e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>e : R ≃+* S<VAR>x : R<GOAL>e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>NonUnitalNonAssocSemiring S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<GOAL>(e₁.trans e₂).toNonUnitalRingHom = e₂.toNonUnitalRingHom.comp e₁.toNonUnitalRingHom
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>e : R ≃+* S<GOAL>e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>e : R ≃+* S<GOAL>e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>Function.Injective RingEquiv.toRingHom
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<GOAL>f.toRingHom = ↑f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_7<VAR>S : Type u_8<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f g : R ≃+* S<GOAL>f = g ↔ ↑f = ↑g
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<GOAL>↑↑f = ↑f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<GOAL>(↑f).toAddMonoidHom = (↑f).toAddMonoidHom
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<GOAL>↑↑f = (↑f).toMonoidHom
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<GOAL>(↑f).toEquiv = (↑f).toEquiv
<VAR>R : Type u_4<VAR>NonAssocSemiring R<GOAL>(RingEquiv.refl R).toRingHom = RingHom.id R
<VAR>R : Type u_4<VAR>NonAssocSemiring R<GOAL>(RingEquiv.refl R).toMonoidHom = MonoidHom.id R
<VAR>R : Type u_4<VAR>NonAssocSemiring R<GOAL>(RingEquiv.refl R).toAddMonoidHom = AddMonoidHom.id R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<VAR>y : S<GOAL>e.toRingHom (e.symm.toRingHom y) = y
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<VAR>x : R<GOAL>e.symm.toRingHom (e.toRingHom x) = x
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring S'<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* S'<GOAL>(e₁.trans e₂).toRingHom = e₂.toRingHom.comp e₁.toRingHom
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<GOAL>e.toRingHom.comp e.symm.toRingHom = RingHom.id S
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<GOAL>e.symm.toRingHom.comp e.toRingHom = RingHom.id R
<VAR>R : Type u_7<VAR>S : Type u_8<VAR>F : Type u_9<VAR>G : Type u_10<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>FunLike F R S<VAR>FunLike G S R<VAR>NonUnitalRingHomClass F R S<VAR>NonUnitalRingHomClass G S R<VAR>hom : F<VAR>inv : G<VAR>hom_inv_id : (↑inv).comp ↑hom = NonUnitalRingHom.id R<VAR>inv_hom_id : (↑hom).comp ↑inv = NonUnitalRingHom.id S<VAR>a : R<GOAL>(RingEquiv.ofHomInv' hom inv hom_inv_id inv_hom_id) a = hom a
<VAR>R : Type u_7<VAR>S : Type u_8<VAR>F : Type u_9<VAR>G : Type u_10<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>FunLike F R S<VAR>FunLike G S R<VAR>NonUnitalRingHomClass F R S<VAR>NonUnitalRingHomClass G S R<VAR>hom : F<VAR>inv : G<VAR>hom_inv_id : (↑inv).comp ↑hom = NonUnitalRingHom.id R<VAR>inv_hom_id : (↑hom).comp ↑inv = NonUnitalRingHom.id S<VAR>a : S<GOAL>(RingEquiv.ofHomInv' hom inv hom_inv_id inv_hom_id).symm a = inv a
<VAR>R : Type u_7<VAR>S : Type u_8<VAR>F : Type u_9<VAR>G : Type u_10<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>FunLike F R S<VAR>FunLike G S R<VAR>RingHomClass F R S<VAR>RingHomClass G S R<VAR>hom : F<VAR>inv : G<VAR>hom_inv_id : (↑inv).comp ↑hom = RingHom.id R<VAR>inv_hom_id : (↑hom).comp ↑inv = RingHom.id S<VAR>a : S<GOAL>(RingEquiv.ofHomInv hom inv hom_inv_id inv_hom_id).symm a = inv a
<VAR>R : Type u_7<VAR>S : Type u_8<VAR>F : Type u_9<VAR>G : Type u_10<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>FunLike F R S<VAR>FunLike G S R<VAR>RingHomClass F R S<VAR>RingHomClass G S R<VAR>hom : F<VAR>inv : G<VAR>hom_inv_id : (↑inv).comp ↑hom = RingHom.id R<VAR>inv_hom_id : (↑hom).comp ↑inv = RingHom.id S<VAR>a : R<GOAL>(RingEquiv.ofHomInv hom inv hom_inv_id inv_hom_id) a = hom a
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Semiring R<VAR>Semiring S<VAR>f : R ≃+* S<VAR>a : R<VAR>n : ℕ<GOAL>f (a ^ n) = f a ^ n
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Semiring R<VAR>Semiring S<VAR>f : R ≃+* S<VAR>a : R<GOAL>IsUnit (f a) ↔ IsUnit a
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Add R<VAR>Add S<VAR>Mul R<VAR>Mul S<VAR>e : R ≃+* S<GOAL>e.trans e.symm = RingEquiv.refl R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>Add R<VAR>Add S<VAR>Mul R<VAR>Mul S<VAR>e : R ≃+* S<GOAL>e.symm.trans e = RingEquiv.refl S
<VAR>A : Type u_7<VAR>B : Type u_8<VAR>MulZeroClass A<VAR>MulZeroClass B<VAR>NoZeroDivisors B<VAR>e : A ≃* B<GOAL>NoZeroDivisors A
<VAR>A : Type u_7<VAR>B : Type u_8<VAR>Semiring A<VAR>Semiring B<VAR>IsDomain B<VAR>e : A ≃* B<GOAL>IsDomain A
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>g : G<VAR>x : AddMonoidAlgebra k G<VAR>g' : G<GOAL>(x.divOf g) g' = x (g + g')
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>g : G<VAR>x : AddMonoidAlgebra k G<GOAL>(x.divOf g).support = x.support.preimage (fun x => g + x) ⋯
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>g : G<GOAL>AddMonoidAlgebra.divOf 0 g = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<GOAL>x.divOf 0 = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x y : AddMonoidAlgebra k G<VAR>g : G<GOAL>(x + y).divOf g = x.divOf g + y.divOf g
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>a b : G<GOAL>x.divOf (a + b) = (x.divOf a).divOf b
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>g : Multiplicative G<VAR>x : AddMonoidAlgebra k G<GOAL>(AddMonoidAlgebra.divOfHom g) x = x.divOf (Multiplicative.toAdd g)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>a : G<VAR>x : AddMonoidAlgebra k G<GOAL>(AddMonoidAlgebra.of' k G a * x).divOf a = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>a : G<GOAL>(x * AddMonoidAlgebra.of' k G a).divOf a = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>a : G<GOAL>(AddMonoidAlgebra.of' k G a).divOf a = 1
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g g' : G<VAR>h : ¬∃ d, g' = g + d<GOAL>(x.modOf g) g' = x g'
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g g' : G<VAR>h : ∃ d, g' = g + d<GOAL>(x.modOf g) g' = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g d : G<GOAL>(x.modOf g) (d + g) = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g d : G<GOAL>(x.modOf g) (g + d) = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>g : G<VAR>x : AddMonoidAlgebra k G<GOAL>(AddMonoidAlgebra.of' k G g * x).modOf g = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g : G<GOAL>(x * AddMonoidAlgebra.of' k G g).modOf g = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>g : G<GOAL>(AddMonoidAlgebra.of' k G g).modOf g = 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g : G<GOAL>AddMonoidAlgebra.of' k G g * x.divOf g + x.modOf g = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g : G<GOAL>x.modOf g + AddMonoidAlgebra.of' k G g * x.divOf g = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>Semiring k<VAR>AddCancelCommMonoid G<VAR>x : AddMonoidAlgebra k G<VAR>g : G<GOAL>AddMonoidAlgebra.of' k G g ∣ x ↔ x.modOf g = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>i : ι<VAR>m : M<GOAL>AddMonoidAlgebra.toDirectSum (Finsupp.single i m) = (DirectSum.of (fun i => M) i) m
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>i : ι<VAR>m : M<GOAL>((DirectSum.of (fun x => M) i) m).toAddMonoidAlgebra = Finsupp.single i m
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : AddMonoidAlgebra M ι<GOAL>f.toDirectSum.toAddMonoidAlgebra = f
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : ⨁ (x : ι), M<GOAL>f.toAddMonoidAlgebra.toDirectSum = f
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Semiring M<GOAL>AddMonoidAlgebra.toDirectSum 0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Semiring M<VAR>f g : AddMonoidAlgebra M ι<GOAL>(f + g).toDirectSum = f.toDirectSum + g.toDirectSum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring M<VAR>f g : AddMonoidAlgebra M ι<GOAL>(f * g).toDirectSum = f.toDirectSum * g.toDirectSum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>DirectSum.toAddMonoidAlgebra 0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f g : ⨁ (x : ι), M<GOAL>(f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f g : ⨁ (x : ι), M<GOAL>(f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraEquivDirectSum = AddMonoidAlgebra.toDirectSum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraAddEquivDirectSum = AddMonoidAlgebra.toDirectSum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraAddEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraRingEquivDirectSum = AddMonoidAlgebra.toDirectSum
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraRingEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>(m : A) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraAlgEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>(m : A) → Decidable (m ≠ 0)<GOAL>⇑addMonoidAlgebraAlgEquivDirectSum = AddMonoidAlgebra.toDirectSum
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R ≃+* S<VAR>l : List R<GOAL>f l.prod = (List.map (⇑f) l).prod
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<VAR>l : List R<GOAL>f l.sum = (List.map (⇑f) l).sum
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>f : R ≃+* Sᵐᵒᵖ<VAR>l : List R<GOAL>MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommSemiring R<VAR>CommSemiring S<VAR>f : R ≃+* S<VAR>s : Multiset R<GOAL>f s.prod = (Multiset.map (⇑f) s).prod
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<VAR>s : Multiset R<GOAL>f s.sum = (Multiset.map (⇑f) s).sum
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommSemiring R<VAR>CommSemiring S<VAR>g : R ≃+* S<VAR>f : α → R<VAR>s : Finset α<GOAL>g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>g : R ≃+* S<VAR>f : α → R<VAR>s : Finset α<GOAL>g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : Option α → M<VAR>s : Finset α<GOAL>∏ x ∈ Finset.insertNone s, f x = f none * ∏ x ∈ s, f (some x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : Option α → M<VAR>s : Finset α<GOAL>∑ x ∈ Finset.insertNone s, f x = f none + ∑ x ∈ s, f (some x)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → M<VAR>x : M<VAR>s : Finset α<GOAL>x + ∑ i ∈ s, f i = ∑ i ∈ Finset.insertNone s, i.elim x f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : α → M<VAR>x : M<VAR>s : Finset α<GOAL>x * ∏ i ∈ s, f i = ∏ i ∈ Finset.insertNone s, i.elim x f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Finset (Option α)<GOAL>∏ x ∈ Finset.eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Finset (Option α)<GOAL>∑ x ∈ Finset.eraseNone s, f x = ∑ x ∈ s, Option.elim' 0 f x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>(a : α) → Monoid (β a)<VAR>a : α<VAR>l : List ((a : α) → β a)<GOAL>l.prod a = (List.map (fun f => f a) l).prod
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>(a : α) → AddMonoid (β a)<VAR>a : α<VAR>l : List ((a : α) → β a)<GOAL>l.sum a = (List.map (fun f => f a) l).sum
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>(a : α) → AddCommMonoid (β a)<VAR>a : α<VAR>s : Multiset ((a : α) → β a)<GOAL>s.sum a = (Multiset.map (fun f => f a) s).sum
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>(a : α) → CommMonoid (β a)<VAR>a : α<VAR>s : Multiset ((a : α) → β a)<GOAL>s.prod a = (Multiset.map (fun f => f a) s).prod
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>(a : α) → AddCommMonoid (β a)<VAR>a : α<VAR>s : Finset γ<VAR>g : γ → (a : α) → β a<GOAL>(∑ c ∈ s, g c) a = ∑ c ∈ s, g c a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>(a : α) → CommMonoid (β a)<VAR>a : α<VAR>s : Finset γ<VAR>g : γ → (a : α) → β a<GOAL>(∏ c ∈ s, g c) a = ∏ c ∈ s, g c a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>(a : α) → AddCommMonoid (β a)<VAR>s : Finset γ<VAR>g : γ → (a : α) → β a<GOAL>∑ c ∈ s, g c = fun a => ∑ c ∈ s, g c a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>(a : α) → CommMonoid (β a)<VAR>s : Finset γ<VAR>g : γ → (a : α) → β a<GOAL>∏ c ∈ s, g c = fun a => ∏ c ∈ s, g c a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>Fintype γ<VAR>(a : α) → CommMonoid (β a)<VAR>a : α<VAR>g : γ → (a : α) → β a<GOAL>(∏ c : γ, g c) a = ∏ c : γ, g c a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>Fintype γ<VAR>(a : α) → AddCommMonoid (β a)<VAR>a : α<VAR>g : γ → (a : α) → β a<GOAL>(∑ c : γ, g c) a = ∑ c : γ, g c a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Finset γ<VAR>f : γ → α<VAR>g : γ → β<GOAL>(∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>f : γ → α<VAR>g : γ → β<GOAL>(∑ x ∈ s, f x, ∑ x ∈ s, g x) = ∑ x ∈ s, (f x, g x)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>DecidableEq ι<VAR>R : Type u_2<VAR>Semiring R<VAR>x : ι → R<GOAL>x = ∑ i : ι, x i • fun j => if i = j then 1 else 0
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>Z : I → Type u_2<VAR>(i : I) → CommMonoid (Z i)<VAR>Fintype I<VAR>f : (i : I) → Z i<GOAL>∏ i : I, Pi.mulSingle i (f i) = f
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>Z : I → Type u_2<VAR>(i : I) → AddCommMonoid (Z i)<VAR>Fintype I<VAR>f : (i : I) → Z i<GOAL>∑ i : I, Pi.single i (f i) = f
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>Z : I → Type u_2<VAR>(i : I) → CommMonoid (Z i)<VAR>Finite I<VAR>G : Type u_3<VAR>CommMonoid G<VAR>g h : ((i : I) → Z i) →* G<VAR>H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)<GOAL>g = h
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>Z : I → Type u_2<VAR>(i : I) → AddCommMonoid (Z i)<VAR>Finite I<VAR>G : Type u_3<VAR>AddCommMonoid G<VAR>g h : ((i : I) → Z i) →+ G<VAR>H : ∀ (i : I) (x : Z i), g (Pi.single i x) = h (Pi.single i x)<GOAL>g = h
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>Z : I → Type u_2<VAR>(i : I) → AddCommMonoid (Z i)<VAR>Finite I<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>g h : ((i : I) → Z i) →+ M<VAR>H : ∀ (i : I), g.comp (AddMonoidHom.single Z i) = h.comp (AddMonoidHom.single Z i)<GOAL>g = h
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>Z : I → Type u_2<VAR>(i : I) → CommMonoid (Z i)<VAR>Finite I<VAR>M : Type u_3<VAR>CommMonoid M<VAR>g h : ((i : I) → Z i) →* M<VAR>H : ∀ (i : I), g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)<GOAL>g = h
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>f : I → Type u_2<VAR>(i : I) → NonAssocSemiring (f i)<VAR>Finite I<VAR>G : Type u_3<VAR>NonAssocSemiring G<VAR>g h : ((i : I) → f i) →+* G<VAR>H : ∀ (i : I) (x : f i), g (Pi.single i x) = h (Pi.single i x)<GOAL>g = h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>f : γ → α × β<GOAL>(∑ c ∈ s, f c).1 = ∑ c ∈ s, (f c).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Finset γ<VAR>f : γ → α × β<GOAL>(∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Finset γ<VAR>f : γ → α × β<GOAL>(∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Finset γ<VAR>f : γ → α × β<GOAL>(∑ c ∈ s, f c).2 = ∑ c ∈ s, (f c).2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>s : Finset ι<VAR>f : ι → WithTop α<GOAL>∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>LT α<VAR>s : Finset ι<VAR>f : ι → WithTop α<GOAL>∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>LT α<VAR>s : Finset ι<VAR>f : ι → WithTop α<VAR>h : ∀ i ∈ s, f i ≠ ⊤<GOAL>∑ i ∈ s, f i < ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoidWithZero α<VAR>NoZeroDivisors α<VAR>Nontrivial α<VAR>DecidableEq α<VAR>LT α<VAR>s : Finset ι<VAR>f : ι → WithTop α<VAR>h : ∀ i ∈ s, f i ≠ ⊤<GOAL>∏ i ∈ s, f i < ⊤