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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩

Premises used: half_pos, lt_min, And.intro, Exists.intro, Min.min
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
refine_1 : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(min δ δ'') : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
refine_2 :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g A t (min δ δ'') →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
        HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)
apply : dist B A < δ'
⊢ dist B.det A.det ≤ (↑ε : ℝ)

Tactic:
apply (hδ' B _).le

Premises used: LT.lt.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
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)
rw : ‖B - A‖ < δ'
⊢ dist B A < δ'

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)
⊢ ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)

Tactic:
hB
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)
⊢ (↑(min δ δ'') : ℝ) ≤ (↑δ'' : ℝ)

Tactic:
simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]

Premises used: le_refl, min_le_iff, NNReal.coe_min, or_true
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)
⊢ (↑δ'' : ℝ) < δ'

Tactic:
half_lt_self δ'pos

Premises used: half_lt_self, NNReal.toReal
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
B : E →L[ℝ] E
hB : ‖B - A‖ ≤ (↑(min δ δ'') : ℝ)
δ₁ : (↑(min δ δ'') : ℝ) ≤ (↑δ'' : ℝ)
⊢ ‖B - A‖ < δ'

Tactic:
calc
        ‖B - A‖ ≤ (min δ δ'' : ℝ≥0) := hB
        _ ≤ δ'' := by simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]
        _ < δ' := half_lt_self δ'pos

Premises used: half_lt_self, Min.min
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
⊢ (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
h t g (htg.mono_num (min_le_left _ _))

Premises used: ENNReal.ofNNReal, WithTop.map₂, WithTop.some, min_le_left, ApproximatesLinearOn.mono_num, Option.map₂
-- 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
m : ℝ≥0 := |A.det|.toNNReal + ε
I : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
δpos : 0 < δ
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
⊢ (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact h t g (htg.mono_num (min_le_left _ _))

Premises used: min_le_left, ApproximatesLinearOn.mono_num
-- 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),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
                HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
have :
    ∀ A : E →L[ℝ] E,
      ∃ δ : ℝ≥0,
        0 < δ ∧
          (∀ B : E →L[ℝ] E, ‖B - A‖ ≤ δ → |B.det - A.det| ≤ ε) ∧
            ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ →
              μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ε) * μ t := by
    intro A
    let m : ℝ≥0 := Real.toNNReal |A.det| + ε
    have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, ENNReal.coe_lt_coe]
    rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, δpos⟩
    obtain ⟨δ', δ'pos, hδ'⟩ : ∃ (δ' : ℝ), 0 < δ' ∧ ∀ B, dist B A < δ' → dist B.det A.det < ↑ε := by
      refine continuousAt_iff.1 ?_ ε εpos
      exact ContinuousLinearMap.continuous_det.continuousAt
    let δ'' : ℝ≥0 := ⟨δ' / 2, (half_pos δ'pos).le⟩
    refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩
    · intro B hB
      rw [← Real.dist_eq]
      apply (hδ' B _).le
      rw [dist_eq_norm]
      calc
        ‖B - A‖ ≤ (min δ δ'' : ℝ≥0) := hB
        _ ≤ δ'' := by simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]
        _ < δ' := half_lt_self δ'pos
    · intro t g htg
      exact h t g (htg.mono_num (min_le_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 < ε
this :
  ∀ (A : E →L[ℝ] E),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
                HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
choose :
  ∀ (δ : (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∞)),
    (μ : (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∞)
⊢ (μ : (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:
choose δ hδ using this
-- 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),
    Pairwise (Disjoint on t) ∧
      (∀ (n : ℕ), MeasurableSet (t n)) ∧
        s ⊆ ⋃ (n : ℕ), t n ∧
          (∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧ (s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y)

Tactic:
exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'

Premises used: exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, LT.lt.ne', And.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∞)
obtain :
  ∀ (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))),
    (μ : (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∞)
⊢ (μ : (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:
obtain ⟨t, A, t_disj, t_meas, t_cover, ht, -⟩ :
    ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
      Pairwise (Disjoint on t) ∧
        (∀ n : ℕ, MeasurableSet (t n)) ∧
          (s ⊆ ⋃ n : ℕ, t n) ∧
            (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))) ∧
              (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
    exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'

Premises used: exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, LT.lt.ne', And.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))
h : f '' s ⊆ ⋃ (n : ℕ), f '' (s ∩ t n)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)

Tactic:
apply measure_mono

Premises used: MeasureTheory.measure_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 : 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))
h : f '' s ⊆ f '' (s ∩ ⋃ (i : ℕ), t i)
⊢ f '' s ⊆ ⋃ (n : ℕ), f '' (s ∩ t n)

Tactic:
rw [← image_iUnion, ← inter_iUnion]

Premises used: Set.image_iUnion, 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
ε : ℝ≥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))
⊢ f '' s ⊆ f '' (s ∩ ⋃ (i : ℕ), t i)

Tactic:
Set.image_mono (subset_inter Subset.rfl t_cover)

Premises used: Set.image_mono, Set.Subset.rfl, Set.subset_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
ε : ℝ≥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))
⊢ f '' s ⊆ f '' (s ∩ ⋃ (i : ℕ), t i)

Tactic:
exact Set.image_mono (subset_inter Subset.rfl t_cover)

Premises used: Set.image_mono, Set.Subset.rfl, Set.subset_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
ε : ℝ≥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))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le