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

State before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
⊢ bind (bind x g) f = bind x fun x' => bind (g x') f
Tactic:
ext
State after:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (bind x g) f).μ s✝ = ↑↑↑(bind x fun x' => bind (g x') f).μ s✝

State before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (bind x g) f).μ s✝ = ↑↑↑(bind x fun x' => bind (g x') f).μ s✝
Tactic:
simp [bind]
State after:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑(Measure.bind (Measure.bind ↑x.μ fun x => ↑(g x).μ) fun x => ↑(f x).μ) s✝ =
    ↑↑(Measure.bind ↑x.μ fun x => Measure.bind ↑(g x).μ fun x => ↑(f x).μ) s✝

State before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑(Measure.bind (Measure.bind ↑x.μ fun x => ↑(g x).μ) fun x => ↑(f x).μ) s✝ =
    ↑↑(Measure.bind ↑x.μ fun x => Measure.bind ↑(g x).μ fun x => ↑(f x).μ) s✝
Tactic:
rw[Measure.bind_bind (m:=x.μ) (is_measurable hg) (is_measurable hf)]
State after:
no goals