have :
  ((univ : Finset β) : Set β).PairwiseDisjoint fun b ↦
    univ.filter fun a : α ↦ g a = b := by
  refine' fun b₁ _ b₂ _ hb ↦ disjoint_left.2 fun a ha₁ ha₂ ↦ _
  simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂
  exact hb (ha₁.symm.trans ha₂)
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1
α : 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
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1