Exists finite inner ball cover with card

theorem exists_finite_inner_ball_cover_with_card    {d : ℕ} [NeZero d]    {x₀ : EuclideanSpace ℝ (Fin d)}    {r ρ R : ℝ}    (_hr : 0 < r)    (hρ : 0 < ρ)    (hbuffer : r + 2 * ρ < R) :    ∃ t : Finset (EuclideanSpace ℝ (Fin d)),      t.card ≤ Nat.ceil ((4 * r / ρ + 1) ^ 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  classical  have hquarter : 0 < ρ / 4 := by positivity  obtain ⟨s, hs_mem, hs_cover, _⟩ :=    exists_finite_inner_ball_cover      (d := d) (x₀ := x₀) (r := r) (ρ := ρ / 4) (R := R)      (by positivity) hquarter (by linarith)  obtain ⟨t, ht_subset, ht_sep, ht_net⟩ :=    exists_maximal_separated_subfinset s (δ := ρ / 2) (by positivity)  have ht_mem : ∀ c ∈ t, c ∈ Metric.closedBall x₀ r := by    intro c hc    exact hs_mem c (ht_subset hc)  have hcover : Metric.closedBall x₀ r ⊆ ⋃ c ∈ t, Metric.ball c ρ := by    intro x hx    have hxcover : x ∈ ⋃ c ∈ s, Metric.ball c (ρ / 4) := hs_cover hx    rw [Set.mem_iUnion] at hxcover    obtain ⟨a, hxcover⟩ := hxcover    rw [Set.mem_iUnion] at hxcover    obtain ⟨ha, hxa⟩ := hxcover    obtain ⟨c, hc, hac⟩ := ht_net a ha    refine Set.mem_iUnion.2 ⟨c, Set.mem_iUnion.2 ⟨hc, ?_⟩⟩    refine Metric.mem_ball.2 ?_    have hxa' : dist x a < ρ / 4 := by      simpa using hxa    calc      dist x c ≤ dist x a + dist a c := dist_triangle _ _ _      _ < ρ / 4 + ρ / 2 := by linarith      _ < ρ := by linarith  have hbuffer' : ∀ c ∈ t, Metric.closedBall c (2 * ρ) ⊆ Metric.ball x₀ R := by    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 := by simpa [add_comm, add_left_comm, add_assoc] using hbuffer  have hdisj :      (↑t : Set (EuclideanSpace ℝ (Fin d))).PairwiseDisjoint (fun c => Metric.ball c (ρ / 4)) := by    intro c hc c' hc' hne    change Disjoint (Metric.ball c (ρ / 4)) (Metric.ball c' (ρ / 4))    rw [Set.disjoint_left]    intro x hxc hxc'    have hsep : ρ / 2 ≤ dist c c' := ht_sep hc hc' hne    have hxc1 : dist x c < ρ / 4 := by      simpa using hxc    have hxc2 : dist x c' < ρ / 4 := by      simpa using hxc'    have hdist : dist c c' < ρ / 2 := by      calc        dist c c' ≤ dist c x + dist x c' := dist_triangle _ _ _        _ < ρ / 4 + ρ / 4 := by              simpa [dist_comm] using add_lt_add_of_lt_of_lt hxc1 hxc2        _ = ρ / 2 := by ring    exact False.elim ((not_lt_of_ge hsep) hdist)  have hsmall_subset :      (⋃ c ∈ t, Metric.ball c (ρ / 4)) ⊆ Metric.ball x₀ (r + ρ / 4) := by    intro x hx    rw [Set.mem_iUnion] at hx    obtain ⟨c, hx⟩ := hx    rw [Set.mem_iUnion] at hx    obtain ⟨hc, hxc⟩ := hx    have hc' : dist c x₀ ≤ r := by      simpa using ht_mem c hc    have hxc' : dist x c < ρ / 4 := by      simpa using hxc    refine Metric.mem_ball.2 ?_    calc      dist x x₀ ≤ dist x c + dist c x₀ := dist_triangle _ _ _      _ < ρ / 4 + r := by linarith      _ = r + ρ / 4 := by ring  have hsum_le :      ∑ c ∈ t, volume.real (Metric.ball c (ρ / 4))        ≤ volume.real (Metric.ball x₀ (r + ρ / 4)) := by    rw [← measureReal_biUnion_finset (μ := volume) hdisj (fun c hc => measurableSet_ball)      (fun c hc => (measure_ball_lt_top (μ := volume) (x := c) (r := ρ / 4)).ne)]    exact measureReal_mono hsmall_subset  have hsum_eq :      ∑ c ∈ t, volume.real (Metric.ball c (ρ / 4)) =        (t.card : ℝ) *          ((ρ / 4) ^ d * volume.real (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1)) := by    calc      ∑ c ∈ t, volume.real (Metric.ball c (ρ / 4))          = ∑ c ∈ t, ((ρ / 4) ^ d * volume.real (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1)) := by              refine Finset.sum_congr rfl ?_              intro c hc              exact volumeReal_ball_eq c hquarter      _ = (t.card : ℝ) *            ((ρ / 4) ^ d * volume.real (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1)) := by            simp [mul_left_comm]  have hfactor : (ρ / 4) * (4 * r / ρ + 1) = r + ρ / 4 := by    calc      (ρ / 4) * (4 * r / ρ + 1) = (ρ / 4) * (4 * r / ρ) + ρ / 4 := by ring      _ = r + ρ / 4 := by field_simp [hρ.ne']  have houter_pos : 0 < r + ρ / 4 := by positivity  have houter_eq :      volume.real (Metric.ball x₀ (r + ρ / 4)) =        ((4 * r / ρ + 1) ^ d) *          ((ρ / 4) ^ d * volume.real (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1)) := by    rw [volumeReal_ball_eq x₀ houter_pos, ← hfactor, mul_pow]    ring  have hunit_pos : 0 < volume.real (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1) := by    exact ENNReal.toReal_pos      (Metric.measure_ball_pos volume (0 : EuclideanSpace ℝ (Fin d)) zero_lt_one).ne'      measure_ball_lt_top.ne  have hconst_pos :      0 < (ρ / 4) ^ d * volume.real (Metric.ball (0 : EuclideanSpace ℝ (Fin d)) 1) := by    exact mul_pos (by positivity) hunit_pos  have hcard_real : (t.card : ℝ) ≤ (4 * r / ρ + 1) ^ d := by    rw [hsum_eq, houter_eq] at hsum_le    nlinarith [hconst_pos]  have hcard : t.card ≤ Nat.ceil ((4 * r / ρ + 1) ^ d) := by    exact_mod_cast hcard_real.trans (Nat.le_ceil ((4 * r / ρ + 1) ^ d))  exact ⟨t, hcard, ht_mem, hcover, hbuffer'⟩