no goals
ι : Type ?u.118660
α : Type u_1
β : Type ?u.118666
γ : Type ?u.118669
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
l : List α
hl : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → 1 ≤ x
x : α
hx : x ∈ Quotient.mk (List.isSetoid α) l
⊢ x ≤ prod (Quotient.mk (List.isSetoid α) l)
simpa using List.single_le_prod hl x hx