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