ι : Type ?u.936144
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : DecidableEq α
s : Finset β
a : α
f : β → Multiset α
⊢ count a (sum (map (fun x => f x) s.val)) = sum (map (fun x => count a (f x)) s.val)
ι : Type ?u.936144
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : DecidableEq α
s : Finset β
a : α
f : β → Multiset α
⊢ count a (∑ x in s, f x) = ∑ x in s, count a (f x)
dsimp only [Finset.sum]
no goals
ι : Type ?u.936144
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : DecidableEq α
s : Finset β
a : α
f : β → Multiset α
⊢ count a (sum (map (fun x => f x) s.val)) = sum (map (fun x => count a (f x)) s.val)
rw [count_sum]