-- Mathlib/Topology/MetricSpace/ShrinkingLemma.lean
theorem exists_locallyFinite_subset_iUnion_ball_radius_lt (hs : IsClosed s) {R : α → ℝ}
    (hR : ∀ x ∈ s, 0 < R x) :
    ∃ (ι : Type u) (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)

Proof state:
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ 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)

Tactic:
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))

Result:
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (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)

Proof state:
case intro.intro.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (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)

Tactic:
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⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (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)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (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)

Tactic:
exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (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)

Tactic:
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with
  ⟨ι, c, r', hr', hsub', hfin⟩

Result:
case intro.intro.intro.intro.intro
α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
this : ∀ x ∈ s, (𝓝 x).HasBasis (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)