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

State before:
X Y : Type
Z : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.70233
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.71430
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
f : X → Rand Y
φ : Y → Z
⊢ (r >>= f).𝔼 φ = r.𝔼 fun x' => (f x').𝔼 φ
Tactic:
simp[𝔼]
State after:
X Y : Type
Z : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.70233
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.71430
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
f : X → Rand Y
φ : Y → Z
⊢ ∫' x, φ x ∂(r >>= f).ℙ = ∫' x, ∫' x, φ x ∂(f x).ℙ ∂r.ℙ

State before:
X Y : Type
Z : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : MeasurableSpace Y
R : Type ?u.70233
inst✝⁶ : RealScalar R
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module ℝ Y
inst✝³ : AddCommGroup Z
inst✝² : Module ℝ Z
U : Type ?u.71430
inst✝¹ : AddCommGroup U
inst✝ : Module ℝ U
r : Rand X
f : X → Rand Y
φ : Y → Z
⊢ ∫' x, φ x ∂(r >>= f).ℙ = ∫' x, ∫' x, φ x ∂(f x).ℙ ∂r.ℙ
Tactic:
sorry_proof
State after:
no goals