. simp (disch:=sorry) only [bind,rand_simp]
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).val = (bind x fun x' => bind (g x') f).val

case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval