-- 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:
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
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
have mono : Monotone (fun n ↦ (T n) ∩ s) := fun m n hmn ↦ inter_subset_inter_left s
    (biUnion_subset_biUnion_left fun k hkm ↦ Nat.le_trans hkm hmn)

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
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < 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
n : ℕ
⊢ T n ∈ 𝒜

Tactic:
simpa using h𝒜.biUnion_mem {k | k ≤ n}.toFinset (fun k _ ↦ S.set_mem k)

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 => ((⇑μ ∘ 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)
⊢ 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
this : Filter.Tendsto (fun n => ((⇑μ ∘ fun n => T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
⊢ ε / 2 > 0

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
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)) ≤ μ (s \ (s ∩ T N)) + μ (s ∆ t ∩ T N)

Tactic:
rw [← symmDiff_of_le (inter_subset_left ..), symmDiff_comm _ s,
  inter_symmDiff_distrib_right]

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)
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)) ≤ μ (s ∆ (s ∩ T N)) + μ ((s ∩ T N) ∆ (t ∩ T N))

Proof state:
case bd
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 (ε / 2)

Tactic:
rwa [← μ.restrict_apply' (hgen ▸ measurableSet_generateFrom (T_mem N))]

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 ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
have T_finite (n) : μ (T n) < ∞ := by
  simpa using measure_biUnion_lt_top {k | k ≤ n}.toFinset.finite_toSet
    (fun k _ ↦ S.finite k)

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 ∈ 𝒜, μ (s ∆ t) < 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 ∈ 𝒜
n : ℕ
⊢ μ (T n) < ⊤

Tactic:
simpa using measure_biUnion_lt_top {k | k ≤ n}.toFinset.finite_toSet
  (fun k _ ↦ S.finite k)

Result:
no goals