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

State before:
X Y : Type
Z : Type ?u.95201
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : MeasurableSpace Y
R : Type ?u.95213
inst✝⁸ : RealScalar R
inst✝⁷ : AddCommGroup Y
inst✝⁶ : Module ℝ Y
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
U : Type ?u.96410
inst✝³ : AddCommGroup U
inst✝² : Module ℝ U
inst✝¹ : AddCommGroup X
inst✝ : Module ℝ X
x : Rand X
φ : X → Y
⊢ x.𝔼 φ = mean (x.map φ)
Tactic:
simp [bind,mean,pure,𝔼]
State after:
no goals