E : Type u_1
F : Type ?u.847296
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 μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : Measurable f
t : Set E
ht : MeasurableSet t
⊢ ↑↑(Measure.map f (withDensity (Measure.restrict μ s) fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x)))))
      t =
    ↑↑(Measure.restrict μ (f '' s)) t
E : Type u_1
F : Type ?u.847296
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 μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : Measurable f
⊢ Measure.map f (withDensity (Measure.restrict μ s) fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x)))) =
    Measure.restrict μ (f '' s)
apply Measure.ext fun t ht => ?_
no goals
E : Type u_1
F : Type ?u.847296
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 μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : Measurable f
t : Set E
ht : MeasurableSet t
⊢ ↑↑(Measure.map f (withDensity (Measure.restrict μ s) fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x)))))
      t =
    ↑↑(Measure.restrict μ (f '' s)) t
rw [map_apply h'f ht, withDensity_apply _ (h'f ht), Measure.restrict_apply ht,
  restrict_restrict (h'f ht),
  lintegral_abs_det_fderiv_eq_addHaar_image μ ((h'f ht).inter hs)
    (fun x hx => (hf' x hx.2).mono (inter_subset_right _ _)) (hf.mono (inter_subset_right _ _)),
  image_preimage_inter]