Theorem: Probly.DRand.dpure_action (Probly/DRand.lean)

State before:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
φ : X → ℝ
x dx : X
⊢ (dpure x dx).action φ = (fderiv ℝ φ x) dx
Tactic:
simp[Rand.dpure]
State after:
no goals