case intro
M✝ : Type ?u.14811
A : Type ?u.14814
B : Type u_2
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset { x // x ∈ S }
⊢ Multiset.prod (Multiset.map Subtype.val m) ∈ S
M✝ : Type ?u.14811
A : Type ?u.14814
B : Type u_2
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B 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.14811
A : Type ?u.14814
B : Type u_2
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset { x // x ∈ S }
⊢ ↑(Multiset.prod m) ∈ S
case intro
M✝ : Type ?u.14811
A : Type ?u.14814
B : Type u_2
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B 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.14811
A : Type ?u.14814
B : Type u_2
inst✝⁵ : Monoid M✝
inst✝⁴ : SetLike B M✝
inst✝³ : SubmonoidClass B M✝
S : B
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset { x // x ∈ S }
⊢ ↑(Multiset.prod m) ∈ S
exact m.prod.coe_prop