ι : Type ?u.942035
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ prod (map (fun x => id x) (toFinset S).val) ∣ prod S
ι : Type ?u.942035
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ Finset.prod (toFinset S) id ∣ prod S
rw [Finset.prod_eq_multiset_prod]
ι : Type ?u.942035
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ map (fun x => id x) (toFinset S).val ≤ S
ι : Type ?u.942035
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ prod (map (fun x => id x) (toFinset S).val) ∣ prod S
refine' Multiset.prod_dvd_prod_of_le _
no goals
ι : Type ?u.942035
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
S : Multiset α
⊢ map (fun x => id x) (toFinset S).val ≤ S
simp [Multiset.dedup_le S]