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 : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → ℝ≥0∞
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (μ.restrict s)

Tactic:
aemeasurable_ofReal_abs_det_fderivWithin μ hs hf'

Premises used: MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin
-- 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∞
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) (μ.restrict s)

Tactic:
exact aemeasurable_ofReal_abs_det_fderivWithin μ hs hf'

Premises used: MeasureTheory.aemeasurable_ofReal_abs_det_fderivWithin
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
rw :
  @Integrable _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s)) (g ∘ 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|)) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
⊢ IntegrableOn g (f '' s) μ ↔ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ

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

Premises used: MeasureTheory.measurableEmbedding_of_fderivWithin, MeasureTheory.IntegrableOn, MeasurableEmbedding.integrable_map_iff, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
simp :
  @Integrable _ _ _ (↑s : Type u_1) (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      ((g ∘ f) ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞))) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
⊢ @Integrable _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s)) (g ∘ 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|)) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ

Tactic:
simp only [Set.restrict_eq, ← Function.comp_assoc, ENNReal.ofReal]

Premises used: ENNReal.ofReal, Set.restrict_eq, Function.comp_assoc
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
rw :
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ
hf₁ : AEMeasurable (β := ℝ≥0) (fun (x : E) ↦ |(f' x).det|.toNNReal) (μ.restrict s)
⊢ @Integrable _ _ _ (↑s : Type u_1) (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      ((g ∘ f) ∘ Subtype.val (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞))) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ

Tactic:
rw [← (MeasurableEmbedding.subtype_coe hs).integrable_map_iff, map_comap_subtype_coe hs,
    restrict_withDensity hs, integrable_withDensity_iff_integrable_coe_smul₀]

Premises used: MeasureTheory.restrict_withDensity, MeasurableEmbedding.integrable_map_iff, MeasureTheory.integrable_withDensity_iff_integrable_coe_smul₀, map_comap_subtype_coe, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
simp_rw :
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) (μ.restrict s)
simp_rw₁ :
  Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ |(f' x).det| • (g ∘ f) x) (μ.restrict s) ↔
    Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) (μ.restrict s)
⊢ Integrable.{u_2, u_1} (ε := F) (fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x) (μ.restrict s) ↔
    IntegrableOn.{u_1, u_2} (ε := F) (fun (x : E) ↦ |(f' x).det| • g (f x)) s μ

Tactic:
simp_rw [IntegrableOn, Real.coe_toNNReal _ (abs_nonneg _), Function.comp_apply]

Premises used: MeasureTheory.IntegrableOn, Real.coe_toNNReal, Function.comp_apply, abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ AEMeasurable (β := ℝ≥0) (fun (x : E) ↦ |(f' x).det|.toNNReal) (μ.restrict s)

Tactic:
aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf'

Premises used: MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
⊢ AEMeasurable (β := ℝ≥0) (fun (x : E) ↦ |(f' x).det|.toNNReal) (μ.restrict s)

Tactic:
exact aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf'

Premises used: MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
rw :
  Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|))
      fun (x : (↑s : Type u_1)) ↦ g (s.restrict (π := fun (a : E) ↦ E) f x))
    (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in f '' s, g x ∂μ) (∫ (x : E) in s, |(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).integral_map]

Premises used: MeasurableEmbedding.integral_map, MeasureTheory.measurableEmbedding_of_fderivWithin, MeasureTheory.restrict_map_withDensity_abs_det_fderiv_eq_addHaar
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
simp :
  Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞)))
      fun (x : (↑s : Type u_1)) ↦ (g ∘ f) (↑x : E))
    (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s)) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|))
      fun (x : (↑s : Type u_1)) ↦ g (s.restrict (π := fun (a : E) ↦ E) f x))
    (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ)

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

Premises used: Set.restrict_apply, ENNReal.ofReal, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
rw :
  Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, |(f' x).det|.toNNReal • (g ∘ f) x ∂μ)
    (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : E) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : E) ↦ x ∈ s))
        (μ.withDensity fun (x : E) ↦ (↑|(f' x).det|.toNNReal : ℝ≥0∞)))
      fun (x : (↑s : Type u_1)) ↦ (g ∘ f) (↑x : E))
    (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)

Tactic:
rw [← (MeasurableEmbedding.subtype_coe hs).integral_map, map_comap_subtype_coe hs,
    setIntegral_withDensity_eq_setIntegral_smul₀
      (aemeasurable_toNNReal_abs_det_fderivWithin μ hs hf') _ hs]

Premises used: setIntegral_withDensity_eq_setIntegral_smul₀, MeasurableEmbedding.integral_map, MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin, map_comap_subtype_coe, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
e_f : ∀ (x : E), |(f' x).det|.toNNReal • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in s, |(f' x).det|.toNNReal • (g ∘ f) x ∂μ)
    (∫ (x : E) in s, |(f' x).det| • (g ∘ f) x ∂μ)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
g : E → F
x : E
e_f : (↑|(f' x).det|.toNNReal : ℝ) • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
e_f₁ e_f₂ : |(f' x).det| • (g ∘ f) x = |(f' x).det| • (g ∘ f) x
⊢ |(f' x).det|.toNNReal • (g ∘ f) x = |(f' x).det| • (g ∘ f) x

Tactic:
rw [NNReal.smul_def, Real.coe_toNNReal _ (abs_nonneg (f' x).det)]

Premises used: ContinuousLinearMap.det, Real.coe_toNNReal, NNReal.smul_def, abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
⊢ (↑f : E → E) '' f.source = f.target

Tactic:
have : f '' f.source = f.target := PartialEquiv.image_source_eq_target f.toPartialEquiv
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
this : (↑f : E → E) '' f.source = f.target
rw :
  Eq.{u_2 + 1} (α := F) (∫ (x : E) in (↑f : E → E) '' f.source, g x ∂μ)
    (∫ (x : E) in f.source, |(f' x).det| • g ((↑f : E → E) x) ∂μ)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in f.target, g x ∂μ) (∫ (x : E) in f.source, |(f' x).det| • g ((↑f : E → E) x) ∂μ)

Tactic:
rw [← this]
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
this : (↑f : E → E) '' f.source = f.target
apply : ∀ x ∈ f.source, HasFDerivWithinAt (↑f : E → E) (f' x) f.source x
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : E) in (↑f : E → E) '' f.source, g x ∂μ)
    (∫ (x : E) in f.source, |(f' x).det| • g ((↑f : E → E) x) ∂μ)

Tactic:
apply integral_image_eq_integral_abs_det_fderiv_smul μ f.open_source.measurableSet _ f.injOn

Premises used: MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, OpenPartialHomeomorph.open_source, IsOpen.measurableSet, OpenPartialHomeomorph.injOn
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
this : (↑f : E → E) '' f.source = f.target
x : E
hx : x ∈ f.source
⊢ HasFDerivWithinAt (↑f : E → E) (f' x) f.source x

Tactic:
(hf' x hx).hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
f' : E → E →L[ℝ] E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
f : OpenPartialHomeomorph E E
hf' : ∀ x ∈ f.source, HasFDerivAt (↑f : E → E) (f' x) x
g : E → F
this : (↑f : E → E) '' f.source = f.target
x : E
hx : x ∈ f.source
⊢ HasFDerivWithinAt (↑f : E → E) (f' x) f.source x

Tactic:
exact (hf' x hx).hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt
-- 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 : MeasurableEmbedding f
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
rw :
  ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ) =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)
⊢ ((Measure.comap f (μ.withDensity fun (x : E) ↦ ENNReal.ofReal (g x)) : Measure E) : (a : Set E) → ℝ≥0∞) s =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Tactic:
rw [Measure.comap_apply f hf.injective (fun t ht ↦ hf.measurableSet_image' ht) _ hs,
    withDensity_apply _ (hf.measurableSet_image' hs),
    ← ofReal_integral_eq_lintegral_ofReal hg_int
      ((ae_restrict_iff' (hf.measurableSet_image' hs)).mpr hg),
    integral_image_eq_integral_abs_det_fderiv_smul μ hs hf' hf.injective.injOn]

Premises used: Iff.mpr, MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, Function.Injective.injOn, MeasurableEmbedding.measurableSet_image', MeasureTheory.Measure.comap_apply, MeasurableEmbedding.injective, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, MeasureTheory.ae_restrict_iff', MeasureTheory.withDensity_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 : MeasurableEmbedding f
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ) =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Tactic:
simp_rw [smul_eq_mul]

Premises used: smul_eq_mul
-- 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 →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
f : E ≃ᵐ E
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, Membership.mem (γ := Set E) ((⇑f : (a : E) → E) '' s) x → 0 ≤ g x
hg_int : IntegrableOn g ((⇑f : (a : E) → E) '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt (⇑f : (a : E) → E) (f' x) s x
rw :
  ((Measure.comap (⇑f : (a : E) → E) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal (g x)) : Measure E) :
        (a : Set E) → ℝ≥0∞)
      s =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g ((f : (a : E) → E) x) ∂μ)
rw₁ rw₂ :
  ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g ((f : (a : E) → E) x) ∂μ) =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g ((f : (a : E) → E) x) ∂μ)
⊢ ((Measure.map (⇑f.symm : (a : E) → E) (μ.withDensity fun (x : E) ↦ ENNReal.ofReal (g x)) : Measure E) :
        (a : Set E) → ℝ≥0∞)
      s =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g ((f : (a : E) → E) x) ∂μ)

Tactic:
rw [MeasurableEquiv.map_symm,
    MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul μ hs
      f.measurableEmbedding hg hg_int hf']

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, MeasurableEquiv.map_symm
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → ℝ≥0∞
⊢ ∫⁻ (x : ℝ) in f '' s, g x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal |f' x| * g (f x)

Tactic:
simpa only [det_toSpanSingleton] using
    lintegral_image_eq_lintegral_abs_det_fderiv_mul volume hs
      (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g

Premises used: HasDerivWithinAt.hasFDerivWithinAt, ContinuousLinearMap.det_toSpanSingleton, MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' s) volume ↔
    IntegrableOn.{0, u_1} (ε := F) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ |f' x| • g (f x)) s volume

Tactic:
simpa only [det_toSpanSingleton] using
    integrableOn_image_iff_integrableOn_abs_det_fderiv_smul volume hs
      (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g

Premises used: MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul, HasDerivWithinAt.hasFDerivWithinAt, ContinuousLinearMap.det_toSpanSingleton, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ Eq.{u_1 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (f '' s)) fun (x : ℝ) ↦ g x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ℝ) ↦ |f' x| • g (f x))

Tactic:
simpa only [det_toSpanSingleton] using
    integral_image_eq_integral_abs_det_fderiv_smul volume hs
      (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g

Premises used: MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul, HasDerivWithinAt.hasFDerivWithinAt, ContinuousLinearMap.det_toSpanSingleton, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
⊢ a.Countable

Tactic:
have a_count : a.Countable :=
    countable_setOf_isolated_right_within.union countable_setOf_isolated_left_within
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
⊢ MeasurableSet s₁

Tactic:
have hs₁ : MeasurableSet s₁ := hs.diff a_count.measurableSet
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
⊢ u.Countable

Tactic:
have hu : Set.Countable u := MonotoneOn.countable_setOf_two_preimages (hf.mono diff_subset)
-- Module: Mathlib.MeasureTheory.Function.JacobianOneDim
Goal:
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf : MonotoneOn f s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : Set ℝ := {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ∪ {x : ℝ | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}
a_count : a.Countable
s₁ : Set ℝ := s \ a
hs₁ : MeasurableSet s₁
u : Set ℝ := {c : ℝ | ∃ (x : ℝ) (y : ℝ), x ∈ s₁ ∧ y ∈ s₁ ∧ x < y ∧ f x = c ∧ f y = c}
hu : u.Countable
b : Set ℝ := s₁ ∩ f ⁻¹' u
h : ∀ (x : ℝ), x ∈ b ↔ Membership.mem (γ := Set ℝ) (⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}) x
⊢ b = ⋃ z ∈ u, s₁ ∩ f ⁻¹' {z}

Tactic:
ext