-- 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)
⊢ ∑' (i : ℕ), P (⋃ m, ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ ≤ ∑' (i : ℕ), δ i

Tactic:
refine ENNReal.tsum_le_tsum (fun n ↦ ?_)

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)
n : ℕ
⊢ P (⋃ m, ⋃ (_ : m ≤ u n), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t n))ᶜ ≤ δ n

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)
⊢ P (interUnionBalls seq u t)ᶜ < ε

Tactic:
rw [interUnionBalls, Set.compl_iInter]

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 (⋃ i, (⋃ m, ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε

Proof state:
case refine_2
α : 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
n : ℕ
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⋂ n_1, (f n n_1)ᶜ = ∅

Tactic:
rw [← compl_iUnion, h_univ, compl_univ]

Result:
no goals

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)
n : ℕ
h'' : ∀ (n : ℕ), Prod.swap ⁻¹' t n = t n
⊢ P (⋂ i, ⋂ (_ : i ≤ u n), (UniformSpace.ball (seq i) (t n))ᶜ) ≤ δ n

Tactic:
exact (s'bound n (δ n) (hδ1 n)).le

Result:
no goals

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✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α

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✝ : Nonempty α
seq : ℕ → α := TopologicalSpace.denseSeq α
hseq_dense : DenseRange seq
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε