M✝ : Type ?u.55549
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type ?u.55558
inst✝¹ : AddMonoid A
t : Set A
M : Type u_1
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ Multiset.prod (Quotient.mk (List.isSetoid M) l) ∈ s
M✝ : Type ?u.55549
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type ?u.55558
inst✝¹ : AddMonoid A
t : Set A
M : Type u_1
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
⊢ (∀ (a : M), a ∈ m → a ∈ s) → Multiset.prod m ∈ s
refine' Quotient.inductionOn m fun l hl => _
M✝ : Type ?u.55549
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type ?u.55558
inst✝¹ : AddMonoid A
t : Set A
M : Type u_1
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ List.prod l ∈ s
M✝ : Type ?u.55549
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type ?u.55558
inst✝¹ : AddMonoid A
t : Set A
M : Type u_1
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ Multiset.prod (Quotient.mk (List.isSetoid M) l) ∈ s
rw [Multiset.quot_mk_to_coe, Multiset.coe_prod]
no goals
M✝ : Type ?u.55549
inst✝² : Monoid M✝
s✝ : Set M✝
A : Type ?u.55558
inst✝¹ : AddMonoid A
t : Set A
M : Type u_1
inst✝ : CommMonoid M
s : Set M
hs : IsSubmonoid s
m : Multiset M
l : List M
hl : ∀ (a : M), a ∈ Quotient.mk (List.isSetoid M) l → a ∈ s
⊢ List.prod l ∈ s
exact list_prod_mem hs hl