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

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
this✝ : μ (s ∩ ({x} + r • t')) ≠ 0
this : (s ∩ ({x} + r • t')).Nonempty
⊢ {x} + r • t' ⊆ {x} + r • t

Tactic:
exact add_subset_add Subset.rfl (smul_set_mono t't)

Result:
no goals

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
this : μ (s ∩ ({x} + r • t')) ≠ 0
⊢ (s ∩ ({x} + r • t)).Nonempty

Tactic:
have : (s ∩ ({x} + r • t')).Nonempty := nonempty_of_measure_ne_zero this

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
this✝ : μ (s ∩ ({x} + r • t')) ≠ 0
this : (s ∩ ({x} + r • t')).Nonempty
⊢ (s ∩ ({x} + r • t)).Nonempty

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
h' : μ (s ∩ ({x} + r • t')) = 0
⊢ False

Tactic:
simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr

Result:
no goals

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty

Tactic:
obtain ⟨t', t'_meas, t't, t'pos, t'top⟩ : ∃ t', MeasurableSet t' ∧ t' ⊆ t ∧ 0 < μ t' ∧ μ t' < ⊤ :=
  exists_subset_measure_lt_top ht h't.bot_lt

Result:
case intro.intro.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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
⊢ (s ∩ ({x} + r • t)).Nonempty

Tactic:
have : μ (s ∩ ({x} + r • t')) ≠ 0 := fun h' => by
  simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
this : μ (s ∩ ({x} + r • t')) ≠ 0
⊢ (s ∩ ({x} + r • t)).Nonempty

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
this✝ : μ (s ∩ ({x} + r • t')) ≠ 0
this : (s ∩ ({x} + r • t')).Nonempty
⊢ (s ∩ ({x} + r • t)).Nonempty

Tactic:
apply this.mono (inter_subset_inter Subset.rfl _)

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
this✝ : μ (s ∩ ({x} + r • t')) ≠ 0
this : (s ∩ ({x} + r • t')).Nonempty
⊢ {x} + r • t' ⊆ {x} + r • t

Proof state:
case intro.intro.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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, (s ∩ ({x} + r • t)).Nonempty

Tactic:
filter_upwards [(tendsto_order.1
        (tendsto_addHaar_inter_smul_one_of_density_one μ s x h t' t'_meas t'pos.ne' t'top.ne)).1
    0 zero_lt_one]

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) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
⊢ ∀ (a : ℝ), 0 < μ (s ∩ ({x} + a • t')) / μ ({x} + a • t') → (s ∩ ({x} + a • t)).Nonempty