no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1687278
δ : Type ?u.1687281
m : MeasurableSpace α
μ ν✝ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g
s : Set β
hs : MeasurableSet s
f : β → ℝ≥0∞
hf : Measurable f
⊢ (∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ) = ∫⁻ (b : β) in s, f b ∂ν
rw [← hg.map_eq, set_lintegral_map hs hf hg.measurable]