∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Fintype β]
  {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) →
    (∀ (i : β), MeasurableSet (f i)) →
      autoParam (∀ (i : β), μ (f i) ≠ ⊤) MeasureTheory.measureReal_iUnion_fintype._auto_1 →
        μ.real (⋃ b, f b) = ∑ p, μ.real (f p)