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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
rw : ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ℕ), f '' (s ∩ u i)) : ℝ≥0∞)
| ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
rw [A, image_iUnion]

Premises used: Set.image_iUnion
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
conv_rhs :
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ℕ), f '' (s ∩ u i)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)

Tactic:
conv_rhs => rw [A, image_iUnion]

Premises used: Set.image_iUnion
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
hn : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (i : ℕ) ↦ f '' (s ∩ u i))
h : ∀ (i : ℕ), MeasurableSet (f '' (s ∩ u i))
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ℕ), f '' (s ∩ u i)) : ℝ≥0∞)

Tactic:
rw [measure_iUnion]

Premises used: MeasureTheory.measure_iUnion
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
i j : ℕ
hij : i ≠ j
apply : Disjoint (s ∩ u i) (s ∩ u j)
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint (fun (i : ℕ) ↦ f '' (s ∩ u i)) i j

Tactic:
apply Disjoint.image _ hf inter_subset_left inter_subset_left

Premises used: Set.inter_subset_left, Disjoint.image
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
i j : ℕ
hij : i ≠ j
⊢ Disjoint (s ∩ u i) (s ∩ u j)

Tactic:
Disjoint.mono inter_subset_right inter_subset_right
            (disjoint_disjointed _ hij)

Premises used: disjoint_disjointed, Disjoint.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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
i j : ℕ
hij : i ≠ j
⊢ Disjoint (s ∩ u i) (s ∩ u j)

Tactic:
exact
          Disjoint.mono inter_subset_right inter_subset_right
            (disjoint_disjointed _ hij)

Premises used: disjoint_disjointed, Disjoint.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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
i : ℕ
⊢ MeasurableSet (f '' (s ∩ u i))

Tactic:
measurable_image_of_fderivWithin (hs.inter (u_meas i))
            (fun x hx => (hf' x hx.1).mono inter_subset_left)
            (hf.mono inter_subset_left)

Premises used: MeasureTheory.measurable_image_of_fderivWithin, Set.inter_subset_left, And.left, Set.InjOn.mono, HasFDerivWithinAt.mono, MeasurableSet.inter
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
i : ℕ
⊢ MeasurableSet (f '' (s ∩ u i))

Tactic:
exact
          measurable_image_of_fderivWithin (hs.inter (u_meas i))
            (fun x hx => (hf' x hx.1).mono inter_subset_left)
            (hf.mono inter_subset_left)

Premises used: MeasureTheory.measurable_image_of_fderivWithin, Set.inter_subset_left, And.left, Set.InjOn.mono, HasFDerivWithinAt.mono, MeasurableSet.inter
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
x : ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
x₁ :
  LE.le (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ)
    (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)))
x₂ :
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
calc
    (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) =
        ∑' n, ∫⁻ x in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ := by
      conv_lhs => rw [A]
      rw [lintegral_iUnion]
      · intro n; exact hs.inter (u_meas n)
      · exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right
    _ ≤ ∑' n, μ (f '' (s ∩ u n)) := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply
        lintegral_abs_det_fderiv_le_addHaar_image_aux2 μ (hs.inter (u_meas n)) _
          (fun x hx => (hf' x hx.1).mono inter_subset_left) (hf.mono inter_subset_left)
      have : μ (u n) < ∞ :=
        lt_of_le_of_lt (measure_mono (disjointed_subset _ _)) (measure_spanningSets_lt_top μ n)
      exact ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)
    _ = μ (f '' s) := by
      conv_rhs => rw [A, image_iUnion]
      rw [measure_iUnion]
      · intro i j hij
        apply Disjoint.image _ hf inter_subset_left inter_subset_left
        exact
          Disjoint.mono inter_subset_right inter_subset_right
            (disjoint_disjointed _ hij)
      · intro i
        exact
          measurable_image_of_fderivWithin (hs.inter (u_meas i))
            (fun x hx => (hf' x hx.1).mono inter_subset_left)
            (hf.mono inter_subset_left)

Premises used: ENNReal.ofReal, abs, MeasureTheory.Measure.restrict, ContinuousLinearMap.det, Set.image, DFunLike.coe, MeasureTheory.lintegral
-- 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
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
le_antisymm (lintegral_abs_det_fderiv_le_addHaar_image μ hs hf' hf)
    (addHaar_image_le_lintegral_abs_det_fderiv μ hs hf')

Premises used: MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image, le_antisymm, MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv
-- 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
rcases :
  ∀ (t : Set E) (ts : t ⊆ s) (ht : MeasurableSet t) (t_eq_s : t =ᶠ[ae μ] s),
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (f '' s)
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
H : f '' s =ᶠ[ae μ] f '' t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' t) : ℝ≥0∞)

Tactic:
apply measure_congr

Premises used: MeasureTheory.measure_congr
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
H : f '' t ∪ f '' (s \ t) =ᶠ[ae μ] f '' t
⊢ f '' s =ᶠ[ae μ] f '' t

Tactic:
rw [this, image_union]

Premises used: Set.image_union
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s \ t)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f '' t ∪ f '' (s \ t) =ᶠ[ae μ] f '' t

Tactic:
refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)

Premises used: Iff.mpr, MeasureTheory.ae_eq_empty, MeasureTheory.union_ae_eq_left_of_ae_eq_empty
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' t) : ℝ≥0∞)

Tactic:
have A : μ (f '' s) = μ (f '' t) := by
    apply measure_congr
    have : s = t ∪ (s \ t) := by simp [union_eq_self_of_subset_left ts]
    rw [this, image_union]
    refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)
    apply addHaar_image_eq_zero_of_differentiableOn_of_addHaar_eq_zero _
      (fun x hx ↦ ?_) (ae_eq_set.1 t_eq_s).2
    exact (hf' x hx.1).differentiableWithinAt.mono diff_subset
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∫⁻ (x : E) in t, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
have B : (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ)
      = (∫⁻ x in t, ENNReal.ofReal |(f' x).det| ∂μ) :=
    setLIntegral_congr t_eq_s.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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
B : ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∫⁻ (x : E) in t, ENNReal.ofReal |(f' x).det| ∂μ
rw : ∀ x ∈ t, HasFDerivWithinAt f (f' x) t x
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
rw [A, B, lintegral_abs_det_fderiv_eq_addHaar_image _ ht _ (hf.mono ts)]

Premises used: MeasureTheory.lintegral_abs_det_fderiv_eq_addHaar_image, Set.InjOn.mono
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
B : ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∫⁻ (x : E) in t, ENNReal.ofReal |(f' x).det| ∂μ
x : E
hx : x ∈ t
⊢ HasFDerivWithinAt f (f' x) t x

Tactic:
(hf' x (ts hx)).mono ts

Premises used: HasFDerivWithinAt.mono
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
A : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' t) : ℝ≥0∞)
B : ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∫⁻ (x : E) in t, ENNReal.ofReal |(f' x).det| ∂μ
x : E
hx : x ∈ t
⊢ HasFDerivWithinAt f (f' x) t x

Tactic:
exact (hf' x (ts hx)).mono ts

Premises used: HasFDerivWithinAt.mono
-- 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
apply : ∀ (x : E) (hx : x ∈ s), ContinuousWithinAt f s x
⊢ AEMeasurable f (μ.restrict s)

Tactic:
apply ContinuousOn.aemeasurable₀ (fun x hx ↦ ?_) hs

Premises used: ContinuousOn.aemeasurable₀
-- 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
x : E
hx : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
(hf' x hx).differentiableWithinAt.continuousWithinAt

Premises used: DifferentiableWithinAt.continuousWithinAt, HasFDerivWithinAt.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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
x : E
hx : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
exact (hf' x hx).differentiableWithinAt.continuousWithinAt

Premises used: DifferentiableWithinAt.continuousWithinAt, HasFDerivWithinAt.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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ AEMeasurable f (μ.restrict s)

Tactic:
have h'f : AEMeasurable f (μ.restrict s) := by
    apply ContinuousOn.aemeasurable₀ (fun x hx ↦ ?_) hs
    exact (hf' x hx).differentiableWithinAt.continuousWithinAt
-- 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)
apply : ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) ≪ μ.restrict s
⊢ AEMeasurable f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|)

Tactic:
apply h'f.mono_ac

Premises used: AEMeasurable.mono_ac
-- 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)
⊢ ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) ≪ μ.restrict s

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- 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)
⊢ ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) ≪ μ.restrict s

Tactic:
exact withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- 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)
⊢ 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 _ _
-- 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|)
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∞)
⊢ Measure.map f ((μ.restrict s).withDensity fun (x : E) ↦ ENNReal.ofReal |(f' x).det|) = μ.restrict (f '' s)

Tactic:
apply Measure.ext fun t ht => ?_

Premises used: MeasureTheory.Measure.ext
-- 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
⊢ NullMeasurableSet (f ⁻¹' t) (μ.restrict s)

Tactic:
have h't : NullMeasurableSet (f ⁻¹' t) (μ.restrict s) := h'f.nullMeasurableSet_preimage ht