no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1688080
δ : Type ?u.1688083
m : MeasurableSpace α
μ ν✝ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set α
⊢ (∫⁻ (a : α) in s, f (g a) ∂μ) = ∫⁻ (b : β) in g '' s, f b ∂ν
rw [← hg.set_lintegral_comp_preimage_emb hge, preimage_image_eq _ hge.injective]