unfold randFwdDeriv
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (randFwdDeriv fun w => flip (x w)) = fun w dw =>
    let x' := x w;
    let dx' := (fderiv ℝ x w) dw;
    { val := flip x', dval := dx' • dflip }
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.33480
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.33597
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.33714
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.33831
inst✝¹ : MeasurableSpace α
β : Type ?u.33837
inst✝ : MeasurableSpace β
x : W → ℝ
hf : Differentiable ℝ x
⊢ (fun x_1 dx => { val := (fun w => flip (x w)) x_1, dval := randDeriv (fun w => flip (x w)) x_1 dx }) = fun w dw =>
    let x' := x w;
    let dx' := (fderiv ℝ x w) dw;
    { val := flip x', dval := dx' • dflip }