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

State before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : MeasurableSpace Y
Z : Type u_1
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.27216
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
f : X → Rand Y
φ : Y → Z
⊢ E (bind x f) φ = E x fun x' => E (f x') φ
Tactic:
simp (disch:=sorry) only [E,rand_simp]
State after:
no goals