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
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
rw :
  ∫⁻ (x : E) in s ∩ ⋃ (i : ℕ), t i, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ
rw₁ rw₂ :
  ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ

Tactic:
rw [← inter_iUnion, inter_eq_self_of_subset_left t_cover]

Premises used: Set.inter_iUnion, Set.inter_eq_self_of_subset_left
-- 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
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
      HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [lintegral_add_right' _ aemeasurable_const, setLIntegral_const]

Premises used: MeasureTheory.lintegral_add_right', MeasureTheory.setLIntegral_const, aemeasurable_const
-- 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
apply :
  Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝 0)
    (𝓝
      (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- 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
⊢ Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝 0)
    (𝓝
      (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
tendsto_const_nhds.add ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- 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
refine :
  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∞)))
⊢ Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝 0)
    (𝓝
      (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
refine tendsto_const_nhds.add ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- 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
⊢ 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
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
⊢ 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
⊢ 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
⊢ Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
have :
    Tendsto (fun ε : ℝ≥0 => (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s) (𝓝[>] 0)
      (𝓝 ((∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 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
this :
  Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 0)
    (𝓝
      (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑0 : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))

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
this :
  Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))
apply :
  ∀ᶠ (c : ℝ≥0) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑c : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ

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

Tactic:
addHaar_image_le_lintegral_abs_det_fderiv_aux1 μ hs hf' εpos

Premises used: MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv_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
this :
  Tendsto
    (fun (ε : ℝ≥0) ↦
      ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
        HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ))
ε : ℝ≥0
εpos : 0 < ε
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
      HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact addHaar_image_le_lintegral_abs_det_fderiv_aux1 μ hs hf' εpos

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

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

Tactic:
measure_iUnion_le _

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

Tactic:
exact measure_iUnion_le _

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

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

Premises used: ENNReal.tsum_le_tsum