-- 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 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 < ε
⊢ MeasurableSet (⋃ i, f i) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε

Tactic:
refine ⟨MeasurableSet.iUnion (fun n ↦ (hf n).1), fun ε ε_pos ↦ ?_⟩

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 < ε
⊢ ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε

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 < ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t_1 ∈ 𝒜, (μ (tᶜ ∆ t_1)).toReal < ε

Tactic:
obtain ⟨u, u_mem, hμtcu⟩ := ht.2 ε ε_pos

Result:
case compl.intro.intro
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 < ε
u : Set X
u_mem : u ∈ 𝒜
hμtcu : (μ (t ∆ u)).toReal < ε
⊢ ∃ t_1 ∈ 𝒜, (μ (tᶜ ∆ t_1)).toReal < ε

Proof state:
case iUnion.intro
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))
⊢ ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε

Tactic:
refine ⟨⋃ n ∈ Finset.range (N + 1), g n, h𝒜.biUnion_mem _ (fun i _ ↦ g_mem i), ?_⟩

Result:
case iUnion.intro
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))
⊢ (μ ((⋃ i, f i) ∆ ⋃ n ∈ Finset.range (N + 1), g n)).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✝ t : Set X
ht✝ : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, (μ (t ∆ t_1)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
u : Set X
u_mem : u ∈ 𝒜
hμtcu : (μ (t ∆ u)).toReal < ε
⊢ (μ (tᶜ ∆ uᶜ)).toReal < ε

Tactic:
rwa [compl_symmDiff_compl]

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 n => (μ (Accumulate f n)).toReal) Filter.atTop (nhds (μ (⋃ i, f i)).toReal)
⊢ ∃ t ∈ 𝒜, (μ ((⋃ i, f i) ∆ t)).toReal < ε

Tactic:
rcases Metric.tendsto_atTop.1 this (ε / 2) (by linarith [ε_pos]) with ⟨N, hN⟩

Result:
case iUnion.intro
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
⊢ ∃ 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
this : MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (s ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases this.2 ε ε_pos with ⟨t, t_mem, hμst⟩

Result:
case intro.intro
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
this : MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (s ∆ t)).toReal < ε
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
hμst : (μ (s ∆ t)).toReal < ε
⊢ ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε

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 ∈ Finset.range (N + 1), g n)).toReal < ε / 2

Tactic:
calc
  (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
  (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal
    ≤ (μ (⋃ n ∈ (Finset.range (N + 1)), f n ∆ g n)).toReal :=
        toReal_mono (measure_ne_top _ _) (measure_mono biSup_symmDiff_biSup_le)
  _ ≤ ∑ n ∈ Finset.range (N + 1), (μ (f n ∆ g n)).toReal := by
        rw [← toReal_sum (fun _ _ ↦ measure_ne_top _ _)]
        exact toReal_mono (ne_of_lt <| sum_lt_top.2 fun _ _ ↦ measure_lt_top μ _)
          (measure_biUnion_finset_le _ _)
  _ < ∑ n ∈ Finset.range (N + 1), (ε / (2 * (N + 1))) :=
        Finset.sum_lt_sum (fun i _ ↦ le_of_lt (hg i)) ⟨0, by simp, hg 0⟩
  _ ≤ ε / 2 := by
        simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul,
          Nat.cast_add, Nat.cast_one]
        rw [div_mul_eq_div_mul_one_div, ← mul_assoc, mul_comm ((N : ℝ) + 1),
          mul_assoc]
        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