no goals
α : Type u_2
β : Type ?u.37787
m : MeasurableSpace α
μ ν : Measure α
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
⊢ withDensityᵥ μ (f - g) = withDensityᵥ μ f - withDensityᵥ μ g
rw [sub_eq_add_neg, sub_eq_add_neg, withDensityᵥ_add hf hg.neg, withDensityᵥ_neg]