Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: 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
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_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 : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ (μ ((⋃ n, f n) \ ⋃ n ∈ Finset.range (N + 1), f n)).toReal < ε / 2

Tactic:
rw [measure_sdiff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]

Goal state after:
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
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_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 : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ (μ (⋃ n, f n)).toReal - (μ (⋃ n ∈ Finset.range (N + 1), f n)).toReal < ε / 2

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
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_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 : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ μ (⋃ n ∈ Finset.range (N + 1), f n) ≤ μ (⋃ n, f n)

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
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_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 : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ ⋃ n ∈ Finset.range (N + 1), f n ⊆ ⋃ n, f n

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
f : ℕ → Set X
hs✝ : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
ε : ℝ
ε_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 : ℕ), μ.real (f n ∆ g n) < ε / (2 * (↑N + 1))
⊢ NullMeasurableSet (⋃ n ∈ Finset.range (N + 1), f n) μ