convert h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ x ∈ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this, f x = 1
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this = univ