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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ

Tactic:
convert! hf
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ

Tactic:
have hf' : ApproximatesLinearOn f (B : E →L[ℝ] E) s δ := by convert! hf
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
H :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
change :
  HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.source : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) F.target
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
change (m : ℝ≥0∞) * μ F.source ≤ μ F.target

Premises used: ENNReal.ofNNReal, PartialEquiv.target, PartialEquiv.source, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
H :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
h0 : (↑m : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞) (0 : ℝ≥0∞)
ht : (↑m : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.source : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) F.target

Tactic:
rwa [← F.symm_image_target_eq_source, mul_comm, ← ENNReal.le_div_iff_mul_le, div_eq_mul_inv,
      mul_comm, ← ENNReal.coe_inv mpos.ne']

Premises used: ENNReal.coe_inv, PartialEquiv.symm_image_target_eq_source, ENNReal.le_div_iff_mul_le, div_eq_mul_inv, LT.lt.ne', mul_comm
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
H :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
h0 : (↑m : ℝ≥0∞) ≠ 0
⊢ (↑m : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply Or.inl

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
H :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
⊢ (↑m : ℝ≥0∞) ≠ 0

Tactic:
simpa only [ENNReal.coe_eq_zero, Ne] using mpos.ne'

Premises used: Ne, ENNReal.coe_eq_zero, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
H :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
⊢ (↑m : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
h :
  (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
suffices H : μ (F.symm '' F.target) ≤ (m⁻¹ : ℝ≥0) * μ F.target by
    change (m : ℝ≥0∞) * μ F.source ≤ μ F.target
    rwa [← F.symm_image_target_eq_source, mul_comm, ← ENNReal.le_div_iff_mul_le, div_eq_mul_inv,
      mul_comm, ← ENNReal.coe_inv mpos.ne']
    · apply Or.inl
      simpa only [ENNReal.coe_eq_zero, Ne] using mpos.ne'
    · simp
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
⊢ (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)

Tactic:
hδ₀ _ _ ((hf'.to_inv h1δ).mono_num h2δ.le)

Premises used: LT.lt.le, ApproximatesLinearOn.mono_num, ApproximatesLinearOn.to_inv
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 0 < δ₀
hδ₀ :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hf' : ApproximatesLinearOn f (↑B : E →L[ℝ] E) s δ
F : PartialEquiv E E := hf'.toPartialEquiv (s := s) h1δ
⊢ (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)

Tactic:
exact hδ₀ _ _ ((hf'.to_inv h1δ).mono_num h2δ.le)

Premises used: LT.lt.le, ApproximatesLinearOn.mono_num, ApproximatesLinearOn.to_inv
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
h :
  ∀ (a : E),
    Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall a r) : ℝ≥0∞)
            ((μ : (a : Set E) → ℝ≥0∞) (closedBall a r) : ℝ≥0∞))
        (𝓝[>] 0) (𝓝 1) →
      a ∈ s → ‖f' a - A‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂μ.restrict s, ‖f' x - A‖₊ ≤ δ

Tactic:
filter_upwards [Besicovitch.ae_tendsto_measure_inter_div μ s, ae_restrict_mem hs]

Premises used: MeasureTheory.ae_restrict_mem, Besicovitch.ae_tendsto_measure_inter_div
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
apply : ∀ (z : E), norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ (↑δ : ℝ) * ‖z‖
⊢ ‖f' x - A‖₊ ≤ δ

Tactic:
apply ContinuousLinearMap.opNorm_le_bound _ δ.2 fun z => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, Subtype.property
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε

Tactic:
fun_prop
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
⊢ Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0)
    (𝓝 (((↑δ : ℝ) + 0) * (‖z‖ + 0) + ‖f' x - A‖ * 0))

Tactic:
have :
      Tendsto (fun ε : ℝ => ((δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0)
        (𝓝 ((δ + 0) * (‖z‖ + 0) + ‖f' x - A‖ * 0)) :=
      Tendsto.mono_left (Continuous.tendsto (by fun_prop) 0) nhdsWithin_le_nhds
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
this :
  Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0)
    (𝓝 (((↑δ : ℝ) + 0) * (‖z‖ + 0) + ‖f' x - A‖ * 0))
⊢ Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 ((↑δ : ℝ) * ‖z‖))

Tactic:
simp only [add_zero, mul_zero] at this

Premises used: MulZeroClass.mul_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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
this : Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 ((↑δ : ℝ) * ‖z‖))
apply :
  EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ norm (E := E) ((f' x - A : (a : E) → E) z : E)) fun (ε : ℝ) ↦
    ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ (↑δ : ℝ) * ‖z‖

Tactic:
apply le_of_tendsto_of_tendsto tendsto_const_nhds this

Premises used: tendsto_const_nhds, le_of_tendsto_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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
this : Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 ((↑δ : ℝ) * ‖z‖))
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + a) * (‖z‖ + a) + ‖f' x - A‖ * a
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ norm (E := E) ((f' x - A : (a : E) → E) z : E)) fun (ε : ℝ) ↦
    ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε

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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
this : Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 ((↑δ : ℝ) * ‖z‖))
⊢ ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + a) * (‖z‖ + a) + ‖f' x - A‖ * a

Tactic:
H

Premises used: Set.Ioi, Set.Mem, setOf
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
δ : ℝ≥0
hf : ApproximatesLinearOn f A s δ
hs : MeasurableSet s
f' : E → E →L[ℝ] E
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
x : E
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)
xs : x ∈ s
z : E
H : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
this : Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 ((↑δ : ℝ) * ‖z‖))
⊢ ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) a →
      norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + a) * (‖z‖ + a) + ‖f' x - A‖ * a

Tactic:
exact H