-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite [IsFiniteMeasure μ]
    (h𝒜 : IsSetAlgebra 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) : μ.MeasureDense 𝒜 where
  measurable s hs := hgen ▸ measurableSet_generateFrom hs
  approx s ms

Proof state:
case h₁
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n => (μ (Accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (Accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), (μ (f n ∆ g n)).toReal < ε / (2 * (↑N + 1))
⊢ μ (⋃ n ∈ Finset.range (N + 1), f n) ≤ μ (⋃ n, f n)

Tactic:
exact measure_mono <| iUnion_subset <|
  fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
ε : ℝ
ε_pos : 0 < ε
⊢ (μ (∅ ∆ ∅)).toReal < ε

Tactic:
simpa

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n => (μ (Accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (Accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), (μ (f n ∆ g n)).toReal < ε / (2 * (↑N + 1))
⊢ 0 ≤ ε / 2

Tactic:
linarith [ε_pos]

Result:
no goals

Proof state:
case hC
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ t : Set X
t_mem : t ∈ 𝒜
ht✝ : MeasurableSet t
⊢ MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, (μ (t ∆ t_1)).toReal < ε

Tactic:
exact ⟨hgen ▸ measurableSet_generateFrom t_mem, fun ε ε_pos ↦ ⟨t, t_mem, by simpa⟩⟩

Result:
no goals

Proof state:
case iUnion
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε

Tactic:
have := tendsto_measure_iUnion_accumulate (μ := μ) (f := f)

Result:
case iUnion
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun i => μ (Accumulate f i)) Filter.atTop (nhds (μ (⋃ i, f i)))
⊢ ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n => (μ (Accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
⊢ ε / 2 > 0

Tactic:
linarith [ε_pos]

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n => (μ (Accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (Accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
g : ℕ → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), (μ (f n ∆ g n)).toReal < ε / (2 * (↑N + 1))
⊢ 0 ∈ Finset.range (N + 1)

Tactic:
simp

Result:
no goals

Proof state:
case empty
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
⊢ MeasurableSet ∅ ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (∅ ∆ t)).toReal < ε

Tactic:
exact ⟨MeasurableSet.empty, fun ε ε_pos ↦ ⟨∅, h𝒜.empty_mem, by simpa⟩⟩

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n => (μ (Accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist (μ (Accumulate f n)).toReal (μ (⋃ i, f i)).toReal < ε / 2
n : ℕ
⊢ 0 < 2 * (↑N + 1)

Tactic:
linarith

Result:
no goals

Proof state:
case iUnion
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun i => μ (Accumulate f i)) Filter.atTop (nhds (μ (⋃ i, f i)))
⊢ ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε

Tactic:
rw [← tendsto_toReal_iff (fun _ ↦ measure_ne_top _ _) (measure_ne_top _ _)] at this

Result:
case iUnion
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst✝ : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
x✝ : Set X
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (f n ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
this : Filter.Tendsto (fun n => (μ (Accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
⊢ ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε