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 : 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 ε)

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]
-- 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 : 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 ε)
⊢ 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
-- 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 : 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 ε)
K₁ :
  f '' (s ∩ closedBall x r) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (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 ε)

Tactic:
rw [this] at K
-- 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 : 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) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
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 ε)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        ({f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
      ℝ≥0∞)

Tactic:
measure_mono K

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
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) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
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 x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞)

Tactic:
simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
          measure_preimage_add]

Premises used: Set.image_add_left, Set.singleton_add, abs_of_nonneg, MeasureTheory.measure_preimage_add, abs_pow, MeasureTheory.Measure.addHaar_smul
-- 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 : 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) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
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 ε)
rw :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞) ≤
    ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞) ≤
    ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)

Tactic:
rw [add_comm]

Premises used: add_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 : 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) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
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 ε)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞) ≤
    ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)

Tactic:
gcongr
-- 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 : 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) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
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 ε)
simp :
  ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    (↑m : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
⊢ ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
simp only [addHaar_closedBall' μ _ r0]

Premises used: MeasureTheory.Measure.addHaar_closedBall'
-- 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 : 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) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
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 ε)
⊢ ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    (↑m : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E)) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)

Tactic:
ring
-- 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 : 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) ⊆
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
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 x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞)
μ₂ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank ℝ E))
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)) :
        ℝ≥0∞) ≤
    ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
μ₃ :
  ENNReal.ofReal (r ^ finrank ℝ E) *
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
calc
      μ (f '' (s ∩ closedBall x r)) ≤ μ ({f x} + r • (A '' closedBall 0 1 + closedBall 0 ε)) :=
        measure_mono K
      _ = ENNReal.ofReal (r ^ finrank ℝ E) * μ (A '' closedBall 0 1 + closedBall 0 ε) := by
        simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
          measure_preimage_add]
      _ ≤ ENNReal.ofReal (r ^ finrank ℝ E) * (m * μ (closedBall 0 1)) := by
        rw [add_comm]; gcongr
      _ = m * μ (closedBall x r) := by simp only [addHaar_closedBall' μ _ r0]; ring

Premises used: Real, ENNReal.ofNNReal, HMul.hMul, ENNReal.ofReal, Inter.inter, HPow.hPow, HAdd.hAdd, MeasureTheory.measure_mono, Set.image, HSMul.hSMul, Metric.closedBall, Singleton.singleton, OfNat.ofNat, DFunLike.coe, Module.finrank
-- 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 : 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 : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)

Tactic:
have I : ∀ x r, x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ m * μ (closedBall x r) := by
    intro x r xs r0
    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
    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]
    rw [this] at K
    calc
      μ (f '' (s ∩ closedBall x r)) ≤ μ ({f x} + r • (A '' closedBall 0 1 + closedBall 0 ε)) :=
        measure_mono K
      _ = ENNReal.ofReal (r ^ finrank ℝ E) * μ (A '' closedBall 0 1 + closedBall 0 ε) := by
        simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
          measure_preimage_add]
      _ ≤ ENNReal.ofReal (r ^ finrank ℝ E) * (m * μ (closedBall 0 1)) := by
        rw [add_comm]; gcongr
      _ = m * μ (closedBall x r) := by simp only [addHaar_closedBall' μ _ r0]; ring
-- 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 : 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δ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
h :
  ∀ (a : ℝ≥0∞) (ha : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) a),
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

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
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δ : (↑δ : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
a : ℝ≥0∞
ha : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) a
⊢ 0 < a

Tactic:
rw [mem_Ioi] at ha

Premises used: Set.mem_Ioi
-- 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 : 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 ε ⋯))
δ_1 : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ_1
hδ : (↑δ_1 : ℝ) < ε
I :
  ∀ (x : E) (r : ℝ),
    x ∈ s →
      0 ≤ r →
        (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ closedBall x r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
a : ℝ≥0∞
ha : 0 < a
x : E
h : x ∈ s
δ : ℝ
δpos : δ > 0
⊢ δ / 2 ∈ (fun (x : E) ↦ (Ioi 0 : Set ℝ)) x ∩ Ioo 0 δ

Tactic:
simp [half_pos δpos, δpos]

Premises used: half_pos