Theorem: SciLean.Rand.pure_𝔼 (SciLean/Core/Rand/Rand.lean)

State before:
X : Type
Y : Type u_1
Z : Type ?u.67988
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.68000
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.69197
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
x : X
φ : X → Y
⊢ (pure x).𝔼 φ = φ x
Tactic:
simp [𝔼]
State after:
no goals