ι : Type ?u.125685
α : Type u_1
β : Type ?u.125691
γ : Type ?u.125694
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ ∀ (a : List α), (∀ (x : α), x ∈ a → 1 ≤ x) → List.prod a = 1 → ∀ (x : α), x ∈ a → x = 1
ι : Type ?u.125685
α : Type u_1
β : Type ?u.125691
γ : Type ?u.125694
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ ∀ (a : List α),
    (∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a → 1 ≤ x) →
      prod (Quotient.mk (List.isSetoid α) a) = 1 → ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) a → x = 1
simp only [quot_mk_to_coe, coe_prod, mem_coe]
no goals
ι : Type ?u.125685
α : Type u_1
β : Type ?u.125691
γ : Type ?u.125694
inst✝ : OrderedCommMonoid α
s t : Multiset α
a : α
⊢ ∀ (a : List α), (∀ (x : α), x ∈ a → 1 ≤ x) → List.prod a = 1 → ∀ (x : α), x ∈ a → x = 1
exact fun l => List.all_one_of_le_one_le_of_prod_eq_one