simp (disch:=sorry) [mean,expectedValue,E,hφ]
X : Type
inst✝⁸ : MeasurableSpace X
Y : Type
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.27192
inst✝⁶ : MeasurableSpace Z
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace ℝ X
inst✝³ : NormedAddCommGroup Y
inst✝² : NormedSpace ℝ Y
inst✝¹ : NormedAddCommGroup Z
inst✝ : NormedSpace ℝ Z
x : Rand X
φ : X → Y
hφ : Measurable φ
⊢ E x φ =
    mean
      (let x' ~ x
      pure (φ x'))
no goals