awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ T N)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (s ∩ T N)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) ((s ∩ T N) ∆ (t ∩ T N)) : ℝ≥0∞)

Tactic:
exact measure_symmDiff_le _ _ _

Premises used: MeasureTheory.measure_symmDiff_le
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
ac : (μ : (a : Set X) → ℝ≥0∞) (s \ (s ∩ T N)) < ENNReal.ofReal (ε / 2)
bd : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t ∩ T N) < ENNReal.ofReal (ε / 2)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ (s ∩ T N)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t ∩ T N) : ℝ≥0∞) <
    ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)

Tactic:
apply ENNReal.add_lt_add

Premises used: ENNReal.add_lt_add
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
ac : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N)) < ε / 2
⊢ (μ : (a : Set X) → ℝ≥0∞) (s \ (s ∩ T N)) < ENNReal.ofReal (ε / 2)

Tactic:
rw [measure_diff
                    (inter_subset_left ..)
                    (ms.inter (hgen ▸ measurableSet_generateFrom (T_mem N))).nullMeasurableSet
                    (ne_top_of_le_ne_top hμs (measure_mono (inter_subset_left ..))),
                  lt_ofReal_iff_toReal_lt (sub_ne_top hμs),
                  toReal_sub_of_le (measure_mono (inter_subset_left ..)) hμs]

Premises used: ENNReal.sub_ne_top, MeasurableSet.nullMeasurableSet, Set.inter_subset_left, ENNReal.lt_ofReal_iff_toReal_lt, ne_top_of_le_ne_top, ENNReal.toReal_sub_of_le, MeasureTheory.measure_diff, MeasureTheory.measure_mono, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
ac : dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) s)) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N))) < ε / 2
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N)) < ε / 2

Tactic:
apply lt_of_le_of_lt (sub_le_dist ..)

Premises used: lt_of_le_of_lt, Real.sub_le_dist
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
ac :
  dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (univ ∩ s))) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N))) <
    ε / 2
⊢ dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) s)) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N))) < ε / 2

Tactic:
nth_rw 1 [← univ_inter s]

Premises used: Set.univ_inter
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
ac :
  dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (T N ∩ s)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), T i ∩ s))) <
    ε / 2
⊢ dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (univ ∩ s))) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N))) <
    ε / 2

Tactic:
rw [inter_comm s, dist_comm, ← T_spanning, iUnion_inter _ T]

Premises used: dist_comm, Set.iUnion_inter, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (T N ∩ s)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), T i ∩ s))) <
    ε / 2

Tactic:
apply hN N (le_refl _)

Premises used: le_refl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht bd bd₁ bd₂ bd₃ : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ t ∩ T N) < ENNReal.ofReal (ε / 2)

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

Premises used: MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
linarith : ε / 2 < 0 → 2 / 2 = 1
linarith₁ : ε / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : ε / 2 < 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ ε / 2

Tactic:
linarith [ε_pos]
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
rw : ENNReal.ofReal (ε / 2 + ε / 2) = ENNReal.ofReal ε
rw₁ rw₂ : ENNReal.ofReal ε = ENNReal.ofReal ε
⊢ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) = ENNReal.ofReal ε

Tactic:
rw [← ofReal_add (by linarith [ε_pos]) (by linarith [ε_pos]), add_halves]

Premises used: add_halves, ENNReal.ofReal_add
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this_1 :
  Filter.Tendsto
    (fun (n : ℕ) ↦ ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
    Filter.atTop (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) n))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s))) <
      ε / 2
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
μ₁ :
  (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ T N)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ (s ∩ T N)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t ∩ T N) : ℝ≥0∞)
μ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s \ (s ∩ T N)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t ∩ T N) : ℝ≥0∞) <
    ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
μ₃ : ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) = ENNReal.ofReal ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ T N)) < ENNReal.ofReal ε

Tactic:
calc
        μ (s ∆ (t ∩ T N))
          ≤ μ (s \ (s ∩ T N)) + μ ((s ∆ t) ∩ T N) := by
              rw [← symmDiff_of_le (inter_subset_left ..), symmDiff_comm _ s,
                inter_symmDiff_distrib_right]
              exact measure_symmDiff_le _ _ _
        _ < ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) := by
              apply ENNReal.add_lt_add
              · rw [measure_diff
                    (inter_subset_left ..)
                    (ms.inter (hgen ▸ measurableSet_generateFrom (T_mem N))).nullMeasurableSet
                    (ne_top_of_le_ne_top hμs (measure_mono (inter_subset_left ..))),
                  lt_ofReal_iff_toReal_lt (sub_ne_top hμs),
                  toReal_sub_of_le (measure_mono (inter_subset_left ..)) hμs]
                apply lt_of_le_of_lt (sub_le_dist ..)
                nth_rw 1 [← univ_inter s]
                rw [inter_comm s, dist_comm, ← T_spanning, iUnion_inter _ T]
                apply hN N (le_refl _)
              · rwa [← μ.restrict_apply' (hgen ▸ measurableSet_generateFrom (T_mem N))]
        _ = ENNReal.ofReal ε := by
              rw [← ofReal_add (by linarith [ε_pos]) (by linarith [ε_pos]), add_halves]

Premises used: ENNReal.ofReal, HDiv.hDiv, Inter.inter, SDiff.sdiff, OfNat.ofNat, DFunLike.coe, symmDiff
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this :
  Filter.Tendsto (α := ℕ) (β := ℝ≥0∞)
    (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ T n ∩ s : ℕ → ℝ≥0∞) Filter.atTop
    (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s)) : Filter ℝ≥0∞)
⊢ ∀ (i : ℕ), Ne (α := ℝ≥0∞) (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) i) ∞

Tactic:
fun n ↦ ne_top_of_le_ne_top hμs (measure_mono (inter_subset_right ..))

Premises used: ne_top_of_le_ne_top, MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this :
  Filter.Tendsto (α := ℕ) (β := ℝ≥0∞)
    (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ T n ∩ s : ℕ → ℝ≥0∞) Filter.atTop
    (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s)) : Filter ℝ≥0∞)
⊢ ∀ (i : ℕ), Ne (α := ℝ≥0∞) (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) i) ∞

Tactic:
exact fun n ↦ ne_top_of_le_ne_top hμs (measure_mono (inter_subset_right ..))

Premises used: ne_top_of_le_ne_top, MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this :
  Filter.Tendsto (α := ℕ) (β := ℝ≥0∞)
    (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ T n ∩ s : ℕ → ℝ≥0∞) Filter.atTop
    (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s)) : Filter ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ne_top_of_le_ne_top hμs
        (measure_mono (iUnion_subset (fun i ↦ inter_subset_right ..)))

Premises used: Set.iUnion_subset, ne_top_of_le_ne_top, MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
T : (x : ℕ) → Set X := accumulate (S.set (C := 𝒜))
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)
T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
mono : Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s
this :
  Filter.Tendsto (α := ℕ) (β := ℝ≥0∞)
    (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ T n ∩ s : ℕ → ℝ≥0∞) Filter.atTop
    (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s)) : Filter ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_top_of_le_ne_top hμs
        (measure_mono (iUnion_subset (fun i ↦ inter_subset_right ..)))

Premises used: Set.iUnion_subset, ne_top_of_le_ne_top, MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : IsSeparable μ
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
IsSeparable.exists_countable_measureDense

Premises used: MeasureTheory.IsSeparable.exists_countable_measureDense
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
⊢ (countableGeneratingSet X).Countable

Tactic:
have h := countable_countableGeneratingSet (α := X)