no goals
M : Type u_1
A : Type ?u.81053
B : Type ?u.81056
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l x_1, List.prod l = x
rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image_iff_bex] at hx