Theorem: SciLean.Rand.bind_pull_mean (SciLean/Core/Rand/PushPullExpectation.lean)

State before:
R : Type ?u.1821
inst✝⁸ : RealScalar R
X : Type
inst✝⁷ : MeasurableSpace X
inst✝⁶ : AddCommGroup X
inst✝⁵ : Module ℝ X
Y : Type
inst✝⁴ : AddCommGroup Y
inst✝³ : Module ℝ Y
inst✝² : MeasurableSpace Y
Z : Type ?u.3033
inst✝¹ : AddCommGroup Z
inst✝ : Module ℝ Z
x : Rand X
f : X → Rand Y
⊢ (mean do
      let x' ← x
      pure (mean (f x'))) =
    mean (x >>= f)
Tactic:
simp[rand_push_E]
State after:
no goals