exact tsum_eq_sum fun _ h ↦ (h $ mem_univ _).elim
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (∑' (a : α), if b = g a then f a else 0) = ∑ a : α, if b = g a then f a else 0
no goals