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δ : (↑δ : ℝ) < ε
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∞)
J :
  ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
apply :
  Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝 0)
    (𝓝 ((↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)))
⊢ Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝[>] 0)
    (𝓝 ((↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- 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∞)
J :
  ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
apply : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ≠ 0 ∨ (↑m : ℝ≥0∞) ≠ ∞
⊢ Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝 0)
    (𝓝 ((↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)))

Tactic:
apply ENNReal.Tendsto.const_mul (tendsto_const_nhds.add tendsto_id)

Premises used: Filter.tendsto_id, tendsto_const_nhds, ENNReal.Tendsto.const_mul, Filter.Tendsto.add
-- 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∞)
J :
  ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ≠ 0 ∨ (↑m : ℝ≥0∞) ≠ ∞

Tactic:
simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]

Premises used: Ne, not_false_iff, or_true, ENNReal.coe_ne_top
-- 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∞)
J :
  ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
⊢ Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝[>] 0)
    (𝓝 ((↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)))

Tactic:
have L : Tendsto (fun a => (m : ℝ≥0∞) * (μ s + a)) (𝓝[>] 0) (𝓝 (m * (μ s + 0))) := by
    apply Tendsto.mono_left _ nhdsWithin_le_nhds
    apply ENNReal.Tendsto.const_mul (tendsto_const_nhds.add tendsto_id)
    simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_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δ : (↑δ : ℝ) < ε
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∞)
J :
  ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
L :
  Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝[>] 0)
    (𝓝 ((↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)))
⊢ Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝[>] 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
rw [add_zero] at L

Premises used: add_zero
-- 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∞)
J :
  ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
L :
  Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝[>] 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
ge_of_tendsto L J

Premises used: ge_of_tendsto
-- 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∞)
J :
  ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a
L :
  Tendsto (fun (a : ℝ≥0∞) ↦ (↑m : ℝ≥0∞) * HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) a) (𝓝[>] 0)
    (𝓝 (HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤ HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact ge_of_tendsto L J

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

Tactic:
apply nhdsWithin_le_nhds

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

Tactic:
rcases eq_zero_or_pos m with (rfl | mpos)

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

Tactic:
filter_upwards
-- 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
hm : (↑0 : ℝ≥0∞) < ENNReal.ofReal |A.det|
⊢ ∀ (a : ℝ≥0) (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s a →
      HMul.hMul (β := ℝ≥0∞) (↑0 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)

Tactic:
simp only [forall_const, zero_mul, imp_true_iff, zero_le, ENNReal.coe_zero]

Premises used: zero_le, MulZeroClass.zero_mul, imp_true_iff, ENNReal.coe_zero, forall_const
-- 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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
h : A.det = 0
⊢ False

Tactic:
simp only [h, ENNReal.not_lt_zero, ENNReal.ofReal_zero, abs_zero] at hm

Premises used: ENNReal.not_lt_zero, abs_zero, ENNReal.ofReal_zero
-- 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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
⊢ A.det ≠ 0

Tactic:
have hA : A.det ≠ 0 := by
    intro h; simp only [h, ENNReal.not_lt_zero, ENNReal.ofReal_zero, abs_zero] at hm
-- 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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
simp : ∀ (hm : m < |A.det|.toNNReal), |(↑B : E →L[ℝ] E).det|.toNNReal⁻¹ < m⁻¹
⊢ ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)

Tactic:
simp only [ENNReal.ofReal, abs_inv, Real.toNNReal_inv, ContinuousLinearEquiv.det_coe_symm,
      ENNReal.coe_lt_coe] at hm ⊢

Premises used: ENNReal.ofReal, abs_inv, ENNReal.coe_lt_coe, Real.toNNReal_inv, ContinuousLinearEquiv.det_coe_symm
-- 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
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
hm : m < |A.det|.toNNReal
⊢ |(↑B : E →L[ℝ] E).det|.toNNReal⁻¹ < m⁻¹

Tactic:
NNReal.inv_lt_inv mpos.ne' hm

Premises used: LT.lt.ne', NNReal.inv_lt_inv
-- 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
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
hm : m < |A.det|.toNNReal
⊢ |(↑B : E →L[ℝ] E).det|.toNNReal⁻¹ < m⁻¹

Tactic:
exact NNReal.inv_lt_inv mpos.ne' hm

Premises used: LT.lt.ne', NNReal.inv_lt_inv
-- 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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
⊢ ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)

Tactic:
have I : ENNReal.ofReal |(B.symm : E →L[ℝ] E).det| < (m⁻¹ : ℝ≥0) := by
    simp only [ENNReal.ofReal, abs_inv, Real.toNNReal_inv, ContinuousLinearEquiv.det_coe_symm,
      ENNReal.coe_lt_coe] at hm ⊢
    exact NNReal.inv_lt_inv mpos.ne' hm
-- 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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
        (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
have :
      ∀ᶠ δ : ℝ≥0 in 𝓝[>] 0,
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t :=
      addHaar_image_le_mul_of_det_lt μ B.symm I
-- 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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
        (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
rcases :
  ∀ (δ₀ : ℝ≥0)
    (h :
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
          (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
    (h' : 0 < δ₀),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
          (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rcases (this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩

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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
        (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
δ₀ : ℝ≥0
h :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
h' : 0 < δ₀
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
          (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
⟨δ₀, h', h⟩

Premises used: And.intro, Exists.intro
-- 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 : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
mpos : 0 < m
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
this :
  ∀ᶠ (δ : ℝ≥0) in 𝓝[>] 0,
    ∀ (t : Set E) (g : E → E),
      ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
        (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
δ₀ : ℝ≥0
h :
  ∀ (t : Set E) (g : E → E),
    ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ₀ →
      (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
h' : 0 < δ₀
⊢ ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E) (g : E → E),
        ApproximatesLinearOn g (↑B.symm : E →L[ℝ] E) t δ →
          (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤ HMul.hMul (β := ℝ≥0∞) (↑m⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact ⟨δ₀, h', h⟩