Densities and pushforwards

Reweighting a measure by a density that factors through a map and then pushing forward along the map is reweighting the pushforward by the factor. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/WithDensity.lean.

theorem MeasureTheory.Measure.map_withDensity_comp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure α} {f : β → ENNReal} {g : α → β} (hf : AEMeasurable f (map g μ)) (hg : AEMeasurable g μ) : map g (μ.withDensity (f ∘ g)) = (map g μ).withDensity f

The pushforward along g of a measure with density f ∘ g is the pushforward with density f.