-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite (h𝒜 : IsSetAlgebra 𝒜)
    (S : μ.FiniteSpanningSetsIn 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) :
    μ.MeasureDense 𝒜 where
  measurable s hs := hgen ▸ measurableSet_generateFrom hs
  approx s ms hμs ε ε_pos

Proof state:
case intro.intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this✝ : Filter.Tendsto (fun n => ((⇑μ ∘ fun n => T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n => T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ⊤)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine ⟨t ∩ T N, h𝒜.inter_mem t_mem (T_mem N), ?_⟩

Result:
case intro.intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this✝ : Filter.Tendsto (fun n => ((⇑μ ∘ fun n => T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n => T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ⊤)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ μ (s ∆ (t ∩ T N)) < ENNReal.ofReal ε

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this✝ : Filter.Tendsto (fun n => ((⇑μ ∘ fun n => T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n => T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ⊤)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) = ENNReal.ofReal ε

Tactic:
rw [← ofReal_add (by linarith [ε_pos]) (by linarith [ε_pos]), add_halves]

Result:
no goals

Proof state:
case hx
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n => T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ μ (⋃ n, T n ∩ s) ≠ ⊤

Tactic:
exact ne_top_of_le_ne_top hμs
  (measure_mono (iUnion_subset (fun i ↦ inter_subset_right ..)))

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n => T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
rw [← tendsto_toReal_iff] at this

Result:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this : Filter.Tendsto (fun n => ((⇑μ ∘ fun n => T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

case hf
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n => T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ ∀ (i : ℕ), (⇑μ ∘ fun n => T n ∩ s) i ≠ ⊤

case hx
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n => T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ μ (⋃ n, T n ∩ s) ≠ ⊤

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this✝ : Filter.Tendsto (fun n => ((⇑μ ∘ fun n => T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n => T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ⊤)
⊢ 0 < ε / 2

Tactic:
linarith [ε_pos]

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
have := tendsto_measure_iUnion_atTop (μ := μ) mono

Result:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := Accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ⊤
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n => T n ∩ s
this : Filter.Tendsto (⇑μ ∘ fun n => T n ∩ s) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)))
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε