-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem isSeparable_of_sigmaFinite [CountablyGenerated X] [SigmaFinite μ] :
    IsSeparable μ where
  exists_countable_measureDense

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
have count_𝒜 : 𝒜.Countable :=
  countable_union.2 ⟨h, countable_iff_exists_subset_range.2
    ⟨μ.toFiniteSpanningSetsIn.set, fun _ hx ↦ hx⟩⟩

Result:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Proof state:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Tactic:
rw [← hgen]

Result:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Proof state:
case refine_2.empty
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s : Set X
⊢ MeasurableSet ∅

Tactic:
exact MeasurableSet.empty

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
have hgen := generateFrom_countableGeneratingSet (α := X)

Result:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Proof state:
case refine_2.base
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
t_mem : t ∈ 𝒜
⊢ MeasurableSet t

Tactic:
rcases t_mem with t_mem | ⟨n, rfl⟩

Result:
case refine_2.base.inl
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
t_mem : t ∈ countableGeneratingSet X
⊢ MeasurableSet t

case refine_2.base.inr.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s : Set X
n : ℕ
⊢ MeasurableSet (μ.toFiniteSpanningSetsIn.set n)

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
have h := countable_countableGeneratingSet (α := X)

Result:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
⊢ ∃ 𝒜, 𝒜.Countable ∧ μ.MeasureDense 𝒜

Proof state:
case refine_2.base.inl
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
t_mem : t ∈ countableGeneratingSet X
⊢ MeasurableSet t

Tactic:
exact hgen ▸ measurableSet_generateFrom t_mem

Result:
no goals

Proof state:
case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
⊢ MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Tactic:
exact generateFrom_mono <| le_trans self_subset_generateSetAlgebra <|
  generateSetAlgebra_mono <| subset_union_left ..

Result:
no goals

Proof state:
case refine_2.union
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s t u : Set X
hs✝ : generateSetAlgebra 𝒜 t
ht✝ : generateSetAlgebra 𝒜 u
t_mem : MeasurableSet t
u_mem : MeasurableSet u
⊢ MeasurableSet (t ∪ u)

Tactic:
exact MeasurableSet.union t_mem u_mem

Result:
no goals

Proof state:
case refine_2.compl
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
hs✝ : generateSetAlgebra 𝒜 t
t_mem : MeasurableSet t
⊢ MeasurableSet tᶜ

Tactic:
exact MeasurableSet.compl t_mem

Result:
no goals

Proof state:
case refine_2.base.inr.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst✝¹ : CountablyGenerated X
inst✝ : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) := countableGeneratingSet X ∪ {x | ∃ n, μ.toFiniteSpanningSetsIn.set n = x}
count_𝒜 : 𝒜.Countable
s : Set X
n : ℕ
⊢ MeasurableSet (μ.toFiniteSpanningSetsIn.set n)

Tactic:
exact μ.toFiniteSpanningSetsIn.set_mem n

Result:
no goals