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

State before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2329
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
s : Set Y
hs : MeasurableSet s
hf : Measurable f
⊢ probability (bind x f) s = ∫⁻ (x' : X), probability (f x') s ∂↑x.μ
Tactic:
have := is_measurable hf
State after:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2329
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
s : Set Y
hs : MeasurableSet s
hf : Measurable f
this : Measurable fun x => ↑(f x).μ
⊢ probability (bind x f) s = ∫⁻ (x' : X), probability (f x') s ∂↑x.μ

State before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2329
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
s : Set Y
hs : MeasurableSet s
hf : Measurable f
this : Measurable fun x => ↑(f x).μ
⊢ probability (bind x f) s = ∫⁻ (x' : X), probability (f x') s ∂↑x.μ
Tactic:
simp (disch:=assumption) [bind, probability, Measure.bind_apply]
State after:
no goals