awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
⊢ AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
have apply : ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) ≪ μ.restrict s
Tactic: apply h'f.mono_ac
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
⊢ Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s)
have h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
Tactic: have h''f : AEMeasurable f ((μ.restrict s).withDensity fun x => ENNReal.ofReal |(f' x).det|) := by
    apply h'f.mono_ac
    exact withDensity_absolutelyContinuous _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
⊢ Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s)
have apply : ∀ (t : Set E) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: apply Measure.ext fun t ht => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
Tactic: have h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s) := h'f.nullMeasurableSet_preimage ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det| : (a : Set E) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
  ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't,
    Measure.restrict_apply ht, restrict_restrict₀ h't,
    lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)
      (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
    image_preimage_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
rw :
  Eq (α := ℝ≥0∞)
    (((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det| : (a : Set E) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t
Tactic: rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't,
    Measure.restrict_apply ht, restrict_restrict₀ h't,
    lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)
      (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
    image_preimage_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
rw :
  Eq (α := ℝ≥0∞)
    (((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det| : (a : Set E) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s)
Tactic: rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't,
    Measure.restrict_apply ht, restrict_restrict₀ h't,
    lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)
      (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
    image_preimage_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
rw :
  Eq (α := ℝ≥0∞)
    (((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det| : (a : Set E) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t
rw₂ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rw₃ : ∫⁻ (a : E) in f ⁻¹' t ∩ s, ENNReal.ofReal |(f' a).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s)
Tactic: rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't,
    Measure.restrict_apply ht, restrict_restrict₀ h't,
    lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)
      (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
    image_preimage_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
rw :
  Eq (α := ℝ≥0∞)
    (((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det| : (a : Set E) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t
rw₂ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s)
rw₃ : ∫⁻ (a : E) in f ⁻¹' t ∩ s, ENNReal.ofReal |(f' a).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (f ⁻¹' t ∩ s)) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s) : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't,
    Measure.restrict_apply ht, restrict_restrict₀ h't,
    lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)
      (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
    image_preimage_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
h'f : AEMeasurable f (μ.restrict s)
h''f : AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)
t : Set E
ht : MeasurableSet t
h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s)
rw :
  Eq (α := ℝ≥0∞)
    (((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det| : (a : Set E) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t
rw₂ : ∫⁻ (a : E) in f ⁻¹' t, ENNReal.ofReal |(f' a).det| ∂μ.restrict s = (μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s)
rw₃ : ∫⁻ (a : E) in f ⁻¹' t ∩ s, ENNReal.ofReal |(f' a).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s)
rw₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (f ⁻¹' t ∩ s)) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) : Measure E) :
          (a : Set E) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((μ.restrict (f '' s) : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
have rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' s) : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable h''f ht, withDensity_apply₀ _ h't,
    Measure.restrict_apply ht, restrict_restrict₀ h't,
    lintegral_abs_det_fderiv_eq_addHaar_image₀ μ ((nullMeasurableSet_restrict hs).1 h't)
      (fun x hx => (hf' x hx.2).mono inter_subset_right) (hf.mono inter_subset_right),
    image_preimage_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ ∃ (u : E → E), Measurable u ∧ EqOn u f s
have refine : Measurable (s.piecewise (β := fun (a : E) ↦ E) f 0)
Tactic: refine ⟨piecewise s f 0, ?_, piecewise_eqOn _ _ _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ Measurable (s.piecewise (β := fun (a : E) ↦ E) f 0)
have refine : ContinuousOn f s
Tactic: refine ContinuousOn.measurable_piecewise ?_ continuous_zero.continuousOn hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ ContinuousOn f s
have this : DifferentiableOn ℝ f s
Tactic: have : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ ∃ (u : E → E), Measurable u ∧ EqOn u f s
have refine : Measurable (s.piecewise (β := fun (a : E) ↦ E) f 0)
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
refine : Measurable (s.piecewise (β := fun (a : E) ↦ E) f 0)
⊢ ∃ (u : E → E), Measurable u ∧ EqOn u f s
have refine₁ : ContinuousOn f s
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
refine : Measurable (s.piecewise (β := fun (a : E) ↦ E) f 0)
refine₁ : ContinuousOn f s
⊢ ∃ (u : E → E), Measurable u ∧ EqOn u f s
have refine₂ : ∀ (this : DifferentiableOn ℝ f s), ContinuousOn f s
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
have obtain : ∀ (u : E → E) (u_meas : Measurable u) (uf : EqOn u f s),
  Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ 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 (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
have u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x
Tactic: have u' : ∀ x ∈ s, HasFDerivWithinAt u (f' x) s x := fun x hx =>
    (hf' x hx).congr (fun y hy => uf hy) (uf hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ 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 ∈ s, HasFDerivWithinAt u (f' x) s x
⊢ Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
have hF : let F : (↑s : Type u_1) → E := u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s);
F = u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
Tactic: set F : s → E := u ∘ (↑) with hF
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ 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 ∈ s, HasFDerivWithinAt u (f' x) s x
F : (↑s : Type u_1) → E := u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
hF : F = u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
⊢ Measure.map F
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (u '' s)
have rw : Measure.map u ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) = μ.restrict (u '' s)
Tactic: rw [hF, ← Measure.map_map u_meas measurable_subtype_coe, map_comap_subtype_coe hs,
      restrict_withDensity hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ 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 ∈ s, HasFDerivWithinAt u (f' x) s x
F : (↑s : Type u_1) → E := u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
hF : F = u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
⊢ Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
have A : Measure.map F
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
  μ.restrict (u '' s)
Tactic: 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.nullMeasurableSet u' (hf.congr uf.symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ 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 ∈ s, HasFDerivWithinAt u (f' x) s x
F : (↑s : Type u_1) → E := u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
hF : F = u ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s)
A :
  Measure.map F
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (u '' s)
⊢ Measure.map (s.restrict (π := fun (a : E) ↦ E) f)
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
    μ.restrict (f '' s)
have A₁ : Measure.map F
    (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)) =
  μ.restrict (f '' s)
Tactic: rw [uf.image_eq] at A
Cleared hypotheses: A