α : Type u_1
β : Type ?u.53685
ι : Type ?u.53688
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (sum f fun a n => n • {a}) = sum f fun x n => Multiset.count a (n • {x})
α : Type u_1
β : Type ?u.53685
ι : Type ?u.53688
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (↑toMultiset f) = sum f fun x n => Multiset.count a (n • {x})
rw [toMultiset_apply]
no goals
α : Type u_1
β : Type ?u.53685
ι : Type ?u.53688
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (sum f fun a n => n • {a}) = sum f fun x n => Multiset.count a (n • {x})
exact map_sum (Multiset.countAddMonoidHom a) _ f.support
no goals
α : Type u_1
β : Type ?u.53685
ι : Type ?u.53688
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ (sum f fun x n => Multiset.count a (n • {x})) = sum f fun x n => n * Multiset.count a {x}
simp only [Multiset.count_nsmul]
no goals
α : Type u_1
β : Type ?u.53685
ι : Type ?u.53688
inst✝ : DecidableEq α
f : α →₀ ℕ
a a' : α
x✝ : a' ∈ f.support
H : a' ≠ a
⊢ (fun x n => n * Multiset.count a {x}) a' (↑f a') = 0
simp only [Multiset.count_singleton, if_false, H.symm, mul_zero]
no goals
α : Type u_1
β : Type ?u.53685
ι : Type ?u.53688
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
H : ¬a ∈ f.support
⊢ (fun x n => n * Multiset.count a {x}) a (↑f a) = 0
simp only [not_mem_support_iff.1 H, zero_mul]
no goals
α : Type u_1
β : Type ?u.53685
ι : Type ?u.53688
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ↑f a * Multiset.count a {a} = ↑f a
rw [Multiset.count_singleton_self, mul_one]