Theorem: SciLean.Prob.DRand.bindDR_bindDR (SciLean/Modules/Prob/DRand.lean)

State before:
R : Type ?u.32714
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x : DRand X
g : X → Rand Y
f : Y → Rand Z
⊢ bindDR (bindDR x g) f = bindDR x fun x' => Rand.bind (g x') f
Tactic:
simp (disch:=sorry) only [bindDR,rand_simp,rand_push_E]
State after:
no goals