Theorem: SciLean.Rand.bind_mean (SciLean/Core/Rand/Rand.lean)

State before:
X Y : Type
Z : Type ?u.101457
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.101469
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.102666
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
f : X → Rand Y
⊢ mean (x >>= f) = x.𝔼 fun x' => mean (f x')
Tactic:
simp[mean,rand_push_E]
State after:
no goals