no goals
α : Type u_2
β✝ : Type ?u.136486
E : Type u_3
F : Type ?u.136492
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g✝ : α → E
s✝ t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
β : Type u_1
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → E
s : Set β
⊢ (∫ (y : β) in s, g y ∂Measure.map f μ) = ∫ (x : α) in f ⁻¹' s, g (f x) ∂μ
rw [hf.restrict_map, hf.integral_map]