Theorem: Probly.Rand.bind_pdf (Probly/Rand.lean)

State before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
⊢ pdf' (bind x f) ν = fun y => ∫ (x' : X), pdf' (f x') ν y ∂↑x.μ
Tactic:
funext y
State after:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf' (bind x f) ν y = ∫ (x' : X), pdf' (f x') ν y ∂↑x.μ

State before:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf' (bind x f) ν y = ∫ (x' : X), pdf' (f x') ν y ∂↑x.μ
Tactic:
simp[Rand.pdf',Rand.bind,Rand.pure]
State after:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ ENNReal.toReal (Measure.rnDeriv (Measure.bind ↑x.μ fun x => ↑(f x).μ) ν y) =
    ∫ (x' : X), ENNReal.toReal (Measure.rnDeriv (↑(f x').μ) ν y) ∂↑x.μ

State before:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ ENNReal.toReal (Measure.rnDeriv (Measure.bind ↑x.μ fun x => ↑(f x).μ) ν y) =
    ∫ (x' : X), ENNReal.toReal (Measure.rnDeriv (↑(f x').μ) ν y) ∂↑x.μ
Tactic:
sorry
State after:
no goals