no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1258568
δ : Type ?u.1258571
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
s : Set β
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ (∫⁻ (y : β) in s, f y ∂Measure.map g μ) = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
rw [restrict_map hg hs, lintegral_map hf hg]