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

State before:
X : Type
Y : Type u_1
Z : Type ?u.82732
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.82744
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.83941
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
φ : X → ℝ
y : Y
⊢ (r.𝔼 fun x' => φ x' • y) = r.𝔼 φ • y
Tactic:
sorry_proof
State after:
no goals