-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem tendsto_addHaar_inter_smul_zero_of_density_zero (s : Set E) (x : E)
    (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)) (t : Set E)
    (ht : MeasurableSet t) (h''t : μ t ≠ ∞) :
    Tendsto (fun r : ℝ => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)

Proof state:
case inl.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
⊢ μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) < ε

Tactic:
suffices H : μ (s ∩ ({x} + r • t)) = 0 by
  rw [H]; simpa only [ENNReal.zero_div] using εpos

Result:
case inl.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
⊢ μ (s ∩ ({x} + r • t)) = 0

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r => μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
⊢ μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) < ε

Tactic:
have I :
  μ (s ∩ ({x} + r • t)) ≤
    μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ ({x} + r • (t \ closedBall 0 n)) :=
  calc
    μ (s ∩ ({x} + r • t)) =
        μ (s ∩ ({x} + r • (t ∩ closedBall 0 n)) ∪ s ∩ ({x} + r • (t \ closedBall 0 n))) := by
      rw [← inter_union_distrib_left, ← add_union, ← smul_set_union, inter_union_diff]
    _ ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ (s ∩ ({x} + r • (t \ closedBall 0 n))) :=
      measure_union_le _ _
    _ ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 n))) + μ ({x} + r • (t \ closedBall 0 n)) := by
      gcongr; apply inter_subset_right

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r => μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ (s ∩ ({x} + r • t)) / μ ({x} + r • t) < ε

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
⊢ Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)

Tactic:
refine tendsto_order.2 ⟨fun a' ha' => (ENNReal.not_lt_zero ha').elim, fun ε (εpos : 0 < ε) => ?_⟩

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t = 0
r : ℝ
⊢ μ (s ∩ ({x} + r • t)) ≤ 0

Tactic:
calc
  μ (s ∩ ({x} + r • t)) ≤ μ ({x} + r • t) := measure_mono inter_subset_right
  _ = 0 := by
    simp only [h't, addHaar_smul, image_add_left, measure_preimage_add, singleton_add,
      mul_zero]

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε

Tactic:
obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ μ (t \ closedBall 0 n) < ε / 2 * μ t := by
  have A :
    Tendsto (fun n : ℕ => μ (t \ closedBall 0 n)) atTop
      (𝓝 (μ (⋂ n : ℕ, t \ closedBall 0 n))) := by
    have N : ∃ n : ℕ, μ (t \ closedBall 0 n) ≠ ∞ :=
      ⟨0, ((measure_mono diff_subset).trans_lt h''t.lt_top).ne⟩
    refine tendsto_measure_iInter_atTop
      (fun n ↦ (ht.diff measurableSet_closedBall).nullMeasurableSet) (fun m n hmn ↦ ?_) N
    exact diff_subset_diff Subset.rfl (closedBall_subset_closedBall (Nat.cast_le.2 hmn))
  have : ⋂ n : ℕ, t \ closedBall 0 n = ∅ := by
    simp_rw [diff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
      iUnion_closedBall_nat, compl_univ, inter_empty]
  simp only [this, measure_empty] at A
  have I : 0 < ε / 2 * μ t := ENNReal.mul_pos (ENNReal.half_pos εpos.ne').ne' h't
  exact (Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists

Result:
case inr.intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ⊤
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] 0, μ (s ∩ ({x} + b • t)) / μ ({x} + b • t) < ε