-- Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
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ᶜ < ε

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
hseq_dense : DenseRange seq
t : ℕ → Set (α × α)
hto : ∀ (i : ℕ), t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)
h_basis : (uniformity α).HasAntitoneBasis t
f : ℕ → ℕ → Set α := fun n m => UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n => s' n (δ n)
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
hseq_dense : DenseRange seq
t : ℕ → Set (α × α)
hto : ∀ (i : ℕ), t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)
h_basis : (uniformity α).HasAntitoneBasis t
f : ℕ → ℕ → Set α := fun n m => UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
u : ℕ → ℕ := fun n => s' n (δ n)
⊢ P (interUnionBalls seq u t)ᶜ < ε

Proof state:
case intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
hseq_dense : DenseRange seq
t : ℕ → Set (α × α)
hto : ∀ (i : ℕ), t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)
h_basis : (uniformity α).HasAntitoneBasis t
f : ℕ → ℕ → Set α := fun n m => UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
hseq_dense : DenseRange seq
t : ℕ → Set (α × α)
hto : ∀ (i : ℕ), t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)
h_basis : (uniformity α).HasAntitoneBasis t
f : ℕ → ℕ → Set α := fun n m => UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
δ : ℕ → ℝ≥0∞
hδ1 : ∀ (i : ℕ), 0 < δ i
hδ2 : ∑' (i : ℕ), δ i < ε
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Proof state:
case intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
hseq_dense : DenseRange seq
t : ℕ → Set (α × α)
hto : ∀ (i : ℕ), t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)
h_basis : (uniformity α).HasAntitoneBasis t
f : ℕ → ℕ → Set α := fun n m => UniformSpace.ball (seq m) (t n)
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (hto n).1

Result:
case intro.intro
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
hseq_dense : DenseRange seq
t : ℕ → Set (α × α)
hto : ∀ (i : ℕ), t i ∈ (uniformity α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)
h_basis : (uniformity α).HasAntitoneBasis t
f : ℕ → ℕ → Set α := fun n m => UniformSpace.ball (seq m) (t n)
h_univ : ∀ (n : ℕ), ⋃ m, f n m = univ
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Proof state:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : IsEmpty α
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
refine ⟨∅, by simp, ?_⟩

Result:
α : Type u_1
inst✝⁶ : MeasurableSpace α
inst✝⁵ : UniformSpace α
inst✝⁴ : CompleteSpace α
inst✝³ : SecondCountableTopology α
inst✝² : (uniformity α).IsCountablyGenerated
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
h✝ : IsEmpty α
⊢ P ∅ᶜ < ε