Theorem: Probly.Rand.expectedValue_smul (Probly/Rand.lean)

State before:
X : Type
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.23797
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 : Y
⊢ (E x fun x' => φ x' • y) = E x φ • y
Tactic:
sorry
State after:
no goals