case h
ι : Type ?u.136499
α : Type u_1
β : Type ?u.136505
γ : Type ?u.136508
inst✝ : CommMonoid α
m : Multiset α
h✝ : ∀ (x : α), x ∈ m → x = 1
l : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → x = 1
⊢ prod (Quotient.mk (List.isSetoid α) l) = 1
ι : Type ?u.136499
α : Type u_1
β : Type ?u.136505
γ : Type ?u.136508
inst✝ : CommMonoid α
m : Multiset α
h : ∀ (x : α), x ∈ m → x = 1
⊢ prod m = 1
induction' m using Quotient.inductionOn with l
no goals
case h
ι : Type ?u.136499
α : Type u_1
β : Type ?u.136505
γ : Type ?u.136508
inst✝ : CommMonoid α
m : Multiset α
h✝ : ∀ (x : α), x ∈ m → x = 1
l : List α
h : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → x = 1
⊢ prod (Quotient.mk (List.isSetoid α) l) = 1
simp [List.prod_eq_one h]