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 : (↑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∞)
a :
  ∀ (δ₀ : ℝ≥0) (δ₀pos : 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∞)),
    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:
obtain ⟨δ₀, δ₀pos, hδ₀⟩ :
    ∃ δ : ℝ≥0,
      0 < δ ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g (B.symm : E →L[ℝ] E) t δ → μ (g '' t) ≤ ↑m⁻¹ * μ t := by
    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
    rcases (this.and self_mem_nhdsWithin).exists with ⟨δ₀, h, h'⟩
    exact ⟨δ₀, h', h⟩
-- 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
δ₀pos : 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∞)
pos : ∀ (h : Subsingleton E), ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
neg : ∀ (h : ¬Subsingleton E), ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹

Tactic:
by_cases h : Subsingleton E

Premises used: Subsingleton
-- 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
δ₀pos : 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 : Subsingleton E
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹

Tactic:
simp only [h, true_or, eventually_const]

Premises used: true_or, Filter.eventually_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
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 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 : ¬Subsingleton E
neg : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹

Tactic:
simp only [h, false_or]

Premises used: false_or
-- 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
δ₀pos : 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 : ¬Subsingleton E
neg : 0 < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹

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 : (↑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
δ₀pos : 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 : ¬Subsingleton E
⊢ 0 < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹

Tactic:
simpa only [h, false_or, inv_pos] using B.subsingleton_or_nnnorm_symm_pos

Premises used: inv_pos, false_or, ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_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 : (↑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
δ₀pos : 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∞)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹

Tactic:
have L1 : ∀ᶠ δ in 𝓝 (0 : ℝ≥0), Subsingleton E ∨ δ < ‖(B.symm : E →L[ℝ] E)‖₊⁻¹ := by
    by_cases h : Subsingleton E
    · simp only [h, true_or, eventually_const]
    simp only [h, false_or]
    apply Iio_mem_nhds
    simpa only [h, false_or, inv_pos] using B.subsingleton_or_nnnorm_symm_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 : (↑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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
inl :
  ∀ (H : ‖(↑B.symm : E →L[ℝ] E)‖₊ = 0),
    Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
      (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
inr :
  ∀ (H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0),
    Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
      (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))

Tactic:
rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)

Premises used: ContinuousLinearEquiv.symm, NNNorm.nnnorm, eq_or_ne, OfNat.ofNat, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ = 0
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))

Tactic:
simpa only [H, zero_mul] using tendsto_const_nhds

Premises used: tendsto_const_nhds, MulZeroClass.zero_mul
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))

Tactic:
Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0
inr : Tendsto (fun (δ : ℝ≥0) ↦ (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹) (𝓝 0) (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹)
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))

Tactic:
refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0
⊢ Tendsto (fun (δ : ℝ≥0) ↦ (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹) (𝓝 0) (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹)

Tactic:
(Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.inv₀, Filter.Tendsto.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 : (↑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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0
inr : ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0 ≠ 0
⊢ Tendsto (fun (δ : ℝ≥0) ↦ (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹) (𝓝 0) (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹)

Tactic:
refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.inv₀, Filter.Tendsto.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 : (↑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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
H : ‖(↑B.symm : E →L[ℝ] E)‖₊ ≠ 0
⊢ ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0 ≠ 0

Tactic:
simpa only [tsub_zero, inv_eq_zero, Ne] using H

Premises used: inv_eq_zero, Ne, tsub_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
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))

Tactic:
have :
      Tendsto (fun δ => ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
        (𝓝 (‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0)) := by
      rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
      · simpa only [H, zero_mul] using tendsto_const_nhds
      refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id
      refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_
      simpa only [tsub_zero, inv_eq_zero, Ne] using H
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
this :
  Tendsto (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
    (𝓝 (‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0))
⊢ Tendsto (β := ℝ≥0) (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0) (𝓝 0)

Tactic:
simp only [mul_zero] at this

Premises used: MulZeroClass.mul_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
hA : A.det ≠ 0
B : E ≃L[ℝ] E := A.toContinuousLinearEquivOfDetNeZero hA
I : ENNReal.ofReal |(↑B.symm : E →L[ℝ] E).det| < (↑m⁻¹ : ℝ≥0∞)
δ₀ : ℝ≥0
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
this :
  Tendsto (β := ℝ≥0) (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀

Tactic:
(tendsto_order.1 this).2 δ₀ δ₀pos

Premises used: tendsto_order, And.right, Iff.mp
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
this :
  Tendsto (β := ℝ≥0) (fun (δ : ℝ≥0) ↦ ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀

Tactic:
exact (tendsto_order.1 this).2 δ₀ δ₀pos

Premises used: tendsto_order, And.right, Iff.mp
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
⊢ ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀

Tactic:
have L2 :
    ∀ᶠ δ in 𝓝 (0 : ℝ≥0), ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀ := by
    have :
      Tendsto (fun δ => ‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ) (𝓝 0)
        (𝓝 (‖(B.symm : E →L[ℝ] E)‖₊ * (‖(B.symm : E →L[ℝ] E)‖₊⁻¹ - 0)⁻¹ * 0)) := by
      rcases eq_or_ne ‖(B.symm : E →L[ℝ] E)‖₊ 0 with (H | H)
      · simpa only [H, zero_mul] using tendsto_const_nhds
      refine Tendsto.mul (tendsto_const_nhds.mul ?_) tendsto_id
      refine (Tendsto.sub tendsto_const_nhds tendsto_id).inv₀ ?_
      simpa only [tsub_zero, inv_eq_zero, Ne] using H
    simp only [mul_zero] at this
    exact (tendsto_order.1 this).2 δ₀ δ₀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 : (↑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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
h :
  ∀ (a : ℝ≥0),
    Subsingleton E ∨ a < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ →
      ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - a)⁻¹ * a < δ₀ →
        ∀ (s : Set E) (f : E → E),
          ApproximatesLinearOn f A s a →
            HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥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∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s))
        x}

Tactic:
filter_upwards [L1, L2]
-- 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
δ₀pos : 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∞)
L1 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
L2 : ∀ᶠ (δ : ℝ≥0) in 𝓝 0, ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
δ : ℝ≥0
h1δ : Subsingleton E ∨ δ < ‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹
h2δ : ‖(↑B.symm : E →L[ℝ] E)‖₊ * (‖(↑B.symm : E →L[ℝ] E)‖₊⁻¹ - δ)⁻¹ * δ < δ₀
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
⊢ ApproximatesLinearOn f A s δ

Tactic:
hf