simp[Rand.pdf,Rand.bind,Rand.pure]
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.46786
inst✝¹ : MeasurableSpace Z
R : Type u_1
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf R (bind x f) ν y = ∫ (x' : X), pdf R (f x') ν y ∂↑x.μ
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.46786
inst✝¹ : MeasurableSpace Z
R : Type u_1
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ Scalar.ofReal R ((Measure.bind ↑x.μ fun x => ↑(f x).μ).rnDeriv ν y).toReal =
    ∫ (x' : X), Scalar.ofReal R ((↑(f x').μ).rnDeriv ν y).toReal ∂↑x.μ