-- 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:
α : 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 < ε
⊢ ∃ m, P (⋂ m', ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε

Tactic:
refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_

Result:
case refine_1
α : 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 < ε
m : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P

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)ᶜ = ∅

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
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)

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)
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Proof state:
case refine_1
α : 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 < ε
m : ℕ
⊢ NullMeasurableSet (f n m)ᶜ P

Tactic:
exact (measurable_prod_mk_left (IsOpen.measurableSet (hto n).2.1)).compl.nullMeasurableSet

Result:
no goals

Proof state:
case inl
α : 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ᶜ < ε

case inr
α : 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 α
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
case inl =>
  refine ⟨∅, by simp, ?_⟩
  rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]

Result:
case inr
α : 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 α
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε