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))
⊢ 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∞)

Tactic:
exact tendsto_measure_cthickening_of_isCompact HC

Premises used: tendsto_measure_cthickening_of_isCompact
-- 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))
⊢ 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∞)

Tactic:
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
-- 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∞)
apply :
  EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (ε : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
    fun (ε : ℝ) ↦
    (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)))
⊢ 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∞)

Tactic:
apply L0.congr' _

Premises used: Filter.Tendsto.congr'
-- 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∞)
h :
  ∀ (r : ℝ) (hr : Membership.mem (γ := Set ℝ) (Ioi 0) r),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (cthickening r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
        ℝ≥0∞)
⊢ EventuallyEq (β := ℝ≥0∞) (𝓝[>] 0)
    (fun (ε : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (cthickening ε (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))))
    fun (ε : ℝ) ↦
    (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)))

Tactic:
filter_upwards [self_mem_nhdsWithin] with r hr

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|
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∞)
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Ioi 0) r
h :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 r)) :
      ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)
h₁ h₂ :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (cthickening r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞)
        (HAdd.hAdd (α := Set E) (closedBall 0 r) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) :
      ℝ≥0∞)

Tactic:
rw [← HC.add_closedBall_zero (le_of_lt hr), add_comm]

Premises used: le_of_lt, add_comm, IsCompact.add_closedBall_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|
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∞)
⊢ 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∞)

Tactic:
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]
-- 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∞)
⊢ 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∞)

Tactic:
L1
-- 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∞)
h :
  HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    (μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))
⊢ 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∞)))

Tactic:
convert! L1
-- 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∞)
⊢ HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    (μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))

Tactic:
(addHaar_image_continuousLinearMap _ _ _).symm

Premises used: MeasureTheory.Measure.addHaar_image_continuousLinearMap, Eq.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
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∞)
⊢ HMul.hMul (β := ℝ≥0∞) d ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) =
    (μ : (a : Set E) → ℝ≥0∞) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))

Tactic:
exact (addHaar_image_continuousLinearMap _ _ _).symm

Premises used: MeasureTheory.Measure.addHaar_image_continuousLinearMap, Eq.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
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∞)
⊢ 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∞)))

Tactic:
have L2 :
      Tendsto (fun ε => μ (closedBall 0 ε + A '' closedBall 0 1)) (𝓝[>] 0)
        (𝓝 (d * μ (closedBall 0 1))) := by
      convert! L1
      exact (addHaar_image_continuousLinearMap _ _ _).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
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∞)))
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (0 : ℝ≥0∞)
hinf : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 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∞)

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|
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∞)))
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(measure_closedBall_pos μ _ zero_lt_one).ne'

Premises used: LT.lt.ne', zero_lt_one, Metric.measure_closedBall_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|
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∞)))
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_closedBall_lt_top.ne

Premises used: MeasureTheory.measure_closedBall_lt_top, LT.lt.ne
-- 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∞)))
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exacts [(measure_closedBall_pos μ _ zero_lt_one).ne', measure_closedBall_lt_top.ne]

Premises used: LT.lt.ne', zero_lt_one, Metric.measure_closedBall_pos, MeasureTheory.measure_closedBall_lt_top, LT.lt.ne
-- 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∞)))
⊢ 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∞)

Tactic:
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]
-- 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∞)
⊢ ∀ᶠ (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∞)

Tactic:
have H :
      ∀ᶠ b : ℝ in 𝓝[>] 0, μ (closedBall 0 b + A '' closedBall 0 1) < m * μ (closedBall 0 1) :=
      (tendsto_order.1 L2).2 _ I