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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L1 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L2 :
  Tendsto
    (fun (ε : ℝ) ↦
      (μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
    (𝓝[>] 0) (𝓝 (HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))
I :
  HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
H :
  ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 b) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
⊢ ∃ (ε : ℝ),
    (μ : (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∞) ∧
      0 < ε

Tactic:
(H.and self_mem_nhdsWithin).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, 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|
HC : IsCompact (X := E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
L0 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L1 :
  Tendsto (β := ℝ≥0∞)
    (fun (ε : ℝ) ↦
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : Filter ℝ≥0∞)
L2 :
  Tendsto
    (fun (ε : ℝ) ↦
      (μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
    (𝓝[>] 0) (𝓝 (HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)))
I :
  HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
H :
  ∀ᶠ (b : ℝ) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 b) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
⊢ ∃ (ε : ℝ),
    (μ : (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∞) ∧
      0 < ε

Tactic:
exact (H.and self_mem_nhdsWithin).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, 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|
a :
  ∀ (ε : ℝ)
    (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 < ε),
    Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
      {x : ℝ≥0 |
        (fun (δ : ℝ≥0) ↦
            ∀ (s : Set E) (f : E → E),
              ApproximatesLinearOn f A s δ →
                (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
          x}
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
        x}

Tactic:
obtain ⟨ε, hε, εpos⟩ :
    ∃ ε : ℝ, μ (closedBall 0 ε + A '' closedBall 0 1) < m * μ (closedBall 0 1) ∧ 0 < ε := by
    have HC : IsCompact (A '' closedBall 0 1) :=
      (ProperSpace.isCompact_closedBall _ _).image A.continuous
    have L0 :
      Tendsto (fun ε => μ (cthickening ε (A '' closedBall 0 1))) (𝓝[>] 0)
        (𝓝 (μ (A '' closedBall 0 1))) := by
      apply Tendsto.mono_left _ nhdsWithin_le_nhds
      exact tendsto_measure_cthickening_of_isCompact HC
    have L1 :
      Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)
        (𝓝 (μ (A '' closedBall 0 1))) := by
      apply L0.congr' _
      filter_upwards [self_mem_nhdsWithin] with r hr
      rw [← HC.add_closedBall_zero (le_of_lt hr), add_comm]
    have L2 :
      Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)
        (𝓝 (d * μ (closedBall 0 1))) := by
      convert! L1
      exact (addHaar_image_continuousLinearMap _ _ _).symm
    have I : d * μ (closedBall 0 1) < m * μ (closedBall 0 1) := by
      gcongr; exacts [(measure_closedBall_pos μ _ zero_lt_one).ne', measure_closedBall_lt_top.ne]
    have H :
      ∀ᶠ b : ℝ in 𝓝[>] 0, μ (closedBall 0 b + A '' closedBall 0 1) < m * μ (closedBall 0 1) :=
      (tendsto_order.1 L2).2 _ I
    exact (H.and self_mem_nhdsWithin).exists

Premises used: Metric.closedBall, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : 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 < ε
h : 0 < NNReal.mk ε ⋯
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))

Tactic:
apply Iio_mem_nhds

Premises used: Iio_mem_nhds
-- 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 < ε
⊢ 0 < NNReal.mk ε ⋯

Tactic:
εpos
-- 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 < ε
⊢ 0 < NNReal.mk ε ⋯

Tactic:
exact εpos
-- 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 < ε
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))

Tactic:
have : Iio (.mk ε εpos.le) ∈ 𝓝 (0 : ℝ≥0) := by apply Iio_mem_nhds; exact εpos
-- 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 ε ⋯))
h :
  ∀ a ∈ Iio (NNReal.mk ε ⋯),
    ∀ (s : Set E) (f : E → E),
      ApproximatesLinearOn f A s a →
        (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Membership.mem (γ := Filter ℝ≥0) (𝓝 0)
    {x : ℝ≥0 |
      (fun (δ : ℝ≥0) ↦
          ∀ (s : Set E) (f : E → E),
            ApproximatesLinearOn f A s δ →
              (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
        x}

Tactic:
filter_upwards [this]
-- 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
hδ : δ ∈ Iio (NNReal.mk ε ⋯)
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ (↑δ : ℝ) < ε

Tactic:
simp only [mem_Iio, ← NNReal.coe_lt_coe, NNReal.coe_mk] at hδ

Premises used: Set.mem_Iio, NNReal.coe_mk, NNReal.coe_lt_coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : 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
z : E
zs : z ∈ s
zr : z ∈ closedBall x r
⊢ ‖z - x‖ ≤ r

Tactic:
rw [mem_closedBall_iff_norm] at zr

Premises used: mem_closedBall_iff_norm
-- 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
apply :
  Membership.mem (α := E) (γ := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 r))
    ((A : (a : E) → E) (z - x) : E)
apply₁ : HSub.hSub (β := E) (f z - f x) ((A : (a : E) → E) (z - x) : E) + f x ∈ closedBall (f x) (ε * r)
apply₂ :
  HAdd.hAdd (α := E) ((A : (a : E) → E) (z - x) : E)
      (HSub.hSub (β := E) (f z - f x) ((A : (a : E) → E) (z - x) : E) + f x) =
    f z
⊢ f z ∈ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)

Tactic:
apply Set.mem_add.2 ⟨A (z - x), _, f z - f x - A (z - x) + f x, _, _⟩

Premises used: Iff.mpr, HSub.hSub, HAdd.hAdd, And.intro, Exists.intro, Set.mem_add, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
h : Membership.mem (γ := Set E) (closedBall 0 r) (z - x)
⊢ Membership.mem (α := E) (γ := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 r))
    ((A : (a : E) → E) (z - x) : E)

Tactic:
apply mem_image_of_mem

Premises used: Set.mem_image_of_mem
-- 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
⊢ Membership.mem (γ := Set E) (closedBall 0 r) (z - x)

Tactic:
simpa only [dist_eq_norm, mem_closedBall, mem_closedBall_zero_iff, sub_zero] using zr

Premises used: dist_eq_norm, sub_zero, Metric.mem_closedBall, mem_closedBall_zero_iff
-- 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
rw : ‖HSub.hSub (β := E) (f z - f x) ((A : (a : E) → E) (z - x) : E)‖ ≤ ε * r
⊢ HSub.hSub (β := E) (f z - f x) ((A : (a : E) → E) (z - x) : E) + f x ∈ closedBall (f x) (ε * r)

Tactic:
rw [mem_closedBall_iff_norm, add_sub_cancel_right]

Premises used: mem_closedBall_iff_norm, add_sub_cancel_right
-- 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
⊢ ‖HSub.hSub (β := E) (f z - f x) ((A : (a : E) → E) (z - x) : E)‖ ≤ (↑δ : ℝ) * ‖z - x‖

Tactic:
hf _ zs _ xs
-- 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
c0 : 0 ≤ ‖z - x‖
b0 : 0 ≤ ε
⊢ (↑δ : ℝ) * ‖z - x‖ ≤ ε * r

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 : 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
z₁ : (↑δ : ℝ) * ‖z - x‖ ≤ ε * r
⊢ ‖HSub.hSub (β := E) (f z - f x) ((A : (a : E) → E) (z - x) : E)‖ ≤ ε * r

Tactic:
calc
          ‖f z - f x - A (z - x)‖ ≤ δ * ‖z - x‖ := hf _ zs _ xs
          _ ≤ ε * r := by gcongr

Premises used: HSub.hSub, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
simp :
  HSub.hSub (α := E) (β := E) ((A : (a : E) → E) z : E) ((A : (a : E) → E) x : E) +
      (f z - f x - HSub.hSub (α := E) (β := E) ((A : (a : E) → E) z : E) ((A : (a : E) → E) x : E) + f x) =
    f z
⊢ HAdd.hAdd (α := E) ((A : (a : E) → E) (z - x) : E)
      (HSub.hSub (β := E) (f z - f x) ((A : (a : E) → E) (z - x) : E) + f x) =
    f z

Tactic:
simp only [map_sub]

Premises used: map_sub
-- 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
z : E
zs : z ∈ s
zr : ‖z - x‖ ≤ r
⊢ HSub.hSub (α := E) (β := E) ((A : (a : E) → E) z : E) ((A : (a : E) → E) x : E) +
      (f z - f x - HSub.hSub (α := E) (β := E) ((A : (a : E) → E) z : E) ((A : (a : E) → E) x : E) + f x) =
    f z

Tactic:
abel
-- 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
⊢ 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