Theorem: Probly.FDRand.bind_bind (Probly/FDRand.lean)

State before:
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 = bind x fun x' => bind (g x') f
Tactic:
apply ext
State after:
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

State before:
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
Tactic:
. simp (disch:=sorry) only [bind,rand_simp]
State after:
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

State before:
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
Tactic:
. simp (disch:=sorry) only [bind,rand_simp]
State after:
no goals

State before:
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
Tactic:
simp (disch:=sorry) only [bind,rand_simp]
State after:
no goals

State before:
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
Tactic:
simp (disch:=sorry) only [bind,rand_simp]
State after:
no goals