no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1686621
δ : Type ?u.1686624
m : MeasurableSpace α
μ ν✝ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g
f : β → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α), f (g a) ∂μ) = ∫⁻ (b : β), f b ∂ν
rw [← hg.map_eq, lintegral_map hf hg.measurable]