no goals
α : Type u_1
inst✝ : CanonicallyOrderedMonoid α
m : Multiset α
l : List α
⊢ prod (Quotient.mk (List.isSetoid α) l) = 1 ↔ ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → x = 1
simpa using List.prod_eq_one_iff l