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

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

State before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf (bind x f) ν y = ∫ (x' : X), rpdf (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.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf
      { μ := erase (Measure.bind ↑x.μ fun x => ↑(f x).μ), is_prob := ⋯,
        rand := do
          let __do_lift ← x.rand
          (f __do_lift).rand }
      ν y =
    ∫ (x' : X), rpdf (f x') ν y ∂↑x.μ

State before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf
      { μ := erase (Measure.bind ↑x.μ fun x => ↑(f x).μ), is_prob := ⋯,
        rand := do
          let __do_lift ← x.rand
          (f __do_lift).rand }
      ν y =
    ∫ (x' : X), rpdf (f x') ν y ∂↑x.μ
Tactic:
sorry
State after:
no goals