simp [h]
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
h : c
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv f w dw
no goals