diff --git a/Mathlib.lean b/Mathlib.lean
index 9269de2ed24fa..08887c86a51c2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3718,6 +3718,7 @@ import Mathlib.MeasureTheory.Measure.Portmanteau
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.MeasureTheory.Measure.Regular
+import Mathlib.MeasureTheory.Measure.RegularityCompacts
 import Mathlib.MeasureTheory.Measure.Restrict
 import Mathlib.MeasureTheory.Measure.SeparableMeasure
 import Mathlib.MeasureTheory.Measure.Stieltjes
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index 92a5dcb5aa47b..8ac55f54b6fbc 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -626,6 +626,24 @@ theorem tendsto_measure_iInter_le {α ι : Type*} {_ : MeasurableSpace α} {μ :
   exact tendsto_atTop_iInf
     fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij
 
+/-- Some version of continuity of a measure in the emptyset using the intersection along a set of
+sets. -/
+theorem exists_measure_iInter_lt {α ι : Type*} {_ : MeasurableSpace α} {μ : Measure α}
+    [SemilatticeSup ι] [Countable ι] {f : ι → Set α}
+    (hm : ∀ i, NullMeasurableSet (f i) μ) {ε : ℝ≥0∞} (hε : 0 < ε) (hfin : ∃ i, μ (f i) ≠ ∞)
+    (hfem : ⋂ n, f n = ∅) : ∃ m, μ (⋂ n ≤ m, f n) < ε := by
+  let F m := μ (⋂ n ≤ m, f n)
+  have hFAnti : Antitone F :=
+      fun i j hij => measure_mono (biInter_subset_biInter_left fun k hki => le_trans hki hij)
+  suffices Filter.Tendsto F Filter.atTop (𝓝 0) by
+    rw [@ENNReal.tendsto_atTop_zero_iff_lt_of_antitone
+         _ (nonempty_of_exists hfin) _ _ hFAnti] at this
+    exact this ε hε
+  have hzero : μ (⋂ n, f n) = 0 := by
+    simp only [hfem, measure_empty]
+  rw [← hzero]
+  exact tendsto_measure_iInter_le hm hfin
+
 /-- The measure of the intersection of a decreasing sequence of measurable
 sets indexed by a linear order with first countable topology is the limit of the measures. -/
 theorem tendsto_measure_biInter_gt {ι : Type*} [LinearOrder ι] [TopologicalSpace ι]
diff --git a/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
new file mode 100644
index 0000000000000..1d8e91a4aa967
--- /dev/null
+++ b/Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
@@ -0,0 +1,248 @@
+/-
+Copyright (c) 2023 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne, Peter Pfaffelhuber
+-/
+import Mathlib.Analysis.SpecificLimits.Basic
+import Mathlib.MeasureTheory.Measure.Regular
+import Mathlib.Topology.MetricSpace.Polish
+import Mathlib.Topology.UniformSpace.Cauchy
+
+/-!
+# Inner regularity of finite measures
+
+The main result of this file is `theorem InnerRegularCompactLTTop`:
+A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
+`SecondCountableTopology E` is inner regular with respect to compact sets. In other
+words, a finite measure on such a space is a tight measure.
+
+Finite measures on Polish spaces are an important special case, which makes the result
+`theorem PolishSpace.innerRegular_isCompact_measurableSet` an important result in probability.
+-/
+
+open Set MeasureTheory
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {α : Type*} [MeasurableSpace α] {μ : Measure α}
+
+theorem innerRegularWRT_isCompact_closure_iff [TopologicalSpace α] [R1Space α] :
+    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed := by
+  constructor <;> intro h A hA r hr
+  · rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
+    exact ⟨closure K, closure_minimal hK1 hA, hK2, hK3.trans_le (measure_mono subset_closure)⟩
+  · rcases h hA r hr with ⟨K, ⟨hK1, hK2, hK3⟩⟩
+    refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
+    · simpa only [closure_closure, Function.comp_apply] using hK2.closure
+    · exact hK3.trans_le (measure_mono subset_closure)
+
+lemma innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure
+    [TopologicalSpace α] [R1Space α] :
+    μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
+      ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed := by
+  constructor <;> intro h A hA r hr
+  · obtain ⟨K, hK1, ⟨hK2, _⟩, hK4⟩ := h hA r hr
+    refine ⟨K, hK1, ?_, hK4⟩
+    simp only [closure_closure, Function.comp_apply]
+    exact hK2.closure
+  · obtain ⟨K, hK1, hK2, hK3⟩ := h hA r hr
+    refine ⟨closure K, closure_minimal hK1 hA, ?_, ?_⟩
+    · simpa only [isClosed_closure, and_true]
+    · exact hK3.trans_le (measure_mono subset_closure)
+
+lemma innerRegularWRT_isCompact_isClosed_iff [TopologicalSpace α] [R1Space α] :
+    μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed
+      ↔ μ.InnerRegularWRT IsCompact IsClosed :=
+  innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure.trans
+    innerRegularWRT_isCompact_closure_iff
+
+/--
+If predicate `p` is preserved under intersections with sets satisfying predicate `q`, and sets
+satisfying `p` cover the space arbitrarily well, then `μ` is inner regular with respect to
+predicates `p` and `q`.
+-/
+theorem innerRegularWRT_of_exists_compl_lt {p q : Set α → Prop} (hpq : ∀ A B, p A → q B → p (A ∩ B))
+    (hμ : ∀ ε, 0 < ε → ∃ K, p K ∧ μ Kᶜ < ε) :
+    μ.InnerRegularWRT p q := by
+  intro A hA r hr
+  obtain ⟨K, hK, hK_subset, h_lt⟩ : ∃ K, p K ∧ K ⊆ A ∧ μ (A \ K) < μ A - r := by
+    obtain ⟨K', hpK', hK'_lt⟩ := hμ (μ A - r) (tsub_pos_of_lt hr)
+    refine ⟨K' ∩ A, hpq K' A hpK' hA, inter_subset_right, ?_⟩
+    · refine (measure_mono fun x ↦ ?_).trans_lt hK'_lt
+      simp only [diff_inter_self_eq_diff, mem_diff, mem_compl_iff, and_imp, imp_self, imp_true_iff]
+  refine ⟨K, hK_subset, hK, ?_⟩
+  have h_lt' : μ A - μ K < μ A - r := le_measure_diff.trans_lt h_lt
+  exact lt_of_tsub_lt_tsub_left h_lt'
+
+theorem innerRegularWRT_isCompact_closure_of_univ [TopologicalSpace α]
+    (hμ : ∀ ε, 0 < ε → ∃ K, IsCompact (closure K) ∧ μ (Kᶜ) < ε) :
+    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed := by
+  refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ
+  have : IsCompact (closure s ∩ t) := hs.inter_right ht
+  refine this.of_isClosed_subset isClosed_closure ?_
+  refine (closure_inter_subset_inter_closure _ _).trans_eq ?_
+  rw [IsClosed.closure_eq ht]
+
+theorem exists_isCompact_closure_measure_compl_lt [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] (ε : ℝ≥0∞) (hε : 0 < ε) :
+    ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε := by
+  /-
+  If α is empty, the result is trivial.
+
+  Otherwise, fix a dense sequence `seq` and an antitone basis `t` of entourages. We find a sequence
+  of natural numbers `u n`, such that `interUnionBalls seq u t`, which is the intersection over
+  `n` of the `t n`-neighborhood of `seq 1, ..., seq (u n)`, covers the space arbitrarily well.
+  -/
+  cases isEmpty_or_nonempty α
+  case inl =>
+    refine ⟨∅, by simp, ?_⟩
+    rw [← Set.univ_eq_empty_iff.mpr]
+    · simpa only [compl_univ, measure_empty, ENNReal.coe_pos] using hε
+    · assumption
+  case inr =>
+    let seq := TopologicalSpace.denseSeq α
+    have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
+    obtain ⟨t : ℕ → Set (α × α),
+        hto : ∀ i, t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i),
+        h_basis : (uniformity α).HasAntitoneBasis t⟩ :=
+      (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
+    let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
+    have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (hto n).1
+    have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
+      refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
+      · exact (measurable_prod_mk_left (IsOpen.measurableSet (hto n).2.1)).compl.nullMeasurableSet
+      · rw [← compl_iUnion, h_univ, compl_univ]
+    choose! s' s'bound using h3
+    rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
+    classical
+    let u : ℕ → ℕ := fun n ↦ s' n (δ n)
+    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
+    rw [interUnionBalls, Set.compl_iInter]
+    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
+    refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
+    have h'' n : Prod.swap ⁻¹' t n = t n := SymmetricRel.eq (hto n).2.2
+    simp only [h'', compl_iUnion, ge_iff_le]
+    exact (s'bound n (δ n) (hδ1 n)).le
+
+theorem innerRegularWRT_isCompact_closure [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (IsCompact ∘ closure) IsClosed :=
+  innerRegularWRT_isCompact_closure_of_univ
+    (exists_isCompact_closure_measure_compl_lt P)
+
+theorem innerRegularWRT_isCompact_isClosed [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed := by
+  rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]
+  exact innerRegularWRT_isCompact_closure P
+
+theorem innerRegularWRT_isCompact [UniformSpace α] [CompleteSpace α]
+    [SecondCountableTopology α] [(uniformity α).IsCountablyGenerated]
+    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT IsCompact IsClosed := by
+  rw [← innerRegularWRT_isCompact_closure_iff]
+  exact innerRegularWRT_isCompact_closure P
+
+theorem innerRegularWRT_isCompact_isClosed_isOpen [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsOpen :=
+  (innerRegularWRT_isCompact_isClosed P).trans
+    (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)
+
+theorem innerRegularWRT_isCompact_isOpen [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT IsCompact IsOpen :=
+  (innerRegularWRT_isCompact P).trans
+    (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)
+
+/--
+A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
+`SecondCountableTopology E` is inner regular. In other words, a finite measure
+on such a space is a tight measure.
+-/
+instance InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegular := by
+  refine @Measure.InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite _ _ _ _
+      ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩ _
+  · exact innerRegularWRT_isCompact_isOpen P
+  · exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl
+
+/--
+A special case of `innerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable` for Polish
+spaces: A finite measure on a Polish space is a tight measure.
+-/
+instance InnerRegular_of_polishSpace [TopologicalSpace α]
+    [PolishSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegular := by
+  letI := upgradePolishSpace α
+  exact InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable P
+
+/--
+A measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with `SecondCountableTopology E`
+is inner regular for finite measure sets with respect to compact sets.
+-/
+instance InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable
+    [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
+    (μ : Measure α) :
+    μ.InnerRegularCompactLTTop := by
+  constructor; intro A ⟨hA1, hA2⟩ r hr
+  have IRC : Measure.InnerRegularCompactLTTop (μ.restrict A) := by
+    exact @Measure.InnerRegular.instInnerRegularCompactLTTop _ _ _ _
+        (@InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable _ _ _ _ _ _
+        (μ.restrict A) (@Restrict.isFiniteMeasure _ _ _ μ (fact_iff.mpr hA2.lt_top)))
+  have hA2' : (μ.restrict A) A ≠ ⊤ := by
+    rwa [Measure.restrict_apply_self]
+  have hr' : r < μ.restrict A A := by
+    rwa [Measure.restrict_apply_self]
+  obtain ⟨K, ⟨hK1, hK2, hK3⟩⟩ := @MeasurableSet.exists_lt_isCompact_of_ne_top
+      _ _ (μ.restrict A) _ IRC _ hA1 hA2' r hr'
+  use K, hK1, hK2
+  rwa [Measure.restrict_eq_self μ hK1] at hK3
+
+/--
+A special case of `innerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable`
+for Polish spaces: A measure `μ` on a Polish space inner regular for finite measure sets with
+respect to compact sets.
+-/
+instance InnerRegularCompactLTTop_of_polishSpace
+    [TopologicalSpace α] [PolishSpace α] [BorelSpace α] (μ : Measure α) :
+    μ.InnerRegularCompactLTTop := by
+  letI := upgradePolishSpace α
+  exact InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable μ
+
+theorem innerRegular_isCompact_isClosed_measurableSet_of_finite [PseudoEMetricSpace α]
+    [CompleteSpace α] [SecondCountableTopology α] [BorelSpace α]
+    (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
+  suffices P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s)
+      fun s ↦ MeasurableSet s ∧ P s ≠ ∞ by
+    convert this
+    simp only [eq_iff_iff, iff_self_and]
+    exact fun _ ↦ measure_ne_top P _
+  refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_
+  · exact innerRegularWRT_isCompact_isClosed_isOpen P
+  · rintro s t ⟨hs_compact, hs_closed⟩ ht_open
+    rw [diff_eq]
+    exact ⟨hs_compact.inter_right ht_open.isClosed_compl,
+      hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩
+
+/--
+On a Polish space, any finite measure is regular with respect to compact and closed sets. In
+particular, a finite measure on a Polish space is a tight measure.
+-/
+theorem PolishSpace.innerRegular_isCompact_isClosed_measurableSet [TopologicalSpace α]
+    [PolishSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] :
+    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet := by
+  letI := upgradePolishSpace α
+  exact innerRegular_isCompact_isClosed_measurableSet_of_finite P
+
+end MeasureTheory
diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean
index 418685fd8c5d4..74df527096cba 100644
--- a/Mathlib/Topology/Instances/ENNReal.lean
+++ b/Mathlib/Topology/Instances/ENNReal.lean
@@ -280,6 +280,35 @@ protected theorem tendsto_atTop_zero [Nonempty β] [SemilatticeSup β] {f : β 
     Tendsto f atTop (𝓝 0) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε :=
   .trans (atTop_basis.tendsto_iff nhds_zero_basis_Iic) (by simp only [true_and]; rfl)
 
+theorem tendsto_atTop_zero_iff_le_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β]
+    {f : β → ℝ≥0∞} (hf : Antitone f) :
+    Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n ≤ ε := by
+  rw [ENNReal.tendsto_atTop_zero]
+  refine ⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩
+  · obtain ⟨n, hn⟩ := h ε hε
+    exact ⟨n, hn n le_rfl⟩
+  · obtain ⟨n, hn⟩ := h ε hε
+    exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩
+
+theorem tendsto_atTop_zero_iff_lt_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β]
+    {f : β → ℝ≥0∞} (hf : Antitone f) :
+    Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n < ε := by
+  rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]
+  constructor <;> intro h ε hε
+  · obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
+      (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨ne_of_gt hε, ENNReal.two_ne_top⟩)⟩)
+    · refine ⟨n, hn.trans_lt ?_⟩
+      by_cases hε_top : ε = ∞
+      · rw [hε_top]
+        exact (min_le_left _ _).trans_lt ENNReal.one_lt_top
+      refine (min_le_right _ _).trans_lt ?_
+      rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]
+      conv_lhs => rw [← mul_one ε]
+      rw [ENNReal.mul_lt_mul_left hε.ne' hε_top]
+      norm_num
+  · obtain ⟨n, hn⟩ := h ε hε
+    exact ⟨n, hn.le⟩
+
 theorem tendsto_sub : ∀ {a b : ℝ≥0∞}, (a ≠ ∞ ∨ b ≠ ∞) →
     Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 - p.2) (𝓝 (a, b)) (𝓝 (a - b))
   | ∞, ∞, h => by simp only [ne_eq, not_true_eq_false, or_self] at h
diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
index b8ae4225ddef4..e482affe0f2b0 100644
--- a/Mathlib/Topology/UniformSpace/Cauchy.lean
+++ b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -645,6 +645,34 @@ theorem CauchySeq.totallyBounded_range {s : ℕ → α} (hs : CauchySeq s) :
   rcases le_total m n with hm | hm
   exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]
 
+/-- Given a family of points `xs n`, a family of entourages `V n` of the diagonal and a family of
+natural numbers `u n`, the intersection over `n` of the `V n`-neighborhood of `xs 1, ..., xs (u n)`.
+Designed to be relatively compact when `V n` tends to the diagonal. -/
+def interUnionBalls (xs : ℕ → α) (u : ℕ → ℕ) (V : ℕ → Set (α × α)) : Set α :=
+  ⋂ n, ⋃ m ≤ u n, UniformSpace.ball (xs m) (Prod.swap ⁻¹' V n)
+
+lemma totallyBounded_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) :
+    TotallyBounded (interUnionBalls xs u U) := by
+  rw [Filter.HasBasis.totallyBounded_iff H]
+  intro i _
+  have h_subset : interUnionBalls xs u U
+      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
+    fun x hx ↦ Set.mem_iInter.1 hx i
+  classical
+  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
+  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
+    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
+  exact h_subset hx
+
+/-- The construction `interUnionBalls` is used to have a relatively compact set. -/
+theorem isCompact_closure_interUnionBalls {p : ℕ → Prop} {U : ℕ → Set (α × α)}
+    (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) :
+    IsCompact (closure (interUnionBalls xs u U)) := by
+  rw [isCompact_iff_totallyBounded_isComplete]
+  refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
+  exact totallyBounded_interUnionBalls H xs u
+
 /-!
 ### Sequentially complete space