sorry
case h
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 : Rand X
f : X → DRand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (∫ (x' : X), (f x').action φ ∂↑x.μ) • y = ∫ (x' : X), ((f x').action fun x => φ x) • y ∂↑x.μ
no goals