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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ Tendsto (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
ENNReal.Tendsto.mul_const ?_ (Or.inr h's)

Premises used: ENNReal.Tendsto.mul_const, Or.inr
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
refine : Tendsto (fun (ε : ℝ≥0) ↦ 2 * (↑ε : ℝ≥0∞)) (𝓝 0) (𝓝 (2 * (↑0 : ℝ≥0∞)))
⊢ Tendsto (fun (ε : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)) (𝓝 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
refine ENNReal.Tendsto.mul_const ?_ (Or.inr h's)

Premises used: ENNReal.Tendsto.mul_const, Or.inr
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ Tendsto (fun (ε : ℝ≥0) ↦ 2 * (↑ε : ℝ≥0∞)) (𝓝 0) (𝓝 (2 * (↑0 : ℝ≥0∞)))

Tactic:
ENNReal.Tendsto.const_mul (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr ENNReal.coe_ne_top)

Premises used: Iff.mpr, Filter.tendsto_id, ENNReal.Tendsto.const_mul, ENNReal.tendsto_coe, Or.inr, ENNReal.coe_ne_top
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ Tendsto (fun (ε : ℝ≥0) ↦ 2 * (↑ε : ℝ≥0∞)) (𝓝 0) (𝓝 (2 * (↑0 : ℝ≥0∞)))

Tactic:
exact ENNReal.Tendsto.const_mul (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr ENNReal.coe_ne_top)

Premises used: Iff.mpr, Filter.tendsto_id, ENNReal.Tendsto.const_mul, ENNReal.tendsto_coe, Or.inr, ENNReal.coe_ne_top
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
⊢ Tendsto
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0)
    (𝓝
      (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))))

Tactic:
have :
    Tendsto (fun ε : ℝ≥0 => μ (f '' s) + 2 * ε * μ s) (𝓝[>] 0)
      (𝓝 (μ (f '' s) + 2 * (0 : ℝ≥0) * μ s)) := by
    apply Tendsto.mono_left _ nhdsWithin_le_nhds
    refine tendsto_const_nhds.add ?_
    refine ENNReal.Tendsto.mul_const ?_ (Or.inr h's)
    exact ENNReal.Tendsto.const_mul (ENNReal.tendsto_coe.2 tendsto_id) (Or.inr ENNReal.coe_ne_top)
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this :
  Tendsto
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0)
    (𝓝
      (HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (f '' s)) : Filter ℝ≥0∞)

Tactic:
simp only [add_zero, zero_mul, mul_zero, ENNReal.coe_zero] at this

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, ENNReal.coe_zero, add_zero
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (f '' s)) : Filter ℝ≥0∞)
apply :
  ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0,
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑c : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
apply ge_of_tendsto this

Premises used: ge_of_tendsto
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (f '' s)) : Filter ℝ≥0∞)
h :
  ∀ (a : ℝ≥0),
    Membership.mem (γ := Set ℝ≥0) (Ioi 0) a →
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
        HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
          (HMul.hMul (β := ℝ≥0∞) (2 * (↑a : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0,
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑c : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))

Tactic:
filter_upwards [self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (f '' s)) : Filter ℝ≥0∞)
ε : ℝ≥0
εpos : Membership.mem (γ := Set ℝ≥0) (Ioi 0) ε
⊢ 0 < ε

Tactic:
rw [mem_Ioi] at εpos

Premises used: Set.mem_Ioi
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (f '' s)) : Filter ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))

Tactic:
lintegral_abs_det_fderiv_le_addHaar_image_aux1 μ hs hf' hf εpos

Premises used: MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1
-- 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
h's : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ≥0) ↦
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (f '' s)) : Filter ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))

Tactic:
exact lintegral_abs_det_fderiv_le_addHaar_image_aux1 μ hs hf' hf εpos

Premises used: MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1
-- 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
n : ℕ
apply : ∀ (i : ℕ), MeasurableSet (spanningSets μ i)
⊢ MeasurableSet (u n)

Tactic:
apply MeasurableSet.disjointed fun i => ?_

Premises used: MeasurableSet.disjointed
-- 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
n i : ℕ
⊢ MeasurableSet (spanningSets μ i)

Tactic:
measurableSet_spanningSets μ i

Premises used: MeasureTheory.measurableSet_spanningSets
-- 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
n i : ℕ
⊢ MeasurableSet (spanningSets μ i)

Tactic:
exact measurableSet_spanningSets μ i

Premises used: MeasureTheory.measurableSet_spanningSets
-- 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
⊢ ∀ (n : ℕ), MeasurableSet (u n)

Tactic:
have u_meas : ∀ n, MeasurableSet (u n) := by
    intro n
    apply MeasurableSet.disjointed fun i => ?_
    exact measurableSet_spanningSets μ i
-- 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)
rw : s = s ∩ ⋃ (i : ℕ), u i
rw₁ : s = s ∩ ⋃ (i : ℕ), spanningSets μ i
rw₂ : s = s ∩ univ
rw₃ rw₄ : s = s
⊢ s = ⋃ (n : ℕ), s ∩ u n

Tactic:
rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]

Premises used: Set.inter_univ, iUnion_disjointed, MeasureTheory.iUnion_spanningSets, Set.inter_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)
⊢ s = ⋃ (n : ℕ), s ∩ u n

Tactic:
have A : s = ⋃ n, s ∩ u n := by
    rw [← inter_iUnion, iUnion_disjointed, iUnion_spanningSets, inter_univ]
-- 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 : ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ
| ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
rw [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
u : (n : ℕ) → Set E := fun (n : ℕ) ↦ disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ (n : ℕ), s ∩ u n
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| ∂μ
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ

Tactic:
conv_lhs => rw [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
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)
hd : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (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| ∂μ

Tactic:
rw [lintegral_iUnion]

Premises used: MeasureTheory.lintegral_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
n : ℕ
⊢ MeasurableSet (s ∩ u n)

Tactic:
hs.inter (u_meas n)

Premises used: 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
n : ℕ
⊢ MeasurableSet (s ∩ u n)

Tactic:
exact hs.inter (u_meas n)

Premises used: 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
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ u n)

Tactic:
pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right

Premises used: pairwise_disjoint_mono, disjoint_disjointed, 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
⊢ Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ u n)

Tactic:
exact pairwise_disjoint_mono (disjoint_disjointed _) fun n => inter_subset_right

Premises used: pairwise_disjoint_mono, disjoint_disjointed, 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
apply : ∀ (n : ℕ), ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' (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)))

Tactic:
apply ENNReal.tsum_le_tsum fun n => ?_

Premises used: ENNReal.tsum_le_tsum
-- 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
n : ℕ
lintegral_abs_det_fderiv_le_addHaar_image_aux2 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : E) in s ∩ u n, ENNReal.ofReal |(f' x).det| ∂μ ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ u n))

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)

Premises used: Set.inter_subset_left, And.left, Set.InjOn.mono, HasFDerivWithinAt.mono, MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux2, 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
n : ℕ
⊢ 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)
-- 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
n : ℕ
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, ne_of_lt, 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
n : ℕ
this : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (u n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ u n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_of_lt (lt_of_le_of_lt (measure_mono inter_subset_right) this)

Premises used: lt_of_le_of_lt, MeasureTheory.measure_mono, ne_of_lt, Set.inter_subset_right