no goals
α : Type u_1
β : Type ?u.1801194
γ : Type ?u.1801197
δ : Type ?u.1801200
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (x : α) in s, g x ∂Measure.withDensity μ f) = ∫⁻ (x : α) in s, (f * g) x ∂μ
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul _ hf hg]