no goals
α : Type u_1
β : Type ?u.1756534
γ : Type ?u.1756537
δ : Type ?u.1756540
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hg : Measurable g
⊢ withDensity μ (f + g) = withDensity μ f + withDensity μ g
simpa only [add_comm] using withDensity_add_left hg f