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