ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>CommMonoidWithZero α<VAR>NoZeroDivisors α<VAR>Nontrivial α<VAR>s : Multiset α<VAR>h : 0 ∉ s<GOAL>s.prod ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>a : α<VAR>s : Multiset ι<VAR>f : ι → α<GOAL>(Multiset.map (fun i => a * f i) s).sum = a * (Multiset.map f s).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>a : α<VAR>s : Multiset ι<VAR>f : ι → α<GOAL>(Multiset.map (fun i => f i * a) s).sum = (Multiset.map f s).sum * a
<VAR>α : Type u_2<VAR>NonUnitalSemiring α<VAR>s : Multiset α<VAR>a : α<GOAL>(∀ x ∈ s, a ∣ x) → a ∣ s.sum
<VAR>α : Type u_2<VAR>CommSemiring α<VAR>s : Multiset (Multiset α)<GOAL>(Multiset.map Multiset.sum s).prod = (Multiset.map Multiset.prod s.Sections).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommSemiring α<VAR>s : Multiset ι<VAR>f g : ι → α<GOAL>(Multiset.map (fun i => f i + g i) s).prod = (Multiset.map (fun p => (Multiset.map f p.1).prod * (Multiset.map g p.2).prod) s.antidiagonal).sum
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>s : Multiset α<VAR>a : α<VAR>h : ∀ b ∈ s, Commute a b<GOAL>Commute a s.sum
<VAR>α : Type u_2<VAR>NonUnitalNonAssocSemiring α<VAR>s : Multiset α<VAR>b : α<VAR>h : ∀ a ∈ s, Commute a b<GOAL>Commute s.sum b
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>Semiring R<VAR>degb : A → B<VAR>f g : AddMonoidAlgebra R A<GOAL>(f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>Semiring R<VAR>degt : A → T<VAR>f g : AddMonoidAlgebra R A<GOAL>f.support.inf degt ⊓ g.support.inf degt ≤ (f + g).support.inf degt
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>Semiring R<VAR>Add A<VAR>Add B<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b<VAR>f g : AddMonoidAlgebra R A<GOAL>(f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>Semiring R<VAR>Add A<VAR>Add T<VAR>CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degt : A → T<VAR>degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b)<VAR>f g : AddMonoidAlgebra R A<GOAL>f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>Semiring R<VAR>AddMonoid A<VAR>AddMonoid B<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>l : List (AddMonoidAlgebra R A)<GOAL>l.prod.support.sup degb ≤ (List.map (fun f => f.support.sup degb) l).sum
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>Semiring R<VAR>AddMonoid A<VAR>AddMonoid T<VAR>CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>l : List (AddMonoidAlgebra R A)<GOAL>(List.map (fun f => f.support.inf degt) l).sum ≤ l.prod.support.inf degt
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>Semiring R<VAR>AddMonoid A<VAR>AddMonoid B<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>n : ℕ<VAR>f : AddMonoidAlgebra R A<GOAL>(f ^ n).support.sup degb ≤ n • f.support.sup degb
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>Semiring R<VAR>AddMonoid A<VAR>AddMonoid T<VAR>CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>n : ℕ<VAR>f : AddMonoidAlgebra R A<GOAL>n • f.support.inf degt ≤ (f ^ n).support.inf degt
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>m : Multiset (AddMonoidAlgebra R A)<GOAL>m.prod.support.sup degb ≤ (Multiset.map (fun f => f.support.sup degb) m).sum
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid T<VAR>CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>m : Multiset (AddMonoidAlgebra R A)<GOAL>(Multiset.map (fun f => f.support.inf degt) m).sum ≤ m.prod.support.inf degt
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>s : Finset ι<VAR>f : ι → AddMonoidAlgebra R A<GOAL>(∏ i ∈ s, f i).support.sup degb ≤ ∑ i ∈ s, (f i).support.sup degb
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>ι : Type u_6<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid T<VAR>CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>s : Finset ι<VAR>f : ι → AddMonoidAlgebra R A<GOAL>∑ i ∈ s, (f i).support.inf degt ≤ (∏ i ∈ s, f i).support.inf degt
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>f g : AddMonoidAlgebra R A<GOAL>AddMonoidAlgebra.supDegree D (f + g) ≤ AddMonoidAlgebra.supDegree D f ⊔ AddMonoidAlgebra.supDegree D g
<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Ring R'<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>f : AddMonoidAlgebra R' A<GOAL>AddMonoidAlgebra.supDegree D (-f) = AddMonoidAlgebra.supDegree D f
<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Ring R'<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>f g : AddMonoidAlgebra R' A<GOAL>AddMonoidAlgebra.supDegree D (f - g) ≤ AddMonoidAlgebra.supDegree D f ⊔ AddMonoidAlgebra.supDegree D g
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → AddMonoidAlgebra R A<GOAL>AddMonoidAlgebra.supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i => AddMonoidAlgebra.supDegree D (f i)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>a : A<VAR>r : R<VAR>hr : r ≠ 0<GOAL>AddMonoidAlgebra.supDegree D (AddMonoidAlgebra.single a r) = D a
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>a : A<VAR>r : R<GOAL>AddMonoidAlgebra.supDegree D (AddMonoidAlgebra.single a r) = if r = 0 then ⊥ else D a
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<GOAL>AddMonoidAlgebra.supDegree D 0 = ⊥
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>p : AddMonoidAlgebra R A<GOAL>AddMonoidAlgebra.supDegree D p ≠ ⊥ → p ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>p : AddMonoidAlgebra R A<VAR>b : B<VAR>h : ¬AddMonoidAlgebra.supDegree D p ≤ b<GOAL>p ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>p : AddMonoidAlgebra R A<VAR>a : A<VAR>hlt : ¬D a ≤ AddMonoidAlgebra.supDegree D p<GOAL>p a = 0
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>Add B<VAR>OrderBot B<VAR>D : A → B<VAR>p q : AddMonoidAlgebra R A<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>AddMonoidAlgebra.supDegree D (p * q) ≤ AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
<VAR>R : Type u_7<VAR>A : Type u_8<VAR>B : Type u_9<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>D : A → B<VAR>hzero : D 0 = 0<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>ι : Type u_10<VAR>s : Finset ι<VAR>f : ι → AddMonoidAlgebra R A<GOAL>AddMonoidAlgebra.supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, AddMonoidAlgebra.supDegree D (f i)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeSup B<VAR>Add B<VAR>OrderBot B<VAR>D : A → B<VAR>p q : AddMonoidAlgebra R A<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hD : Function.Injective D<VAR>ap aq : A<VAR>hp : AddMonoidAlgebra.supDegree D p ≤ D ap<VAR>hq : AddMonoidAlgebra.supDegree D q ≤ D aq<GOAL>(p * q) (ap + aq) = p ap * q aq
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>B : Type u_5<VAR>Semiring R<VAR>SemilatticeSup B<VAR>OrderBot B<VAR>D : A → B<VAR>s : AddMonoidAlgebra R A<VAR>hs : s.support.Nonempty<GOAL>AddMonoidAlgebra.supDegree (WithBot.some ∘ D) s = ↑(AddMonoidAlgebra.supDegree D s)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>D : A → T<VAR>f g : AddMonoidAlgebra R A<GOAL>AddMonoidAlgebra.infDegree D f ⊓ AddMonoidAlgebra.infDegree D g ≤ AddMonoidAlgebra.infDegree D (f + g)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>Semiring R<VAR>AddZeroClass A<VAR>SemilatticeInf T<VAR>Add T<VAR>OrderTop T<VAR>CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>D : AddHom A T<VAR>f g : AddMonoidAlgebra R A<GOAL>AddMonoidAlgebra.infDegree (⇑D) f + AddMonoidAlgebra.infDegree (⇑D) g ≤ AddMonoidAlgebra.infDegree (⇑D) (f * g)
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>T : Type u_4<VAR>Semiring R<VAR>SemilatticeInf T<VAR>OrderTop T<VAR>D : A → T<VAR>s : AddMonoidAlgebra R A<VAR>hs : s.support.Nonempty<GOAL>AddMonoidAlgebra.infDegree (WithTop.some ∘ D) s = ↑(AddMonoidAlgebra.infDegree D s)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>AddMonoidWithOne R<VAR>SetLike S R<VAR>s : S<VAR>AddSubmonoidWithOneClass S R<VAR>n : ℕ<GOAL>↑n ∈ s
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>AddMonoidWithOne R<VAR>SetLike S R<VAR>AddSubmonoidWithOneClass S R<VAR>s : S<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>OfNat.ofNat n ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>SetLike S R<VAR>hSR : SubsemiringClass S R<VAR>s : S<GOAL>⇑(SubsemiringClass.subtype s) = Subtype.val
<VAR>S : Type v<VAR>s : S<VAR>R : Type u_1<VAR>Semiring R<VAR>SetLike S R<VAR>SubsemiringClass S R<VAR>x : ↥s<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x : R<GOAL>x ∈ s.toSubmonoid ↔ x ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x : R<GOAL>x ∈ s.carrier ↔ x ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>S T : Subsemiring R<VAR>h : ∀ (x : R), x ∈ S ↔ x ∈ T<GOAL>S = T
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>S : Subsemiring R<VAR>s : Set R<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>Function.Injective Subsemiring.toSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>StrictMono Subsemiring.toSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>Monotone Subsemiring.toSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>Function.Injective Subsemiring.toAddSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>StrictMono Subsemiring.toAddSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>Monotone Subsemiring.toAddSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<GOAL>↑(Subsemiring.mk' s sm hm sa ha) = s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<VAR>x : R<GOAL>x ∈ Subsemiring.mk' s sm hm sa ha ↔ x ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<GOAL>(Subsemiring.mk' s sm hm sa ha).toSubmonoid = sm
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>sm : Submonoid R<VAR>hm : ↑sm = s<VAR>sa : AddSubmonoid R<VAR>ha : ↑sa = s<GOAL>(Subsemiring.mk' s sm hm sa ha).toAddSubmonoid = sa
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>1 ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>0 ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x y : R<GOAL>x ∈ s → y ∈ s → x * y ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x y : R<GOAL>x ∈ s → y ∈ s → x + y ∈ s
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Subsemiring R<VAR>l : List R<GOAL>(∀ x ∈ l, x ∈ s) → l.prod ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>l : List R<GOAL>(∀ x ∈ l, x ∈ s) → l.sum ∈ s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>s : Subsemiring R<VAR>m : Multiset R<GOAL>(∀ a ∈ m, a ∈ s) → m.prod ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>m : Multiset R<GOAL>(∀ a ∈ m, a ∈ s) → m.sum ∈ s
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>s : Subsemiring R<VAR>ι : Type u_2<VAR>t : Finset ι<VAR>f : ι → R<VAR>h : ∀ c ∈ t, f c ∈ s<GOAL>∏ i ∈ t, f i ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>ι : Type u_1<VAR>t : Finset ι<VAR>f : ι → R<VAR>h : ∀ c ∈ t, f c ∈ s<GOAL>∑ i ∈ t, f i ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>↑1 = 1
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>↑0 = 0
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x y : ↥s<GOAL>↑(x + y) = ↑x + ↑y
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x y : ↥s<GOAL>↑(x * y) = ↑x * ↑y
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Subsemiring R<VAR>x : R<VAR>hx : x ∈ s<VAR>n : ℕ<GOAL>x ^ n ∈ s
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Subsemiring R<VAR>x : ↥s<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>⇑s.subtype = Subtype.val
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x : R<VAR>hx : x ∈ s<VAR>n : ℕ<GOAL>n • x ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>↑s.toSubmonoid = ↑s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>s.carrier = ↑s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<VAR>x : R<GOAL>x ∈ s.toAddSubmonoid ↔ x ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>↑s.toAddSubmonoid = ↑s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>x : R<GOAL>x ∈ ⊤
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>↑⊤ = Set.univ
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>r : R<GOAL>↑(Subsemiring.topEquiv.symm r) = r
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>r : ↥⊤<GOAL>Subsemiring.topEquiv r = ↑r
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring S<VAR>f : R →+* S<GOAL>↑(Subsemiring.comap f s) = ⇑f ⁻¹' ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring S<VAR>f : R →+* S<VAR>x : R<GOAL>x ∈ Subsemiring.comap f s ↔ f x ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring T<VAR>s : Subsemiring T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subsemiring.comap f (Subsemiring.comap g s) = Subsemiring.comap (g.comp f) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>s : Subsemiring R<GOAL>↑(Subsemiring.map f s) = ⇑f '' ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>s : Subsemiring R<VAR>y : S<GOAL>y ∈ Subsemiring.map f s ↔ ∃ x ∈ s, f x = y
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>Subsemiring.map (RingHom.id R) s = s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring T<VAR>s : Subsemiring R<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subsemiring.map g (Subsemiring.map f s) = Subsemiring.map (g.comp f) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>s : Subsemiring R<VAR>t : Subsemiring S<GOAL>Subsemiring.map f s ≤ t ↔ s ≤ Subsemiring.comap f t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>GaloisConnection (Subsemiring.map f) (Subsemiring.comap f)
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>x : ↥s<GOAL>↑((s.equivMapOfInjective f hf) x) = f ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>↑f.rangeS = Set.range ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>y : S<GOAL>y ∈ f.rangeS ↔ ∃ x, f x = y
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>f.rangeS = Subsemiring.map f ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>x : R<GOAL>f x ∈ f.rangeS
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>NonAssocSemiring T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>Subsemiring.map g f.rangeS = (g.comp f).rangeS
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>↑⊥ = Set.range Nat.cast
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>x : R<GOAL>x ∈ ⊥ ↔ ∃ n, ↑n = x
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>p p' : Subsemiring R<GOAL>↑(p ⊓ p') = ↑p ∩ ↑p'
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>p p' : Subsemiring R<VAR>x : R<GOAL>x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring R)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring R)<VAR>x : R<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set (Subsemiring R)<GOAL>(sInf s).toSubmonoid = ⨅ t ∈ s, t.toSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set (Subsemiring R)<GOAL>(sInf s).toAddSubmonoid = ⨅ t ∈ s, t.toAddSubmonoid
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>A : Subsemiring R<GOAL>A = ⊤ ↔ ∀ (x : R), x ∈ A
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>↑(Subsemiring.center R) = Set.center R
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>(Subsemiring.center R).toSubmonoid = Submonoid.center R
<VAR>R : Type u_1<VAR>Semiring R<VAR>z : R<GOAL>z ∈ Subsemiring.center R ↔ ∀ (g : R), g * z = z * g
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>Subsemiring.center R = ⊤
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<GOAL>↑(Subsemiring.centralizer s) = s.centralizer
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<GOAL>(Subsemiring.centralizer s).toSubmonoid = Submonoid.centralizer s
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<VAR>z : R<GOAL>z ∈ Subsemiring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<GOAL>Subsemiring.center R ≤ Subsemiring.centralizer s
<VAR>R : Type u_1<VAR>Semiring R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>Subsemiring.centralizer t ≤ Subsemiring.centralizer s
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<GOAL>Subsemiring.centralizer s = ⊤ ↔ s ⊆ ↑(Subsemiring.center R)
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Subsemiring.centralizer Set.univ = Subsemiring.center R
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Subsemiring R<GOAL>s ≤ Subsemiring.centralizer ↑(Subsemiring.centralizer ↑s)
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<GOAL>Subsemiring.centralizer s.centralizer.centralizer = Subsemiring.centralizer s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>x : R<VAR>s : Set R<GOAL>x ∈ Subsemiring.closure s ↔ ∀ (S : Subsemiring R), s ⊆ ↑S → x ∈ S
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<GOAL>s ⊆ ↑(Subsemiring.closure s)
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>P : R<VAR>hP : P ∉ Subsemiring.closure s<GOAL>P ∉ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>t : Subsemiring R<GOAL>Subsemiring.closure s ≤ t ↔ s ⊆ ↑t
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>Subsemiring.closure s ≤ Subsemiring.closure t
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>t : Subsemiring R<VAR>h₁ : s ⊆ ↑t<VAR>h₂ : t ≤ Subsemiring.closure s<GOAL>Subsemiring.closure s = t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<VAR>K : Subsemiring R<VAR>x : S<GOAL>x ∈ Subsemiring.map (↑f) K ↔ f.symm x ∈ K
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<VAR>K : Subsemiring R<GOAL>Subsemiring.map (↑f) K = Subsemiring.comap (↑f.symm) K
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R ≃+* S<VAR>K : Subsemiring S<GOAL>Subsemiring.comap (↑f) K = Subsemiring.map (↑f.symm) K
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>M : Submonoid R<GOAL>↑M.subsemiringClosure = ↑(AddSubmonoid.closure ↑M)
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>M : Submonoid R<GOAL>M.subsemiringClosure.toAddSubmonoid = AddSubmonoid.closure ↑M
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>M : Submonoid R<GOAL>M.subsemiringClosure = Subsemiring.closure ↑M
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<GOAL>Subsemiring.closure ↑(Submonoid.closure s) = Subsemiring.closure s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<GOAL>↑(Subsemiring.closure s) = ↑(AddSubmonoid.closure ↑(Submonoid.closure s))
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>x : R<GOAL>x ∈ Subsemiring.closure s ↔ x ∈ AddSubmonoid.closure ↑(Submonoid.closure s)
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<GOAL>Subsemiring.closure ↑(AddSubmonoid.closure s) = Subsemiring.closure s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>p : R → Prop<VAR>x : R<VAR>h : x ∈ Subsemiring.closure s<VAR>mem : ∀ x ∈ s, p x<VAR>zero : p 0<VAR>one : p 1<VAR>add : ∀ (x y : R), p x → p y → p (x + y)<VAR>mul : ∀ (x y : R), p x → p y → p (x * y)<GOAL>p x
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>p : (x : R) → x ∈ Subsemiring.closure s → Prop<VAR>mem : ∀ (x : R) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>one : p 1 ⋯<VAR>add : ∀ (x : R) (hx : x ∈ Subsemiring.closure s) (y : R) (hy : y ∈ Subsemiring.closure s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : R) (hx : x ∈ Subsemiring.closure s) (y : R) (hy : y ∈ Subsemiring.closure s), p x hx → p y hy → p (x * y) ⋯<VAR>a : R<VAR>ha : a ∈ Subsemiring.closure s<GOAL>p a ha