ι : Type ?u.595257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
⊢ Multiset.toFinset m ⊆ s → Multiset.prod m = ∏ i in s, i ^ Multiset.count i m
ι : Type ?u.595257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
hs : Multiset.toFinset m ⊆ s
⊢ Multiset.prod m = ∏ i in s, i ^ Multiset.count i m
revert hs
ι : Type ?u.595257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ Multiset.toFinset (Quot.mk Setoid.r l) ⊆ s →
    Multiset.prod (Quot.mk Setoid.r l) = ∏ i in s, i ^ Multiset.count i (Quot.mk Setoid.r l)
ι : Type ?u.595257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
⊢ Multiset.toFinset m ⊆ s → Multiset.prod m = ∏ i in s, i ^ Multiset.count i m
refine' Quot.induction_on m fun l => _
ι : Type ?u.595257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ Multiset.toFinset ↑l ⊆ s → List.prod l = ∏ x in s, x ^ List.count x l
ι : Type ?u.595257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ Multiset.toFinset (Quot.mk Setoid.r l) ⊆ s →
    Multiset.prod (Quot.mk Setoid.r l) = ∏ i in s, i ^ Multiset.count i (Quot.mk Setoid.r l)
simp only [quot_mk_to_coe'', coe_prod, coe_count]
no goals
ι : Type ?u.595257
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : Multiset α
s : Finset α
l : List α
⊢ Multiset.toFinset ↑l ⊆ s → List.prod l = ∏ x in s, x ^ List.count x l
apply prod_list_count_of_subset l s