no goals
α : Type u_1
β : Type u_2
γ : Type ?u.33924
δ : Type ?u.33927
inst✝ : MeasurableSpace α
f : α →ₛ β
μ : Measure α
⊢ ∑ y in SimpleFunc.range f, ↑↑μ (↑f ⁻¹' {y}) = ↑↑μ univ
rw [f.sum_measure_preimage_singleton, coe_range, preimage_range]