case intro
ι : Type ?u.89646
α : Type u_1
β : Type ?u.89652
γ : Type ?u.89655
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
s' : Multiset α
hs' : s = 0 ::ₘ s'
⊢ prod s = 0
ι : Type ?u.89646
α : Type u_1
β : Type ?u.89652
γ : Type ?u.89655
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
⊢ prod s = 0
rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩
no goals
case intro
ι : Type ?u.89646
α : Type u_1
β : Type ?u.89652
γ : Type ?u.89655
inst✝ : CommMonoidWithZero α
s : Multiset α
h : 0 ∈ s
s' : Multiset α
hs' : s = 0 ::ₘ s'
⊢ prod s = 0
simp [hs', Multiset.prod_cons]