no goals
E : Type ?u.1050897
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' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ (x : ℝ), x ∈ s → HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ IntegrableOn g (f '' s) ↔ IntegrableOn (fun x => abs (f' x) • g (f x)) s
simpa only [det_one_smulRight] using
  integrableOn_image_iff_integrableOn_abs_det_fderiv_smul volume hs
    (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g