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

State before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.17225
inst✝ : MeasurableSpace Z
f : X → Rand Y
hf : Measurable f
x : X
⊢ bind (pure x) f = f x
Tactic:
ext
State after:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.17225
inst✝ : MeasurableSpace Z
f : X → Rand Y
hf : Measurable f
x : X
s✝ : Set Y
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (pure x) f).μ s✝ = ↑↑↑(f x).μ s✝

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

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