-- 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:
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 : 0 < a
⊢ μ (f '' s) ≤ ↑m * (μ s + a)

Tactic:
obtain ⟨t, r, t_count, ts, rpos, st, μt⟩ :
  ∃ (t : Set E) (r : E → ℝ),
    t.Countable ∧
      t ⊆ s ∧
        (∀ x : E, x ∈ t → 0 < r x) ∧
          (s ⊆ ⋃ x ∈ t, closedBall x (r x)) ∧
            (∑' x : ↥t, μ (closedBall (↑x) (r ↑x))) ≤ μ s + a :=
  Besicovitch.exists_closedBall_covering_tsum_measure_le μ ha.ne' (fun _ => Ioi 0) s
    fun x _ δ δpos => ⟨δ / 2, by simp [half_pos δpos, δpos]⟩

Result:
case h.intro.intro.intro.intro.intro.intro
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 : 0 < a
t : Set E
r : E → ℝ
t_count : t.Countable
ts : t ⊆ s
rpos : ∀ x ∈ t, 0 < r x
st : s ⊆ ⋃ x ∈ t, closedBall x (r x)
μt : ∑' (x : ↑t), μ (closedBall (↑x) (r ↑x)) ≤ μ s + a
⊢ μ (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|
HC : IsCompact (⇑A '' closedBall 0 1)
⊢ Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝[>] 0) (𝓝 (μ (⇑A '' closedBall 0 1)))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

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)
⊢ Tendsto (fun ε => μ (cthickening ε (⇑A '' closedBall 0 1))) (𝓝 0) (𝓝 (μ (⇑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|
ε : ℝ
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δ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ {f x} + r • (⇑A '' closedBall 0 1 + closedBall 0 ε)
this : ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = {f x} + r • (⇑A '' closedBall 0 1 + closedBall 0 ε)
⊢ μ ({f x} + r • (⇑A '' closedBall 0 1 + closedBall 0 ε)) =
    ENNReal.ofReal (r ^ finrank ℝ E) * μ (⇑A '' closedBall 0 1 + closedBall 0 ε)

Tactic:
simp only [abs_of_nonneg r0, addHaar_smul, image_add_left, abs_pow, singleton_add,
  measure_preimage_add]

Result:
no goals

Proof state:
case h.intro.intro.intro.intro.intro.intro
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 : 0 < a
t : Set E
r : E → ℝ
t_count : t.Countable
ts : t ⊆ s
rpos : ∀ x ∈ t, 0 < r x
st : s ⊆ ⋃ x ∈ t, closedBall x (r x)
μt : ∑' (x : ↑t), μ (closedBall (↑x) (r ↑x)) ≤ μ s + a
this : Encodable ↑t
⊢ μ (f '' s) ≤ ↑m * (μ s + a)

Tactic:
calc
  μ (f '' s) ≤ μ (⋃ x : t, f '' (s ∩ closedBall x (r x))) := by
    rw [biUnion_eq_iUnion] at st
    apply measure_mono
    rw [← image_iUnion, ← inter_iUnion]
    exact image_subset _ (subset_inter (Subset.refl _) st)
  _ ≤ ∑' x : t, μ (f '' (s ∩ closedBall x (r x))) := measure_iUnion_le _
  _ ≤ ∑' x : t, m * μ (closedBall x (r x)) :=
    (ENNReal.tsum_le_tsum fun x => I x (r x) (ts x.2) (rpos x x.2).le)
  _ ≤ m * (μ s + a) := by rw [ENNReal.tsum_mul_left]; gcongr

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|
ε : ℝ
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δ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)
⊢ μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)

Tactic:
have :
  A '' closedBall 0 r + closedBall (f x) (ε * r) =
    {f x} + r • (A '' closedBall 0 1 + closedBall 0 ε) := by
  rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
    singleton_add_closedBall_zero, ← image_smul_set ℝ E E A,
    _root_.smul_closedBall _ _ zero_le_one, smul_zero, Real.norm_eq_abs, abs_of_nonneg r0,
    mul_one, mul_comm]

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|
ε : ℝ
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δ : ↑δ < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ ⇑A '' closedBall 0 r + closedBall (f x) (ε * r)
this : ⇑A '' closedBall 0 r + closedBall (f x) (ε * r) = {f x} + r • (⇑A '' closedBall 0 1 + closedBall 0 ε)
⊢ μ (f '' (s ∩ closedBall x r)) ≤ ↑m * μ (closedBall x r)