apply DRand.ext
case h.h
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ randDeriv (fun x => f (g x)) x dx =
    let ydy := (g x, (fderiv ℝ g x) dx);
    randDeriv f ydy.1 ydy.2
case h.h.a
R : Type ?u.6471
inst✝¹⁸ : RealScalar R
W : Type ?u.6477
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type u_2
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type u_1
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type ?u.7444
inst✝¹ : MeasurableSpace α
β : Type ?u.7450
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ ∀ (φ : Z → ℝ),
    (randDeriv (fun x => f (g x)) x dx).action φ =
      (let ydy := (g x, (fderiv ℝ g x) dx);
          randDeriv f ydy.1 ydy.2).action
        φ