case refine'_1
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x

case refine'_2
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ Tendsto (fun j => closedBall (w j) (δ j)) l (VitaliFamily.filterAt (vitaliFamily μ K) x)
refine' (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨_, fun ε hε => _⟩
case h
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : j ∈ δ ⁻¹' Ioi 0
⊢ closedBall (w j) (δ j) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
case refine'_1
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j
no goals
case h
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : j ∈ δ ⁻¹' Ioi 0
⊢ closedBall (w j) (δ j) ∈ VitaliFamily.setsAt (vitaliFamily μ K) x
exact closedBall_mem_vitaliFamily_of_dist_le_mul μ hj h'j
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε

case neg
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : ¬NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
case refine'_2
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
by_cases l.NeBot
case neg
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : ¬NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε

case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε

case neg
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : ¬NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
swap
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have hK : 0 ≤ K := by
  rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
  have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
  exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
have δpos := eventually_mem_of_tendsto_nhdsWithin δlim
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
replace δlim := tendsto_nhds_of_tendsto_nhdsWithin δlim
case hK
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
⊢ 0 < K + 1

case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
replace hK : 0 < K + 1
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
⊢ ∀ (x_1 : ι),
    (dist (δ x_1) 0 < ε / (K + 1) ∧ δ x_1 ∈ Ioi 0) ∧ x ∈ closedBall (w x_1) (K * δ x_1) →
      closedBall (w x_1) (δ x_1) ⊆ closedBall x ε
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
apply (((Metric.tendsto_nhds.mp δlim _ (div_pos hε hK)).and δpos).and xmem).mono
case pos.intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hjε : dist (δ j) 0 < ε / (K + 1)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
⊢ y ∈ closedBall x ε
case pos
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
⊢ ∀ (x_1 : ι),
    (dist (δ x_1) 0 < ε / (K + 1) ∧ δ x_1 ∈ Ioi 0) ∧ x ∈ closedBall (w x_1) (K * δ x_1) →
      closedBall (w x_1) (δ x_1) ⊆ closedBall x ε
rintro j ⟨⟨hjε, hj₀ : 0 < δ j⟩, hx⟩ y hy
case pos.intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
hjε : (K + 1) * δ j < ε
⊢ y ∈ closedBall x ε
case pos.intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hjε : dist (δ j) 0 < ε / (K + 1)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
⊢ y ∈ closedBall x ε
replace hjε : (K + 1) * δ j < ε := by
  simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff' hK).mp hjε
case pos.intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hj₀ : 0 < δ j
y : α
hjε : (K + 1) * δ j < ε
hx : dist x (w j) ≤ K * δ j
hy : dist y (w j) ≤ δ j
⊢ dist y x ≤ ε
case pos.intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
hjε : (K + 1) * δ j < ε
⊢ y ∈ closedBall x ε
simp only [mem_closedBall] at hx hy ⊢
no goals
case pos.intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hj₀ : 0 < δ j
y : α
hjε : (K + 1) * δ j < ε
hx : dist x (w j) ≤ K * δ j
hy : dist y (w j) ≤ δ j
⊢ dist y x ≤ ε
linarith [dist_triangle_right y x (w j)]
no goals
case neg
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : ¬NeBot l
⊢ ∀ᶠ (i : ι) in l, closedBall (w i) (δ i) ⊆ closedBall x ε
simp [not_neBot.1 h]
case intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : δ j ∈ Ioi 0
⊢ 0 ≤ K
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
⊢ 0 ≤ K
rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
case intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : δ j ∈ Ioi 0
this : 0 ≤ K * δ j
⊢ 0 ≤ K
case intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : δ j ∈ Ioi 0
⊢ 0 ≤ K
have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
no goals
case intro.intro
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[Ioi 0] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
h'j : δ j ∈ Ioi 0
this : 0 ≤ K * δ j
⊢ 0 ≤ K
exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this
no goals
case hK
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
hK : 0 ≤ K
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
⊢ 0 < K + 1
linarith
no goals
α : Type u_2
inst✝⁵ : MetricSpace α
inst✝⁴ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_1
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : NeBot l
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hx : x ∈ closedBall (w j) (K * δ j)
hjε : dist (δ j) 0 < ε / (K + 1)
hj₀ : 0 < δ j
y : α
hy : y ∈ closedBall (w j) (δ j)
⊢ (K + 1) * δ j < ε
simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff' hK).mp hjε