-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem addHaar_image_le_mul_of_det_lt (A : E →L[ℝ] E) {m : ℝ≥0}
    (hm : ENNReal.ofReal |A.det| < m) :
    ∀ᶠ δ in 𝓝[>] (0 : ℝ≥0),
      ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ m * μ s

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0, μ (f '' s) ≤ ↑m * (μ s + a)

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)
a : ℝ≥0∞
ha : a ∈ Ioi 0
⊢ μ (f '' s) ≤ ↑m * (μ s + a)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε : μ (closedBall 0 ε + ⇑A '' closedBall 0 1) < ↑m * μ (closedBall 0 1)
εpos : 0 < ε
this : Iio ⟨ε, ⋯⟩ ∈ 𝓝 0
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : ↑δ < ε
I : ∀ (x : E) (r : ℝ), x ∈ s → 0 ≤ r → μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)
J : ∀ᶠ (a : ℝ≥0∞) in 𝓝[>] 0, μ (f '' s) ≤ ↑m * (μ s + a)
⊢ μ s + 0 ≠ 0 ∨ ↑m ≠ ⊤

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

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε => μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ Tendsto (fun ε => μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (d * μ (closedBall 0 1)))

Tactic:
convert L1

Result:
case h.e'_5.h.e'_3
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
L1 : Tendsto (fun ε => μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ d * μ (closedBall 0 1) = μ (⇑A '' closedBall 0 1)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) =ᶠ[𝓝[>] 0] fun ε => μ (closedBall 0 ε + ⇑A '' closedBall 0 1)

Tactic:
filter_upwards [self_mem_nhdsWithin] with r hr

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
r : ℝ
hr : r ∈ Ioi 0
⊢ μ (cthickening r (⇑A '' closedBall 0 1)) = μ (closedBall 0 r + ⇑A '' closedBall 0 1)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ Tendsto (fun ε => μ (closedBall 0 ε + ⇑A '' closedBall 0 1)) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))

Tactic:
apply L0.congr' _

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < ↑m
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
HC : IsCompact (⇑A '' closedBall 0 1)
L0 : Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))
⊢ (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) =ᶠ[𝓝[>] 0] fun ε => μ (closedBall 0 ε + ⇑A '' closedBall 0 1)