no goals
E : Type ?u.1055778
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s✝ : Set E
f✝ : E → E
f'✝ : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
s : Set ℝ
f f' : ℝ → ℝ
inst✝ : CompleteSpace F
hs : MeasurableSet s
hf' : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ (∫ (x : ℝ) in f '' s, g x) = ∫ (x : ℝ) in s, abs (f' x) • g (f x)
simpa only [det_one_smulRight] using
  integral_image_eq_integral_abs_det_fderiv_smul volume hs
    (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g