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 : 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)
rw : s = s ∩ ⋃ (i : ℕ), u i
rw₁ : s = s ∩ ⋃ (i : ℕ), spanningSets μ i
rw₂ : s = s ∩ univ
⊢ s = ⋃ (n : ℕ), s ∩ u n
have rw₃ : s = s
Tactic: rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have A : s = ⋃ (n : ℕ), s ∩ u n
Tactic: have A : s = ⋃ n, s ∩ u n := by
    rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
| ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
have rw : ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
Tactic: rw [A]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
have conv_lhs : ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ =
  ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
Tactic: conv_lhs => rw [A]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
have hm : ∀ (i : ℕ), MeasurableSet (s ∩ u i)
Tactic: rw [lintegral_iUnion]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
hm : ∀ (i : ℕ), MeasurableSet (s ∩ u i)
⊢ ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
have hd : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ u n)
Tactic: rw [lintegral_iUnion]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ)
    (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)))
have apply : ∀ (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n))
Tactic: apply ENNReal.tsum_le_tsum fun n => ?_
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
⊢ ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n))
have lintegral_abs_det_fderiv_le_addHaar_image_aux2 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: 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)
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
have this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have : μ (u n) < ∞ :=
        lt_of_le_of_lt (measure_mono (disjointed_subset _ _)) (measure_spanningSets_lt_top μ n)
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
| ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have rw : ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ℕ), f '' (s ∩ u i)) : ℝ≥0∞)
Tactic: rw [A, image_iUnion]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
have conv_rhs : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ℕ), f '' (s ∩ u i)) : ℝ≥0∞)
Tactic: conv_rhs => rw [A, image_iUnion]
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ℕ), f '' (s ∩ u i)) : ℝ≥0∞)
have hn : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (i : ℕ) ↦ f '' (s ∩ u i))
Tactic: rw [measure_iUnion]
-- 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 : (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))
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (i : ℕ), f '' (s ∩ u i)) : ℝ≥0∞)
have h : ∀ (i : ℕ), MeasurableSet (f '' (s ∩ u i))
Tactic: rw [measure_iUnion]
-- 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 : (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
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint (fun (i : ℕ) ↦ f '' (s ∩ u i)) i j
have apply : Disjoint (s ∩ u i) (s ∩ u j)
Tactic: apply Disjoint.image _ hf inter_subset_left inter_subset_left
-- 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 : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have x : ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
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)
-- 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 : (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 : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have 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)))
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)
-- 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 : (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 : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have x₂ : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n)) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
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)
-- 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
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have 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)
Tactic: rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
-- 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
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∞)
have H : f '' s =ᶠ[ae μ] f '' t
Tactic: apply measure_congr
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
⊢ f '' s =ᶠ[ae μ] f '' t
have H : f '' t ∪ f '' (s \ t) =ᶠ[ae μ] f '' t
Tactic: rw [this, image_union]
-- 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
t : Set E
ts : t ⊆ s
ht : MeasurableSet t
t_eq_s : t =ᶠ[ae μ] s
this : s = t ∪ s \ t
⊢ f '' t ∪ f '' (s \ t) =ᶠ[ae μ] f '' t
have H : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s \ t)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)
-- 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
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)
have A : 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
-- 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
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| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have B : ∫⁻ (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
-- 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
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) in s, ENNReal.ofReal |(f' x).det| ∂μ = (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have rw : ∀ x ∈ t, HasFDerivWithinAt f (f' x) t x
Tactic: rw [A, B, lintegral_abs_det_fderiv_eq_addHaar_image _ ht _ (hf.mono ts)]
-- 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
⊢ AEMeasurable f (μ.restrict s)
have apply : ∀ (x : E) (hx : x ∈ s), ContinuousWithinAt f s x
Tactic: apply ContinuousOn.aemeasurable₀ (fun x hx ↦ ?_) 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 : NullMeasurableSet s μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f 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)
Tactic: have h'f : AEMeasurable f (μ.restrict s) := by
    apply ContinuousOn.aemeasurable₀ (fun x hx ↦ ?_) hs
    exact (hf' x hx).differentiableWithinAt.continuousWithinAt