awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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‖ * ε
have norm_a : ‖a‖ ≤ ‖z‖ + ε
Tactic: have norm_a : ‖a‖ ≤ ‖z‖ + ε :=
    calc
      ‖a‖ = ‖z + (a - z)‖ := by simp only [add_sub_cancel]
      _ ≤ ‖z‖ + ‖a - z‖ := norm_add_le _ _
      _ ≤ ‖z‖ + ε := by grw [mem_closedBall_iff_norm.1 az]
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
⊢ (↑δ : ℝ) * ‖y - x‖ + ε * ‖y - x‖ = r * ((↑δ : ℝ) + ε) * ‖a‖
have simp : (↑δ : ℝ) * (r * ‖a‖) + ε * (r * ‖a‖) = r * ((↑δ : ℝ) + ε) * ‖a‖
Tactic: simp only [ya, add_sub_cancel_left, norm_smul, Real.norm_eq_abs, abs_of_nonneg rpos.le]
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
⊢ r * ((↑δ : ℝ) + ε) * ‖a‖ ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
have ha : 0 ≤ r * ((↑δ : ℝ) + ε)
Tactic: gcongr
-- 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 : E
az : a ∈ closedBall z ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
Tactic: have I : r * ‖(f' x - A) a‖ ≤ r * (δ + ε) * (‖z‖ + ε) :=
    calc
      r * ‖(f' x - A) a‖ = ‖(f' x - A) (r • a)‖ := by
        simp only [map_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg rpos.le]
      _ = ‖f y - f x - A (y - x) - (f y - f x - (f' x) (y - x))‖ := by
        simp only [ya, add_sub_cancel_left, sub_sub_sub_cancel_left, ContinuousLinearMap.coe_sub',
          Pi.sub_apply, map_smul, smul_sub]
      _ ≤ ‖f y - f x - A (y - x)‖ + ‖f y - f x - (f' x) (y - x)‖ := norm_sub_le _ _
      _ ≤ δ * ‖y - x‖ + ε * ‖y - x‖ := (add_le_add (hf _ ys _ xs) (hρ ⟨rρ hy, ys⟩))
      _ = r * (δ + ε) * ‖a‖ := by
        simp only [ya, add_sub_cancel_left, norm_smul, Real.norm_eq_abs, abs_of_nonneg rpos.le]
        ring
      _ ≤ r * (δ + ε) * (‖z‖ + ε) := by gcongr
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) =
    ‖HAdd.hAdd (α := E) (β := E) ((f' x - A : (a : E) → E) a : E) ((f' x - A : (a : E) → E) (z - a) : E)‖
have e_a : (f' x - A : (a : E) → E) z =
  HAdd.hAdd (α := E) (β := E) ((f' x - A : (a : E) → E) a : E) ((f' x - A : (a : E) → E) (z - a) : E)
Tactic: congr 1
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ (f' x - A : (a : E) → E) z =
    HAdd.hAdd (α := E) (β := E) ((f' x - A : (a : E) → E) a : E) ((f' x - A : (a : E) → E) (z - a) : E)
have e_a : HSub.hSub (α := E) (β := E) ((f' x : (a : E) → E) z : E) ((A : (a : E) → E) z : E) =
  HSub.hSub (α := E) (β := E) ((f' x : (a : E) → E) a : E) ((A : (a : E) → E) a : E) +
    (HSub.hSub (α := E) (β := E) ((f' x : (a : E) → E) z : E) ((A : (a : E) → E) z : E) -
      HSub.hSub (α := E) (β := E) ((f' x : (a : E) → E) a : E) ((A : (a : E) → E) a : E))
Tactic: simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ norm (E := E) ((f' x - A : (a : E) → E) a : E) + norm (E := E) ((f' x - A : (a : E) → E) (z - a) : E) ≤
    ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖
have h₁ : norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε)
Tactic: apply add_le_add
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
h₁ : norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ norm (E := E) ((f' x - A : (a : E) → E) a : E) + norm (E := E) ((f' x - A : (a : E) → E) (z - a) : E) ≤
    ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖
have h₂ : norm (E := E) ((f' x - A : (a : E) → E) (z - a) : E) ≤ ‖f' x - A‖ * ‖z - a‖
Tactic: apply add_le_add
-- 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 : E
az : a ∈ closedBall z ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε)
have I₁ : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * (((↑δ : ℝ) + ε) * (‖z‖ + ε))
Tactic: rw [mul_assoc] at I
Cleared hypotheses: I
-- 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 : E
az : a ∈ closedBall z ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have az₁ : ‖z - a‖ ≤ ε
Tactic: rw [mem_closedBall_iff_norm'] at az
Cleared hypotheses: az, ya, norm_a, I
-- 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 : ‖z - a‖ ≤ ε
ya : y = x + r • a
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have bc : 0 ≤ ‖f' x - A‖
Tactic: gcongr
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have x₁ : norm (E := E) ((f' x - A : (a : E) → E) z : E) =
  ‖HAdd.hAdd (α := E) (β := E) ((f' x - A : (a : E) → E) a : E) ((f' x - A : (a : E) → E) (z - a) : E)‖
Tactic: calc
    ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by
      congr 1
      simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
      abel
    _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := norm_add_le _ _
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by
      apply add_le_add
      · rw [mul_assoc] at I; exact (mul_le_mul_iff_right₀ rpos).1 I
      · apply ContinuousLinearMap.le_opNorm
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε := by
      rw [mem_closedBall_iff_norm'] at az
      gcongr
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
x₁ :
  norm (E := E) ((f' x - A : (a : E) → E) z : E) =
    ‖HAdd.hAdd (α := E) (β := E) ((f' x - A : (a : E) → E) a : E) ((f' x - A : (a : E) → E) (z - a) : E)‖
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have x₂ : norm (E := E) ((f' x - A : (a : E) → E) a : E) + norm (E := E) ((f' x - A : (a : E) → E) (z - a) : E) ≤
  ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖
Tactic: calc
    ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by
      congr 1
      simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
      abel
    _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := norm_add_le _ _
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by
      apply add_le_add
      · rw [mul_assoc] at I; exact (mul_le_mul_iff_right₀ rpos).1 I
      · apply ContinuousLinearMap.le_opNorm
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε := by
      rw [mem_closedBall_iff_norm'] at az
      gcongr
-- 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
norm_a : ‖a‖ ≤ ‖z‖ + ε
I : r * norm (E := E) ((f' x - A : (a : E) → E) a : E) ≤ r * ((↑δ : ℝ) + ε) * (‖z‖ + ε)
x₁ :
  norm (E := E) ((f' x - A : (a : E) → E) z : E) =
    ‖HAdd.hAdd (α := E) (β := E) ((f' x - A : (a : E) → E) a : E) ((f' x - A : (a : E) → E) (z - a) : E)‖
x₂ :
  norm (E := E) ((f' x - A : (a : E) → E) a : E) + norm (E := E) ((f' x - A : (a : E) → E) (z - a) : E) ≤
    ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖
⊢ norm (E := E) ((f' x - A : (a : E) → E) z : E) ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
have x₃ : ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ ≤ ((↑δ : ℝ) + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε
Tactic: calc
    ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by
      congr 1
      simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
      abel
    _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := norm_add_le _ _
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by
      apply add_le_add
      · rw [mul_assoc] at I; exact (mul_le_mul_iff_right₀ rpos).1 I
      · apply ContinuousLinearMap.le_opNorm
    _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ε := by
      rw [mem_closedBall_iff_norm'] at az
      gcongr
-- 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
hf : DifferentiableOn ℝ f s
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]