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

Tactic:
have h'' n : Prod.swap ⁻¹' t n = t n := SymmetricRel.eq (hto n).2.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 < ε
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

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

Result:
no goals

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
h3 : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → ∃ m, P (⋂ m', ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
choose! s' s'bound using h3

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
s' : ℕ → ℝ≥0∞ → ℕ
s'bound : ∀ (n : ℕ) (ε : ℝ≥0∞), 0 < ε → P (⋂ m', ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε
⊢ ∃ 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)
⊢ P (⋃ i, (⋃ m, ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ) < ε

Tactic:
refine ((measure_iUnion_le _).trans ?_).trans_lt 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 < ε
u : ℕ → ℕ := fun n => s' n (δ n)
⊢ ∑' (i : ℕ), P (⋃ m, ⋃ (_ : m ≤ u i), UniformSpace.ball (seq m) (Prod.swap ⁻¹' t i))ᶜ ≤ ∑' (i : ℕ), δ i

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 α
⊢ P ∅ᶜ < ε

Tactic:
rwa [Set.eq_empty_of_isEmpty ∅ᶜ, measure_empty]

Result:
no goals