no goals
α : Type u_1
β : Type ?u.163840
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type ?u.163859
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) i = ∫ (x : α) in i, f x ∂μ
rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]