case intro
M✝ : Type ?u.27146
A : Type ?u.27149
B : Type ?u.27152
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset { x // x ∈ S }
⊢ Multiset.prod (Multiset.map Subtype.val m) ∈ S
M✝ : Type ?u.27146
A : Type ?u.27149
B : Type ?u.27152
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset M
hm : ∀ (a : M), a ∈ m → a ∈ S
⊢ Multiset.prod m ∈ S
lift m to Multiset S using hm
case intro
M✝ : Type ?u.27146
A : Type ?u.27149
B : Type ?u.27152
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset { x // x ∈ S }
⊢ ↑(Multiset.prod m) ∈ S
case intro
M✝ : Type ?u.27146
A : Type ?u.27149
B : Type ?u.27152
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset { x // x ∈ S }
⊢ Multiset.prod (Multiset.map Subtype.val m) ∈ S
rw [← coe_multiset_prod]
no goals
case intro
M✝ : Type ?u.27146
A : Type ?u.27149
B : Type ?u.27152
inst✝³ : Monoid M✝
inst✝² : SetLike B M✝
inst✝¹ : SubmonoidClass B M✝
S✝ : B
s : Submonoid M✝
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
m : Multiset { x // x ∈ S }
⊢ ↑(Multiset.prod m) ∈ S
exact m.prod.coe_prop