Theorem: Probly.FDRand.bind_pure
Proof state before:
case a
X✝ : Type ?u.6645
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.6763
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.6880
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
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.val =
    { val := (f x).val, dval := randDeriv (fun x' => (f x').val) x dx + (f x).dval }.val

case a
X✝ : Type ?u.6645
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.6763
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.6880
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
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval
Tactic:
. simp (disch:=sorry) only [rand_simp]
Proof state after:
case a
X✝ : Type ?u.6645
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.6763
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.6880
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
f : X → FDRand Y
x dx : X
⊢ {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval =
    {
        val :=
          let x' ~ Rand.pure x
          (f x').val,
        dval := (DRand.bindDR (dpure x dx) fun x' => (f x').val) + bindRD (Rand.pure x) fun x' => (f x').dval }.dval