no goals
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : Measurable f
⊢ ↑↑(bind m f) s = ∫⁻ (a : α), ↑↑(f a) s ∂m
rw [bind, join_apply hs, lintegral_map (measurable_coe hs) hf]