Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule (Probly/RandFwdDeriv.lean)

State before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
⊢ (randFwdDeriv fun w => Rand.pure (x w)) = fun w dw => fdpure (x w) ((fderiv ℝ x w) dw)
Tactic:
unfold randFwdDeriv fdpure
State after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
⊢ (fun x_1 dx => { val := (fun w => Rand.pure (x w)) x_1, dval := randDeriv (fun w => Rand.pure (x w)) x_1 dx }) =
    fun w dw => { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }

State before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
⊢ (fun x_1 dx => { val := (fun w => Rand.pure (x w)) x_1, dval := randDeriv (fun w => Rand.pure (x w)) x_1 dx }) =
    fun w dw => { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Tactic:
simp (disch:=first | apply hx | sorry) only [rand_simp]
State after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
⊢ (fun x_1 dx =>
      { val := Rand.pure (x x_1), dval := randDeriv Rand.pure (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun w dw => { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }

State before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
⊢ (fun x_1 dx =>
      { val := Rand.pure (x x_1), dval := randDeriv Rand.pure (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun w dw => { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Tactic:
funext w dw
State after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ { val := Rand.pure (x w), dval := randDeriv Rand.pure (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }

State before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ { val := Rand.pure (x w), dval := randDeriv Rand.pure (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Tactic:
rw [Rand.pure.arg_x.randDeriv_rule _ differentiable_id']
State after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ { val := Rand.pure (x w),
      dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }

State before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ { val := Rand.pure (x w),
      dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Tactic:
simp
State after:
no goals