no goals
α : Type u_2
β : Type u_1
γ : Type ?u.19527
δ : Type ?u.19530
ι : Type ?u.19533
R : Type ?u.19536
R' : Type ?u.19539
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Finset β
f : α → β
hf : ∀ (y : β), y ∈ s → MeasurableSet (f ⁻¹' {y})
⊢ ∑ b in s, ↑↑μ (f ⁻¹' {b}) = ↑↑μ (f ⁻¹' ↑s)
simp only [← measure_biUnion_finset (pairwiseDisjoint_fiber f s) hf,
  Finset.set_biUnion_preimage_singleton]