-- 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✝ : IsEmpty α
⊢ IsCompact (closure ∅)

Tactic:
simp

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

Tactic:
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

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

Tactic:
simp only [h'', compl_iUnion, ge_iff_le]

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

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

Tactic:
let seq := TopologicalSpace.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 α
⊢ ∃ 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 < ε
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
cases isEmpty_or_nonempty α

Result:
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ᶜ < ε

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

Tactic:
let u : ℕ → ℕ := fun n ↦ s' n (δ 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)
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε