simp (disch := first | apply hf | apply hg) only [rand_simp,randDeriv_comp]
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ { val := (fun x => f (g x)) x, dval := randDeriv (fun x => f (g x)) x dx } =
    let ydy := (g x, (fderiv ℝ g x) dx);
    { val := f ydy.1, dval := randDeriv f ydy.1 ydy.2 }
no goals