rw [← tsum_fintype]
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f✝ g : α → ℕ∞
inst✝ : Fintype ι
f : α → ℕ∞
t : ι → Set α
⊢ ∑' (x : ↑(⋃ i, t i)), f ↑x ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x