simp only [randDeriv, fderiv_const, Pi.zero_apply,
           ContinuousLinearMap.zero_apply, DRand.action_zero]
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.3752
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3869
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3986
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.4109
inst✝ : MeasurableSpace β
a : Rand α
w dw : W
φ : α → ℝ
⊢ (randDeriv (fun x => a) w dw).action φ = 0.action φ
no goals