[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with ⟨v, hsv, hvc, hcv⟩
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
have := fun i => exists_lt_subset_ball (hvc i) (hcv i)
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r', r' < r i ∧ v i ⊆ ball (c i) r'
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
choose r' hlt hsub using this
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i < r i
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
[PROOFSTEP]
exact ⟨r', hsv.trans <| iUnion_mono <| hsub, hlt⟩
[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
rcases exists_subset_iUnion_closed_subset hs (fun i => @isOpen_ball _ _ (c i) (r i)) uf us with ⟨v, hsv, hvc, hcv⟩
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
have := fun i => exists_pos_lt_subset_ball (hr i) (hvc i) (hcv i)
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
this : ∀ (i : ι), ∃ r', r' ∈ Ioo 0 (r i) ∧ v i ⊆ ball (c i) r'
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
choose r' hlt hsub using this
[GOAL]
case intro.intro.intro
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r✝ : ℝ
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed s
uf : ∀ (x : α), x ∈ s → Set.Finite {i | x ∈ ball (c i) (r i)}
us : s ⊆ ⋃ (i : ι), ball (c i) (r i)
v : ι → Set α
hsv : s ⊆ iUnion v
hvc : ∀ (i : ι), IsClosed (v i)
hcv : ∀ (i : ι), v i ⊆ ball (c i) (r i)
r' : ι → ℝ
hlt : ∀ (i : ι), r' i ∈ Ioo 0 (r i)
hsub : ∀ (i : ι), v i ⊆ ball (c i) (r' i)
⊢ ∃ r', s ⊆ ⋃ (i : ι), ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)
[PROOFSTEP]
exact ⟨r', hsv.trans <| iUnion_mono hsub, hlt⟩
[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
  nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))
[GOAL]
α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
x : α
r : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
this : ∀ (x : α), x ∈ s → Filter.HasBasis (𝓝 x) (fun r => 0 < r ∧ r < R x) fun r => ball x r
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with ⟨ι, c, r', hr', hsub', hfin⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
ι✝ : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c✝ : ι✝ → α
x : α
r : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
this : ∀ (x : α), x ∈ s → Filter.HasBasis (𝓝 x) (fun r => 0 < r ∧ r < R x) fun r => ball x r
ι : Type u
c : ι → α
r' : ι → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)
hfin : LocallyFinite fun a => ball (c a) (r' a)
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs (fun x _ => hfin.point_finite x) hsub' with
  ⟨r, hsub, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
ι✝ : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c✝ : ι✝ → α
x : α
r✝ : ℝ
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ (x : α), x ∈ s → 0 < R x
this : ∀ (x : α), x ∈ s → Filter.HasBasis (𝓝 x) (fun r => 0 < r ∧ r < R x) fun r => ball x r
ι : Type u
c : ι → α
r' : ι → ℝ
hr' : ∀ (a : ι), c a ∈ s ∧ 0 < r' a ∧ r' a < R (c a)
hsub' : s ⊆ ⋃ (a : ι), ball (c a) (r' a)
hfin : LocallyFinite fun a => ball (c a) (r' a)
r : ι → ℝ
hsub : s ⊆ ⋃ (i : ι), ball (c i) (r i)
hlt : ∀ (i : ι), r i ∈ Ioo 0 (r' i)
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i => ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), ball (c i) (r i)
[PROOFSTEP]
exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩
