funext w dw
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
⊢ (randDeriv fun w =>
      let x ~ x w
      f w x) =
    fun w dw =>
    (DRand.bindDR (randDeriv x w dw) fun x => f w x) + bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw
case h.h
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
⊢ randDeriv
      (fun w =>
        let x ~ x w
        f w x)
      w dw =
    (DRand.bindDR (randDeriv x w dw) fun x => f w x) + bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw