simp (disch:=assumption) [bind, probability, Measure.bind_apply]
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2329
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
s : Set Y
hs : MeasurableSet s
hf : Measurable f
this : Measurable fun x => ↑(f x).μ
⊢ probability (bind x f) s = ∫⁻ (x' : X), probability (f x') s ∂↑x.μ
no goals