Theorem: SciLean.Prob.Rand.bind_pdf (SciLean/Modules/Prob/Rand.lean)

State before:
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
⊢ pdf R (bind x f) ν = fun y => ∫ (x' : X), pdf R (f x') ν y ∂↑x.μ
Tactic:
funext y
State after:
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.μ

State before:
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.μ
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.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.μ

State before:
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.μ
Tactic:
sorry
State after:
no goals