case intro.intro
E : Type u_1
F : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
E : Type u_1
F : Type ?u.850332
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
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
obtain ⟨u, u_meas, uf⟩ : ∃ u, Measurable u ∧ EqOn u f s := by
  classical
  refine' ⟨piecewise s f 0, _, piecewise_eqOn _ _ _⟩
  refine' ContinuousOn.measurable_piecewise _ continuous_zero.continuousOn hs
  have : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
  exact this.continuousOn
case intro.intro
E : Type u_1
F : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
case intro.intro
E : Type u_1
F : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
have u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x := fun x hx =>
  (hf' x hx).congr (fun y hy => uf hy) (uf hx)
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
case intro.intro
E : Type u_1
F : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
set F : s → E := u ∘ (↑) with hF
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (u '' s)
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
have A :
  Measure.map F (comap (↑) (μ.withDensity fun x => ENNReal.ofReal (|(f' x).det|))) =
    μ.restrict (u '' s) := by
  rw [hF, ← Measure.map_map u_meas measurable_subtype_coe, map_comap_subtype_coe hs,
    restrict_withDensity hs]
  exact map_withDensity_abs_det_fderiv_eq_addHaar μ hs u' (hf.congr uf.symm) u_meas
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (u '' s)
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
rw [uf.image_eq] at A
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
this : F = Set.restrict s f
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
have : F = s.restrict f := by
  ext x
  exact uf x.2
no goals
case intro.intro
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
this : F = Set.restrict s f
⊢ Measure.map (Set.restrict s f)
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
rwa [this] at A
no goals
E : Type u_1
F : Type ?u.850332
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
⊢ ∃ u, Measurable u ∧ EqOn u f s
classical
refine' ⟨piecewise s f 0, _, piecewise_eqOn _ _ _⟩
refine' ContinuousOn.measurable_piecewise _ continuous_zero.continuousOn hs
have : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
exact this.continuousOn
E : Type u_1
F : Type ?u.850332
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
⊢ Measurable (piecewise s f 0)
E : Type u_1
F : Type ?u.850332
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
⊢ ∃ u, Measurable u ∧ EqOn u f s
refine' ⟨piecewise s f 0, _, piecewise_eqOn _ _ _⟩
E : Type u_1
F : Type ?u.850332
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
⊢ ContinuousOn f s
E : Type u_1
F : Type ?u.850332
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
⊢ Measurable (piecewise s f 0)
refine' ContinuousOn.measurable_piecewise _ continuous_zero.continuousOn hs
E : Type u_1
F : Type ?u.850332
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
this : DifferentiableOn ℝ f s
⊢ ContinuousOn f s
E : Type u_1
F : Type ?u.850332
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
⊢ ContinuousOn f s
have : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
no goals
E : Type u_1
F : Type ?u.850332
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
this : DifferentiableOn ℝ f s
⊢ ContinuousOn f s
exact this.continuousOn
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
⊢ Measure.map u (withDensity (Measure.restrict μ s) fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x)))) =
    Measure.restrict μ (u '' s)
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
⊢ Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (u '' s)
rw [hF, ← Measure.map_map u_meas measurable_subtype_coe, map_comap_subtype_coe hs,
  restrict_withDensity hs]
no goals
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
⊢ Measure.map u (withDensity (Measure.restrict μ s) fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x)))) =
    Measure.restrict μ (u '' s)
exact map_withDensity_abs_det_fderiv_eq_addHaar μ hs u' (hf.congr uf.symm) u_meas
case h
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
x : ↑s
⊢ F x = Set.restrict s f x
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
⊢ F = Set.restrict s f
ext x
no goals
case h
E : Type u_1
F✝ : Type ?u.850332
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
u : E → E
u_meas : Measurable u
uf : EqOn u f s
u' : ∀ (x : E), x ∈ s → HasFDerivWithinAt u (f' x) s x
F : ↑s → E := u ∘ Subtype.val
hF : F = u ∘ Subtype.val
A :
  Measure.map F
      (Measure.comap Subtype.val (withDensity μ fun x => ENNReal.ofReal (abs (ContinuousLinearMap.det (f' x))))) =
    Measure.restrict μ (f '' s)
x : ↑s
⊢ F x = Set.restrict s f x
exact uf x.2