awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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∞)
rw₅ rw₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (t ∩ f '' 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∞)

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]

Premises used: MeasureTheory.Measure.restrict_restrict₀, MeasureTheory.Measure.restrict_apply, Set.image_preimage_inter, MeasureTheory.withDensity_apply₀, And.right, MeasureTheory.nullMeasurableSet_restrict, MeasureTheory.Measure.map_apply_of_aemeasurable, Iff.mp, Set.InjOn.mono, MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image₀, HasFDerivWithinAt.mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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

Tactic:
⟨piecewise s f 0, ?_, piecewise_eqOn _ _ _⟩

Premises used: Set.piecewise_eqOn, And.intro, Exists.intro, Set.piecewise, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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

Tactic:
refine ⟨piecewise s f 0, ?_, piecewise_eqOn _ _ _⟩
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)

Tactic:
ContinuousOn.measurable_piecewise ?_ continuous_zero.continuousOn hs

Premises used: Continuous.continuousOn, continuous_zero, ContinuousOn.measurable_piecewise
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 : ContinuousOn f s
⊢ Measurable (s.piecewise (β := fun (a : E) ↦ E) f 0)

Tactic:
refine ContinuousOn.measurable_piecewise ?_ continuous_zero.continuousOn hs

Premises used: Continuous.continuousOn, continuous_zero, ContinuousOn.measurable_piecewise
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ DifferentiableOn ℝ f s

Tactic:
have : DifferentiableOn ℝ f s := fun x hx => (hf' x hx).differentiableWithinAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
this : DifferentiableOn ℝ f s
⊢ ContinuousOn f s

Tactic:
this.continuousOn

Premises used: DifferentiableOn.continuousOn
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
this : DifferentiableOn ℝ f s
⊢ ContinuousOn f s

Tactic:
exact this.continuousOn

Premises used: DifferentiableOn.continuousOn
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
refine₂ : ∀ (this : DifferentiableOn ℝ f s), ContinuousOn f s
⊢ ∃ (u : E → E), Measurable u ∧ EqOn u 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
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ ∀ 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)
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)
rw : Measure.map u ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) = μ.restrict (u '' 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)

Tactic:
rw [hF, ← Measure.map_map u_meas measurable_subtype_coe, map_comap_subtype_coe hs,
      restrict_withDensity hs]

Premises used: measurable_subtype_coe, MeasureTheory.restrict_withDensity, map_comap_subtype_coe, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 u ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) = μ.restrict (u '' s)

Tactic:
map_withDensity_abs_det_fderiv_eq_addHaar μ hs.nullMeasurableSet u' (hf.congr uf.symm)

Premises used: MeasurableSet.nullMeasurableSet, Set.InjOn.congr, Set.EqOn.symm, MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 u ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) = μ.restrict (u '' s)

Tactic:
exact map_withDensity_abs_det_fderiv_eq_addHaar μ hs.nullMeasurableSet u' (hf.congr uf.symm)

Premises used: MeasurableSet.nullMeasurableSet, Set.InjOn.congr, Set.EqOn.symm, MeasureTheory.map_withDensity_abs_det_fderiv_eq_addHaar
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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)

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)
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 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

Premises used: Set.EqOn.image_eq
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 (f '' s)
h : ∀ (x : (↑s : Type u_1)), F x = s.restrict (π := fun (a : E) ↦ E) f x
⊢ F = s.restrict (π := fun (a : E) ↦ E) f

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 (f '' s)
x : (↑s : Type u_1)
⊢ F x = s.restrict (π := fun (a : E) ↦ E) f x

Tactic:
uf x.2

Premises used: Set.restrict, Subtype.property
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 (f '' s)
x : (↑s : Type u_1)
⊢ F x = s.restrict (π := fun (a : E) ↦ E) f x

Tactic:
exact uf x.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 (f '' s)
⊢ F = s.restrict (π := fun (a : E) ↦ E) f

Tactic:
have : F = s.restrict f := by
    ext x
    exact uf x.2
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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 (f '' s)
this : F = s.restrict (π := fun (a : E) ↦ E) f
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (A :
      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))
    (this : F = s.restrict (π := fun (a : E) ↦ E) f),
    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)
⊢ 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:
rwa [this] at A
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
g : E → ℝ≥0∞
rw :
  ∫⁻ (a : (↑s : Type u_1)),
      g
        (s.restrict (π := fun (a : E) ↦ E) f
          a) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
⊢ ∫⁻ (x : E) in f '' s, g x ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ

Tactic:
rw [← restrict_map_withDensity_abs_det_fderiv_eq_addHaar μ hs hf' hf,
    (measurableEmbedding_of_fderivWithin hs hf' hf).lintegral_map]

Premises used: MeasureTheory.measurableEmbedding_of_fderivWithin, MeasurableEmbedding.lintegral_map, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
g : E → ℝ≥0∞
simp :
  ∫⁻ (a : (↑s : Type u_1)),
      (g ∘ f)
        (↑a :
          E) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
⊢ ∫⁻ (a : (↑s : Type u_1)),
      g
        (s.restrict (π := fun (a : E) ↦ E) f
          a) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ

Tactic:
simp only [Set.restrict_apply, ← Function.comp_apply (f := g)]

Premises used: Set.restrict_apply, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
g : E → ℝ≥0∞
rw :
  ∫⁻ (a : E) in s, HMul.hMul (α := E → ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (g ∘ f) a ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ
rw₁ : ∀ᵐ (x : E) ∂μ.restrict s, ENNReal.ofReal |(f' x).det| < ∞
rw₂ : AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (μ.restrict s)
⊢ ∫⁻ (a : (↑s : Type u_1)),
      (g ∘ f)
        (↑a :
          E) ∂Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ

Tactic:
rw [← (MeasurableEmbedding.subtype_coe hs).lintegral_map, map_comap_subtype_coe hs,
    setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]

Premises used: MeasurableEmbedding.lintegral_map, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀, map_comap_subtype_coe, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
g : E → ℝ≥0∞
⊢ ∫⁻ (a : E) in s, HMul.hMul (α := E → ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (g ∘ f) a ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * (g ∘ f) x ∂μ

Tactic:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Function.Jacobian
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
g : E → ℝ≥0∞
⊢ ∀ᵐ (x : E) ∂μ.restrict s, ENNReal.ofReal |(f' x).det| < ∞

Tactic:
simp only [eventually_true, ENNReal.ofReal_lt_top]

Premises used: ENNReal.ofReal_lt_top, Filter.eventually_true