-- 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₁.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))
⊢ NullMeasurableSet (⋃ n ∈ Finset.range (N + 1), f n) μ

Tactic:
exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
  (fun n _ ↦ (hf n).1.nullMeasurableSet)

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✝ t : Set X
t_mem : t ∈ 𝒜
ht✝ : MeasurableSet t
ε : ℝ
ε_pos : 0 < ε
⊢ (μ (t ∆ t)).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))
⊢ (↑N + 1) * (ε / (2 * (↑N + 1))) ≤ ε / 2

Tactic:
rw [div_mul_eq_div_mul_one_div, ← mul_assoc, mul_comm ((N : ℝ) + 1),
  mul_assoc]

Result:
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))
⊢ ε / 2 * ((↑N + 1) * (1 / (↑N + 1))) ≤ ε / 2

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))
⊢ dist (μ (⋃ n, f n)).toReal (μ (⋃ n ∈ Finset.range (N + 1), f n)).toReal < ε / 2

Tactic:
simp only [Finset.mem_range, Nat.lt_add_one_iff]

Result:
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))
⊢ dist (μ (⋃ n, f n)).toReal (μ (⋃ n, ⋃ (_ : n ≤ N), f n)).toReal < ε / 2

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))
⊢ ε / 2 * ((↑N + 1) * (1 / (↑N + 1))) ≤ ε / 2

Tactic:
exact mul_le_of_le_one_right (by linarith [ε_pos]) <|
  le_of_eq <| mul_one_div_cancel <| Nat.cast_add_one_ne_zero _

Result:
no goals

Proof state:
case h₁.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 iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)

Result:
no goals

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))
⊢ dist (μ (⋃ n, f n)).toReal (μ (⋃ n, ⋃ (_ : n ≤ N), f n)).toReal < ε / 2

Tactic:
exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))

Result:
no goals

Proof state:
case compl
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
ht✝ : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, (μ (t ∆ t_1)).toReal < ε
⊢ MeasurableSet tᶜ ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, (μ (tᶜ ∆ t_1)).toReal < ε

Tactic:
refine ⟨ht.1.compl, fun ε ε_pos ↦ ?_⟩

Result:
case compl
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
ht✝ : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, (μ (t ∆ t_1)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t_1 ∈ 𝒜, (μ (tᶜ ∆ t_1)).toReal < ε