Exists finite inner ball cover

theorem exists_finite_inner_ball_cover    {d : ℕ} [NeZero d]    {x₀ : EuclideanSpace ℝ (Fin d)}    {r ρ R : ℝ}    (_hr : 0 < r)    (hρ : 0 < ρ)    (hbuffer : r + 2 * ρ < R) :    ∃ t : Finset (EuclideanSpace ℝ (Fin d)),      (∀ c ∈ t, c ∈ Metric.closedBall x₀ r) ∧      Metric.closedBall x₀ r ⊆ ⋃ c ∈ t, Metric.ball c ρ ∧      (∀ c ∈ t, Metric.closedBall c (2 * ρ) ⊆ Metric.ball x₀ R) := by  obtain ⟨t, ht_mem, hcover⟩ :=    (isCompact_closedBall x₀ r).elim_nhds_subcover      (fun x => Metric.ball x ρ)      (fun x hx => Metric.ball_mem_nhds x hρ)  have hbuffer' : 2 * ρ + r < R := by    simpa [add_comm, add_left_comm, add_assoc] using hbuffer  refine ⟨t, ht_mem, hcover, ?_⟩  intro c hc x hx  have hc' : dist c x₀ ≤ r := by    simpa using ht_mem c hc  have hx' : dist x c ≤ 2 * ρ := by    simpa using hx  refine Metric.mem_ball.2 ?_  calc    dist x x₀ ≤ dist x c + dist c x₀ := dist_triangle _ _ _    _ ≤ 2 * ρ + r := by linarith    _ < R := hbuffer'