case intro.intro
M✝ : Type ?u.82426
A : Type ?u.82429
B : Type ?u.82432
inst✝¹ : Monoid M✝
M : Type u_1
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
l : List M
h1 : ∀ (y : M), y ∈ l → y ∈ s
h2 : List.prod l = x
⊢ ∃ l x_1, Multiset.prod l = x
M✝ : Type ?u.82426
A : Type ?u.82429
B : Type ?u.82432
inst✝¹ : Monoid M✝
M : Type u_1
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l x_1, Multiset.prod l = x
obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx
no goals
case intro.intro
M✝ : Type ?u.82426
A : Type ?u.82429
B : Type ?u.82432
inst✝¹ : Monoid M✝
M : Type u_1
inst✝ : CommMonoid M
s : Set M
x : M
hx : x ∈ closure s
l : List M
h1 : ∀ (y : M), y ∈ l → y ∈ s
h2 : List.prod l = x
⊢ ∃ l x_1, Multiset.prod l = x
exact ⟨l, h1, (Multiset.coe_prod l).trans h2⟩