ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set R<VAR>p : R → R → Prop<VAR>x y : R<VAR>hx : x ∈ Subsemiring.closure s<VAR>hy : y ∈ Subsemiring.closure s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>H0_left : ∀ (x : R), p 0 x<VAR>H0_right : ∀ (x : R), p x 0<VAR>H1_left : ∀ (x : R), p 1 x<VAR>H1_right : ∀ (x : R), p x 1<VAR>Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)<GOAL>p x y
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<VAR>x : R<GOAL>x ∈ Subsemiring.closure s ↔ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>Subsemiring.closure ↑s = s
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>Subsemiring.closure ∅ = ⊥
<VAR>R : Type u<VAR>NonAssocSemiring R<GOAL>Subsemiring.closure Set.univ = ⊤
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s t : Set R<GOAL>Subsemiring.closure (s ∪ t) = Subsemiring.closure s ⊔ Subsemiring.closure t
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>ι : Sort u_1<VAR>s : ι → Set R<GOAL>Subsemiring.closure (⋃ i, s i) = ⨆ i, Subsemiring.closure (s i)
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Set (Set R)<GOAL>Subsemiring.closure (⋃₀ s) = ⨆ t ∈ s, Subsemiring.closure t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s t : Subsemiring R<VAR>f : R →+* S<GOAL>Subsemiring.map f (s ⊔ t) = Subsemiring.map f s ⊔ Subsemiring.map f t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>ι : Sort u_1<VAR>f : R →+* S<VAR>s : ι → Subsemiring R<GOAL>Subsemiring.map f (iSup s) = ⨆ i, Subsemiring.map f (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s t : Subsemiring S<VAR>f : R →+* S<GOAL>Subsemiring.comap f (s ⊓ t) = Subsemiring.comap f s ⊓ Subsemiring.comap f t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>ι : Sort u_1<VAR>f : R →+* S<VAR>s : ι → Subsemiring S<GOAL>Subsemiring.comap f (iInf s) = ⨅ i, Subsemiring.comap f (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>Subsemiring.map f ⊥ = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>Subsemiring.comap f ⊤ = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring R<VAR>t : Subsemiring S<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring R<VAR>t : Subsemiring S<VAR>p : R × S<GOAL>p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s₁ s₂ : Subsemiring R<VAR>hs : s₁ ≤ s₂<VAR>t₁ t₂ : Subsemiring S<VAR>ht : t₁ ≤ t₂<GOAL>s₁.prod t₁ ≤ s₂.prod t₂
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring R<GOAL>Monotone fun t => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>t : Subsemiring S<GOAL>Monotone fun s => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring R<GOAL>s.prod ⊤ = Subsemiring.comap (RingHom.fst R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring S<GOAL>⊤.prod s = Subsemiring.comap (RingHom.snd R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>S : Set (Subsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>σR : Type u_1<VAR>SetLike σR R<VAR>SubsemiringClass σR R<VAR>f : R →+* S<VAR>s : σR<VAR>x : ↥s<GOAL>(f.domRestrict s) x = f ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>σR : Type u_1<VAR>σS : Type u_2<VAR>SetLike σR R<VAR>SetLike σS S<VAR>SubsemiringClass σR R<VAR>SubsemiringClass σS S<VAR>f : R →+* S<VAR>s' : σR<VAR>s : σS<VAR>h : ∀ x ∈ s', f x ∈ s<VAR>x : ↥s'<GOAL>↑((f.restrict s' s h) x) = f ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>σR : Type u_1<VAR>σS : Type u_2<VAR>SetLike σR R<VAR>SetLike σS S<VAR>SubsemiringClass σR R<VAR>SubsemiringClass σS S<VAR>f : R →+* S<VAR>s' : σR<VAR>s : σS<VAR>h : ∀ x ∈ s', f x ∈ s<GOAL>(SubsemiringClass.subtype s).comp (f.restrict s' s h) = f.comp (SubsemiringClass.subtype s')
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>x : R<GOAL>↑(f.rangeSRestrict x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>Function.Surjective ⇑f.rangeSRestrict
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>f.rangeS = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>f.rangeS = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<GOAL>f.eqLocusS f = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f g : R →+* S<VAR>s : Set R<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(Subsemiring.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f g : R →+* S<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Set R<VAR>hs : Subsemiring.closure s = ⊤<VAR>f g : R →+* S<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>s : Set S<GOAL>Subsemiring.closure (⇑f ⁻¹' s) ≤ Subsemiring.comap f (Subsemiring.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>s : Set R<GOAL>Subsemiring.map f (Subsemiring.closure s) = Subsemiring.closure (⇑f '' s)
<VAR>R : Type u<VAR>NonAssocSemiring R<VAR>s : Subsemiring R<GOAL>s.subtype.rangeS = s
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>(RingHom.fst R S).rangeS = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<GOAL>(RingHom.snd R S).rangeS = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>s : Subsemiring R<VAR>t : Subsemiring S<GOAL>s.prod ⊥ ⊔ ⊥.prod t = s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>g : S → R<VAR>f : R →+* S<VAR>h : Function.LeftInverse g ⇑f<VAR>x : R<GOAL>↑((RingEquiv.ofLeftInverseS h) x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>g : S → R<VAR>f : R →+* S<VAR>h : Function.LeftInverse g ⇑f<VAR>x : ↥f.rangeS<GOAL>(RingEquiv.ofLeftInverseS h).symm x = g ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<VAR>s : Subsemiring R<VAR>x : ↑↑s.toAddSubmonoid<GOAL>↑((e.subsemiringMap s) x) = e ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>e : R ≃+* S<VAR>s : Subsemiring R<VAR>y : ↑(⇑↑e.toAddEquiv '' ↑s.toAddSubmonoid)<GOAL>↑((e.subsemiringMap s).symm y) = (↑e).symm ↑y
<VAR>R' : Type u_1<VAR>α : Type u_2<VAR>NonAssocSemiring R'<VAR>SMul R' α<VAR>S : Subsemiring R'<VAR>g : ↥S<VAR>m : α<GOAL>g • m = ↑g • m
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>t : Subsemiring S<GOAL>Subsemiring.map f (Subsemiring.comap f t) = t ⊓ f.rangeS
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>t : Subsemiring S<VAR>h : t ≤ f.rangeS<GOAL>Subsemiring.map f (Subsemiring.comap f t) = t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>t : Subsemiring S<GOAL>Subsemiring.map f (Subsemiring.comap f t) = t
<VAR>R : Type u<VAR>S : Type v<VAR>NonAssocSemiring R<VAR>NonAssocSemiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>s : Subsemiring R<GOAL>Subsemiring.comap f (Subsemiring.map f s) = s
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>m n : R<VAR>h : Squarefree (m * n)<GOAL>IsRelPrime m n
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>x : R<VAR>h : IsUnit x<GOAL>Squarefree x
<VAR>R : Type u_1<VAR>CommMonoid R<GOAL>Squarefree 1
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>Nontrivial R<GOAL>¬Squarefree 0
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>Nontrivial R<VAR>m : R<VAR>hm : Squarefree m<GOAL>m ≠ 0
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>x : R<VAR>h : Irreducible x<GOAL>Squarefree x
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x : R<VAR>h : Prime x<GOAL>Squarefree x
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>m n : R<VAR>hmn : Squarefree (m * n)<GOAL>Squarefree m
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>m n : R<VAR>hmn : Squarefree (m * n)<GOAL>Squarefree n
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>x y : R<VAR>hdvd : x ∣ y<VAR>hsq : Squarefree y<GOAL>Squarefree x
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>x : R<VAR>n : ℕ<VAR>h : Squarefree (x ^ n)<VAR>h' : ¬IsUnit x<GOAL>n = 0 ∨ n = 1
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<VAR>b : α<VAR>hb : Squarefree b<GOAL>Squarefree (gcd a b)
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>GCDMonoid α<VAR>a : α<VAR>b : α<VAR>ha : Squarefree a<GOAL>Squarefree (gcd a b)
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>DecidableRel Dvd.dvd<VAR>r : R<GOAL>Squarefree r ↔ ∀ (x : R), multiplicity x r ≤ 1 ∨ IsUnit x
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>WfDvdMonoid R<VAR>a b : R<VAR>ha : Prime a<VAR>hb : b ≠ 0<GOAL>multiplicity.Finite a b
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>WfDvdMonoid R<VAR>x : R<VAR>hx₀ : x ≠ 0<GOAL>Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>WfDvdMonoid R<VAR>r : R<GOAL>(∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>WfDvdMonoid R<VAR>r : R<VAR>hr : r ≠ 0<GOAL>Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>WfDvdMonoid R<VAR>r : R<VAR>hr : ∃ x, Irreducible x<GOAL>Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>DecompositionMonoid R<VAR>x : R<VAR>hx : Squarefree x<GOAL>IsRadical x
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>DecompositionMonoid R<VAR>x y : R<VAR>n : ℕ<VAR>hsq : Squarefree x<VAR>h0 : n ≠ 0<GOAL>x ∣ y ^ n ↔ x ∣ y
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x : R<VAR>h0 : x ≠ 0<VAR>h : IsRadical x<GOAL>Squarefree x
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x y p : R<VAR>k : ℕ<VAR>hx : Squarefree x<VAR>hp : Prime p<VAR>h : p ^ (k + 1) ∣ x * y<GOAL>p ^ k ∣ y
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x y p : R<VAR>k : ℕ<VAR>hy : Squarefree y<VAR>hp : Prime p<VAR>h : p ^ (k + 1) ∣ x * y<GOAL>p ^ k ∣ x
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x y d : R<VAR>DecompositionMonoid R<VAR>hx : Squarefree x<VAR>h : d * d ∣ x * y<GOAL>d ∣ y
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x y d : R<VAR>DecompositionMonoid R<VAR>hy : Squarefree y<VAR>h : d * d ∣ x * y<GOAL>d ∣ x
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x y : R<VAR>DecompositionMonoid R<GOAL>Squarefree (x * y) ↔ IsRelPrime x y ∧ Squarefree x ∧ Squarefree y
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x : R<VAR>DecompositionMonoid R<GOAL>IsRadical x ↔ Squarefree x ∨ x = 0
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x : R<VAR>DecompositionMonoid R<VAR>h : x ≠ 0<GOAL>IsRadical x ↔ Squarefree x
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>∃ y n, Squarefree y ∧ y ∣ x ∧ x ∣ y ^ n
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>NormalizationMonoid R<VAR>x : R<VAR>x0 : x ≠ 0<GOAL>Squarefree x ↔ (UniqueFactorizationMonoid.normalizedFactors x).Nodup
<VAR>n : ℤ<GOAL>Squarefree n.natAbs ↔ Squarefree n
<VAR>n : ℕ<GOAL>Squarefree ↑n ↔ Squarefree n
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<GOAL>s.sum = Multiset.foldr (fun x x_1 => x + x_1) ⋯ 0 s
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<GOAL>s.prod = Multiset.foldr (fun x x_1 => x * x_1) ⋯ 1 s
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<GOAL>s.sum = Multiset.foldl (fun x x_1 => x + x_1) ⋯ 0 s
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<GOAL>s.prod = Multiset.foldl (fun x x_1 => x * x_1) ⋯ 1 s
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>l : List α<GOAL>(↑l).prod = l.prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>l : List α<GOAL>(↑l).sum = l.sum
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<GOAL>s.toList.sum = s.sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<GOAL>s.toList.prod = s.prod
<VAR>α : Type u_3<VAR>CommMonoid α<GOAL>Multiset.prod 0 = 1
<VAR>α : Type u_3<VAR>AddCommMonoid α<GOAL>Multiset.sum 0 = 0
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).prod = a * s.prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).sum = a + s.sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∈ s<GOAL>a * (s.erase a).prod = s.prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∈ s<GOAL>a + (s.erase a).sum = s.sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>CommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>DecidableEq ι<VAR>a : ι<VAR>h : a ∈ m<GOAL>f a * (Multiset.map f (m.erase a)).prod = (Multiset.map f m).prod
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>DecidableEq ι<VAR>a : ι<VAR>h : a ∈ m<GOAL>f a + (Multiset.map f (m.erase a)).sum = (Multiset.map f m).sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>a : α<GOAL>{a}.prod = a
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>a : α<GOAL>{a}.sum = a
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>a b : α<GOAL>{a, b}.prod = a * b
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>a b : α<GOAL>{a, b}.sum = a + b
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s t : Multiset α<GOAL>(s + t).prod = s.prod * t.prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s t : Multiset α<GOAL>(s + t).sum = s.sum + t.sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>m : Multiset α<VAR>n : ℕ<GOAL>(n • m).prod = m.prod ^ n
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>m : Multiset α<VAR>n : ℕ<GOAL>(n • m).sum = n • m.sum
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>(Multiset.filter p s).sum + (Multiset.filter (fun a => ¬p a) s).sum = s.sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>(Multiset.filter p s).prod * (Multiset.filter (fun a => ¬p a) s).prod = s.prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>a : α<GOAL>(Multiset.replicate n a).sum = n • a
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>n : ℕ<VAR>a : α<GOAL>(Multiset.replicate n a).prod = a ^ n
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>CommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>DecidableEq ι<VAR>i : ι<VAR>hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1<GOAL>(Multiset.map f m).prod = f i ^ Multiset.count i m
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>DecidableEq ι<VAR>i : ι<VAR>hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0<GOAL>(Multiset.map f m).sum = Multiset.count i m • f i
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<VAR>DecidableEq α<VAR>a : α<VAR>h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 0<GOAL>s.sum = Multiset.count a s • a
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<VAR>DecidableEq α<VAR>a : α<VAR>h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1<GOAL>s.prod = a ^ Multiset.count a s
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<VAR>h : ∀ x ∈ s, x = 1<GOAL>s.prod = 1
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<VAR>h : ∀ x ∈ s, x = 0<GOAL>s.sum = 0
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<VAR>DecidableEq α<VAR>a : α<GOAL>a ^ Multiset.count a s = (Multiset.filter (Eq a) s).prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<VAR>DecidableEq α<VAR>a : α<GOAL>Multiset.count a s • a = (Multiset.filter (Eq a) s).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Multiset α<VAR>F : Type u_6<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<GOAL>(Multiset.map (⇑f) s).prod = f s.prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Multiset α<VAR>F : Type u_6<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>f : F<GOAL>(Multiset.map (⇑f) s).sum = f s.sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Multiset ι<VAR>F : Type u_6<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>(Multiset.map (fun i => f (g i)) s).sum = f (Multiset.map g s).sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Multiset ι<VAR>F : Type u_6<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>(Multiset.map (fun i => f (g i)) s).prod = f (Multiset.map g s).prod
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid α<VAR>CommMonoid β<VAR>CommMonoid γ<VAR>s : Multiset ι<VAR>f : α → β → γ<VAR>hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d<VAR>hf' : f 1 1 = 1<VAR>f₁ : ι → α<VAR>f₂ : ι → β<GOAL>(Multiset.map (fun i => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>s : Multiset ι<VAR>f : α → β → γ<VAR>hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d<VAR>hf' : f 0 0 = 0<VAR>f₁ : ι → α<VAR>f₂ : ι → β<GOAL>(Multiset.map (fun i => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Multiset ι<VAR>r : α → β → Prop<VAR>f : ι → α<VAR>g : ι → β<VAR>h₁ : r 1 1<VAR>h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)<GOAL>r (Multiset.map f s).prod (Multiset.map g s).prod
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Multiset ι<VAR>r : α → β → Prop<VAR>f : ι → α<VAR>g : ι → β<VAR>h₁ : r 0 0<VAR>h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a + b) (g a + c)<GOAL>r (Multiset.map f s).sum (Multiset.map g s).sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>m : Multiset ι<GOAL>(Multiset.map (fun x => 0) m).sum = 0
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>CommMonoid α<VAR>m : Multiset ι<GOAL>(Multiset.map (fun x => 1) m).prod = 1
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>m : Multiset ι<VAR>f g : ι → α<GOAL>(Multiset.map (fun i => f i + g i) m).sum = (Multiset.map f m).sum + (Multiset.map g m).sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>CommMonoid α<VAR>m : Multiset ι<VAR>f g : ι → α<GOAL>(Multiset.map (fun i => f i * g i) m).prod = (Multiset.map f m).prod * (Multiset.map g m).prod
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>CommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>n : ℕ<GOAL>(Multiset.map (fun i => f i ^ n) m).prod = (Multiset.map f m).prod ^ n
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>n : ℕ<GOAL>(Multiset.map (fun i => n • f i) m).sum = n • (Multiset.map f m).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid α<VAR>m : Multiset β<VAR>n : Multiset γ<VAR>f : β → γ → α<GOAL>(Multiset.map (fun a => (Multiset.map (fun b => f a b) n).prod) m).prod = (Multiset.map (fun b => (Multiset.map (fun a => f a b) m).prod) n).prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid α<VAR>m : Multiset β<VAR>n : Multiset γ<VAR>f : β → γ → α<GOAL>(Multiset.map (fun a => (Multiset.map (fun b => f a b) n).sum) m).sum = (Multiset.map (fun b => (Multiset.map (fun a => f a b) m).sum) n).sum
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>p : α → Prop<VAR>s : Multiset α<VAR>p_mul : ∀ (a b : α), p a → p b → p (a + b)<VAR>p_one : p 0<VAR>p_s : ∀ a ∈ s, p a<GOAL>p s.sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>p : α → Prop<VAR>s : Multiset α<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>p_one : p 1<VAR>p_s : ∀ a ∈ s, p a<GOAL>p s.prod
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>hs : s ≠ ∅<VAR>p_s : ∀ a ∈ s, p a<GOAL>p s.prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<VAR>s : Multiset α<VAR>p : α → Prop<VAR>p_mul : ∀ (a b : α), p a → p b → p (a + b)<VAR>hs : s ≠ ∅<VAR>p_s : ∀ a ∈ s, p a<GOAL>p s.sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>s.prod ∣ t.prod
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>s : Multiset α<GOAL>f s.prod = (Multiset.map (⇑f) s).prod
<VAR>F : Type u_1<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>s : Multiset α<GOAL>f s.sum = (Multiset.map (⇑f) s).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>f : α →* β<VAR>s : Multiset α<GOAL>f s.prod = (Multiset.map (⇑f) s).prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>f : α →+ β<VAR>s : Multiset α<GOAL>f s.sum = (Multiset.map (⇑f) s).sum
<VAR>α : Type u_3<VAR>CommMonoid α<VAR>s : Multiset α<VAR>a : α<GOAL>a ∈ s → a ∣ s.prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Multiset (α × β)<GOAL>s.prod.1 = (Multiset.map Prod.fst s).prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Multiset (α × β)<GOAL>s.sum.1 = (Multiset.map Prod.fst s).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>s : Multiset (α × β)<GOAL>s.prod.2 = (Multiset.map Prod.snd s).prod
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>s : Multiset (α × β)<GOAL>s.sum.2 = (Multiset.map Prod.snd s).sum
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CommMonoid β<VAR>S : Multiset α<VAR>g1 g2 : α → β<VAR>h : ∀ a ∈ S, g1 a ∣ g2 a<GOAL>(Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod
<VAR>α : Type u_3<VAR>AddCommMonoid α<GOAL>⇑Multiset.sumAddMonoidHom = Multiset.sum
<VAR>α : Type u_3<VAR>SubtractionCommMonoid α<VAR>m : Multiset α<GOAL>(Multiset.map Neg.neg m).sum = -m.sum
<VAR>α : Type u_3<VAR>DivisionCommMonoid α<VAR>m : Multiset α<GOAL>(Multiset.map Inv.inv m).prod = m.prod⁻¹
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>DivisionCommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<GOAL>(Multiset.map (fun i => (f i)⁻¹) m).prod = (Multiset.map f m).prod⁻¹
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>SubtractionCommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<GOAL>(Multiset.map (fun i => -f i) m).sum = -(Multiset.map f m).sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>SubtractionCommMonoid α<VAR>m : Multiset ι<VAR>f g : ι → α<GOAL>(Multiset.map (fun i => f i - g i) m).sum = (Multiset.map f m).sum - (Multiset.map g m).sum
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>DivisionCommMonoid α<VAR>m : Multiset ι<VAR>f g : ι → α<GOAL>(Multiset.map (fun i => f i / g i) m).prod = (Multiset.map f m).prod / (Multiset.map g m).prod
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>DivisionCommMonoid α<VAR>m : Multiset ι<VAR>f : ι → α<VAR>n : ℤ<GOAL>(Multiset.map (fun i => f i ^ n) m).prod = (Multiset.map f m).prod ^ n