no goals
α : Type u_2
β : Type u_1
γ : Type ?u.18843
δ : Type ?u.18846
ι : Type ?u.18849
R : Type ?u.18852
R' : Type ?u.18855
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
s : Set β
hs : Set.Countable s
f : α → β
hf : ∀ (y : β), y ∈ s → MeasurableSet (f ⁻¹' {y})
⊢ (∑' (b : ↑s), ↑↑μ (f ⁻¹' {↑b})) = ↑↑μ (f ⁻¹' s)
rw [← Set.biUnion_preimage_singleton, measure_biUnion hs (pairwiseDisjoint_fiber f s) hf]