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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
Tactic: have K : f '' (s ∩ closedBall x r) ⊆ A '' closedBall 0 r + closedBall (f x) (ε * r) := by
      rintro y ⟨z, ⟨zs, zr⟩, rfl⟩
      rw [mem_closedBall_iff_norm] at zr
      apply Set.mem_add.2 ⟨A (z - x), _, f z - f x - A (z - x) + f x, _, _⟩
      · apply mem_image_of_mem
        simpa only [dist_eq_norm, mem_closedBall, mem_closedBall_zero_iff, sub_zero] using zr
      · rw [mem_closedBall_iff_norm, add_sub_cancel_right]
        calc
          ‖f z - f x - A (z - x)‖ ≤ δ * ‖z - x‖ := hf _ zs _ xs
          _ ≤ ε * r := by gcongr
      · simp only [map_sub]
        abel
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  {f x} +
    (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε))
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₁ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
    HSMul.hSMul (β := Set E) r (closedBall 0 ε)
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₁ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₂ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + {f x} +
    HSMul.hSMul (β := Set E) r (closedBall 0 ε)
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₁ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₂ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + {f x} +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₃ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
    ({f x} + HSMul.hSMul (β := Set E) r (closedBall 0 ε))
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₁ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₂ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + {f x} +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₃ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + HSMul.hSMul (β := Set E) r (closedBall 0 ε))
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₄ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
    ({f x} + closedBall (HSMul.hSMul (β := E) r 0) (‖r‖ * ε))
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₁ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₂ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + {f x} +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₃ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₄ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + closedBall (HSMul.hSMul (β := E) r 0) (‖r‖ * ε))
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₅ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
    HAdd.hAdd (α := Set E) {f x} (closedBall 0 (‖r‖ * ε))
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₁ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₂ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + {f x} +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₃ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₄ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + closedBall (HSMul.hSMul (β := E) r 0) (‖r‖ * ε))
rw₅ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HAdd.hAdd (α := Set E) {f x} (closedBall 0 (‖r‖ * ε))
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₆ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + closedBall (f x) (‖r‖ * ε)
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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 : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₁ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₂ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + {f x} +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₃ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₄ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + closedBall (HSMul.hSMul (β := E) r 0) (‖r‖ * ε))
rw₅ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HAdd.hAdd (α := Set E) {f x} (closedBall 0 (‖r‖ * ε))
rw₆ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + closedBall (f x) (‖r‖ * ε)
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₇ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  (⇑A : (a : E) → E) '' HSMul.hSMul (β := Set E) r (closedBall 0 1) + closedBall (f x) (‖r‖ * ε)
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have this₁ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
Tactic: have :
      A '' closedBall 0 r + closedBall (f x) (ε * r) =
        {f x} + r • (A '' closedBall 0 1 + closedBall 0 ε) := by
      rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]
-- 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
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this_1 : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
this :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
have K₁ : f '' (s ∩ closedBall x r) ⊆
  {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
Tactic: rw [this] at K
Cleared hypotheses: K, this