rw[Measure.bind_bind (m:=x.μ) (is_measurable hg) (is_measurable hf)]
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑(Measure.bind (Measure.bind ↑x.μ fun x => ↑(g x).μ) fun x => ↑(f x).μ) s✝ =
    ↑↑(Measure.bind ↑x.μ fun x => Measure.bind ↑(g x).μ fun x => ↑(f x).μ) s✝
no goals