no goals
α : Type u_1
β : Type ?u.4775974
E : Type u_2
F : Type ?u.4775980
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4775986
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4890794
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
s : Set α
hf : AEMeasurable f
g : α → E
hs : MeasurableSet s
⊢ (∫ (a : α) in s, g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α) in s, f a • g a ∂μ
rw [restrict_withDensity hs, integral_withDensity_eq_integral_smul₀ hf]