simp[mean,rand_push_E]
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')
no goals