awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
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∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.source : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) F.target
have ht : (↑m : ℝ≥0∞) ≠ ∞ ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞) (∞ : ℝ≥0∞)
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']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
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 ∨ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞) (0 : ℝ≥0∞)
have h0 : (↑m : ℝ≥0∞) ≠ 0
Tactic: apply Or.inl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
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δ
⊢ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
have h : (μ : (a : Set E) → ℝ≥0∞) ((↑F.symm : E → E) '' F.target) ≤
  HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) F.target : ℝ≥0∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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) ∂μ.restrict s, ‖f' x - A‖₊ ≤ δ
have 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‖₊ ≤ δ
Tactic: filter_upwards [Besicovitch.ae_tendsto_measure_inter_div μ s, ae_restrict_mem hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
⊢ ‖f' x - A‖₊ ≤ δ
have apply : ∀ (z : E), norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ (↑δ : ℝ) * ‖z‖
Tactic: apply ContinuousLinearMap.opNorm_le_bound _ δ.2 fun z => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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‖ * ε
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ (↑δ : ℝ) * ‖z‖
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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))
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ (↑δ : ℝ) * ‖z‖
have this₁ : Tendsto (fun (ε : ℝ) ↦ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε) (𝓝[>] 0) (𝓝 ((↑δ : ℝ) * ‖z‖))
Tactic: simp only [add_zero, mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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‖))
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ (↑δ : ℝ) * ‖z‖
have apply : EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ norm (E := E) ((f' x - A : (a : E) → E) z : E)) fun (ε : ℝ) ↦
  ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Tactic: apply le_of_tendsto_of_tendsto tendsto_const_nhds this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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‖))
⊢ EventuallyLE (β := ℝ) (𝓝[>] 0) (fun (x_1 : ℝ) ↦ norm (E := E) ((f' x - A : (a : E) → E) z : E)) fun (ε : ℝ) ↦
    ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have 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
Tactic: filter_upwards [self_mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ (↑δ : ℝ) * ‖z‖
have suffices : ∀ (ε : ℝ), 0 < ε → norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Tactic: suffices H : ∀ ε, 0 < ε → ‖(f' x - A) z‖ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε by
    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
    simp only [add_zero, mul_zero] at this
    apply le_of_tendsto_of_tendsto tendsto_const_nhds this
    filter_upwards [self_mem_nhdsWithin]
    exact H
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
Tactic: have B₁ : ∀ᶠ r in 𝓝[>] (0 : ℝ), (s ∩ ({x} + r • closedBall z ε)).Nonempty :=
    eventually_nonempty_inter_smul_of_density_one μ s x hx _ measurableSet_closedBall
      (measure_closedBall_pos μ z εpos).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have obtain : ∀ (ρ : ℝ) (ρpos : ρ > 0)
  (hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}),
  norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Tactic: obtain ⟨ρ, ρpos, hρ⟩ :
    ∃ ρ > 0, ball x ρ ∩ s ⊆ {y : E | ‖f y - f x - (f' x) (y - x)‖ ≤ ε * ‖y - x‖} :=
    mem_nhdsWithin_iff.1 ((hf' x xs).isLittleO.def εpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
have a : Membership.mem (γ := Filter ℝ) (𝓝 0) {x_1 : ℝ | (fun (r : ℝ) ↦ {x} + r • closedBall z ε ⊆ ball x ρ) x_1}
Tactic: apply nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
Tactic: have B₂ : ∀ᶠ r in 𝓝[>] (0 : ℝ), {x} + r • closedBall z ε ⊆ ball x ρ := by
    apply nhdsWithin_le_nhds
    exact eventually_singleton_add_smul_subset isBounded_closedBall (ball_mem_nhds x ρpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have obtain : ∀ (r : ℝ) (y : E) (ys : y ∈ s) (hy : y ∈ {x} + r • closedBall z ε) (rρ : {x} + r • closedBall z ε ⊆ ball x ρ)
  (rpos : 0 < r), norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Tactic: obtain ⟨r, ⟨y, ⟨ys, hy⟩⟩, rρ, rpos⟩ :
    ∃ r : ℝ,
      (s ∩ ({x} + r • closedBall z ε)).Nonempty ∧ {x} + r • closedBall z ε ⊆ ball x ρ ∧ 0 < r :=
    (B₁.and (B₂.and self_mem_nhdsWithin)).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
⊢ ∃ a ∈ closedBall z ε, y = x + r • a
have hy₁ : ∃ y_1 ∈ closedBall z ε, r • y_1 = -x + y
Tactic: simp only [mem_smul_set, image_add_left, mem_preimage, singleton_add] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
hy : ∃ y_1 ∈ closedBall z ε, r • y_1 = -x + y
⊢ ∃ a ∈ closedBall z ε, y = x + r • a
have rcases : ∀ (a : E) (az : a ∈ closedBall z ε) (ha : r • a = -x + y), ∃ a ∈ closedBall z ε, y = x + r • a
Tactic: rcases hy with ⟨a, az, ha⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have obtain : ∀ (a : E) (az : a ∈ closedBall z ε) (ya : y = x + r • a),
  norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Tactic: obtain ⟨a, az, ya⟩ : ∃ a, a ∈ closedBall z ε ∧ y = x + r • a := by
    simp only [mem_smul_set, image_add_left, mem_preimage, singleton_add] at hy
    rcases hy with ⟨a, az, ha⟩
    exact ⟨a, az, by simp only [ha, add_neg_cancel_left]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
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
ε : ℝ
εpos : 0 < ε
B₁ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • closedBall z ε)).Nonempty
ρ : ℝ
ρpos : ρ > 0
hρ : ball x ρ ∩ s ⊆ {y : E | ‖HSub.hSub (β := E) (f y - f x) ((f' x : (a : E) → E) (y - x) : E)‖ ≤ ε * ‖y - x‖}
B₂ : ∀ᶠ (r : ℝ) in 𝓝[>] 0, {x} + r • closedBall z ε ⊆ ball x ρ
r : ℝ
y : E
ys : y ∈ s
hy : y ∈ {x} + r • closedBall z ε
rρ : {x} + r • closedBall z ε ⊆ ball x ρ
rpos : 0 < r
a : E
az : a ∈ closedBall z ε
ya : y = x + r • a
⊢ ‖z‖ + ‖a - z‖ ≤ ‖z‖ + ε
have grw : ‖z‖ + ε ≤ ‖z‖ + ε
Tactic: grw [mem_closedBall_iff_norm.1 az]