-- Mathlib/MeasureTheory/Measure/OpenPos.lean
/-- A σ-compact measure zero subset is meagre.
(More generally, every Fσ set of measure zero is meagre.) -/
lemma IsMeagre.of_isSigmaCompact_null [T2Space X] (h₁s : IsSigmaCompact s) (h₂s : μ s = 0) :
    IsMeagre s

Proof state:
case intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ IsMeagre s

Tactic:
rw [isMeagre_iff_countable_union_isNowhereDense]

Result:
case intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
n : ℕ
⊢ IsNowhereDense (K n)

Tactic:
have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
n : ℕ
this : μ (K n) = 0
⊢ IsNowhereDense (K n)

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
n : ℕ
this : μ (K n) = 0
⊢ IsNowhereDense (K n)

Tactic:
exact .of_isClosed_null (hcompact n).isClosed this

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ ∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S

Tactic:
exact ⟨range K, fun t ⟨n, hn⟩ ↦ hn ▸ h n, countable_range K, hcover.symm.subset⟩

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
⊢ IsMeagre s

Tactic:
have h (n : ℕ) : IsNowhereDense (K n) := by
  have : μ (K n) = 0 := measure_mono_null (hcover ▸ subset_iUnion K n) h₂s
  exact .of_isClosed_null (hcompact n).isClosed this

Result:
case intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
h : ∀ (n : ℕ), IsNowhereDense (K n)
⊢ IsMeagre s

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₁s : IsSigmaCompact s
h₂s : μ s = 0
⊢ IsMeagre s

Tactic:
rcases h₁s with ⟨K, hcompact, hcover⟩

Result:
case intro.intro
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
s : Set X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : T2Space X
h₂s : μ s = 0
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcover : ⋃ n, K n = s
⊢ IsMeagre s