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)
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 : ℕ) ↦ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n))) Filter.atTop
    (nhds (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))))
N : ℕ
hN :
  ∀ n ≥ N,
    dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
        (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
      ε / 2
g : (n : ℕ) → Set X
g_mem : ∀ (n : ℕ), g n ∈ 𝒜
hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
n : μ.real (⋃ n ∈ Finset.range (N + 1), f n ∆ g n) ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n)
n₁ : ∑ n ∈ Finset.range (N + 1), ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) ≤ ε / 2
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2

Tactic:
calc
                    (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
                    (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal
                      ≤ μ.real (⋃ n ∈ (Finset.range (N + 1)), f n ∆ g n) :=
                          toReal_mono (measure_ne_top _ _) (measure_mono biSup_symmDiff_biSup_le)
                    _ ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n) := by
                          simp_rw [measureReal_def, ← 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 _

Premises used: HMul.hMul, biSup_symmDiff_biSup_le, MeasureTheory.Measure.real, le_of_lt, MeasureTheory.measure_ne_top, HDiv.hDiv, Nat.cast, Finset.range, ENNReal.toReal, HAdd.hAdd, And.intro, MeasureTheory.measure_mono, Exists.intro, Finset.sum_lt_sum, OfNat.ofNat, ENNReal.toReal_mono, DFunLike.coe, Set.iUnion, symmDiff
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 ∈ 𝒜, μ.real (s ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
rcases :
  ∀ (t : Set X) (t_mem : t ∈ 𝒜) (hμst : μ.real (s ∆ t) < ε),
    ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

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

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 ∈ 𝒜, μ.real (s ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
hμst : μ.real (s ∆ t) < ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
⟨t, t_mem, (lt_ofReal_iff_toReal_lt (measure_ne_top _ _)).2 hμst⟩

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, ENNReal.lt_ofReal_iff_toReal_lt, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
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 ∈ 𝒜, μ.real (s ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
hμst : μ.real (s ∆ t) < ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
exact ⟨t, t_mem, (lt_ofReal_iff_toReal_lt (measure_ne_top _ _)).2 hμst⟩
-- 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 := 𝒜))
n : ℕ
⊢ T n ∈ 𝒜

Tactic:
simpa using h𝒜.biUnion_mem {k | k ≤ n}.toFinset (fun k _ ↦ S.set_mem k)

Premises used: setOf, MeasureTheory.IsSetAlgebra.biUnion_mem, LE.le, Set.toFinset, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem
-- 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 := 𝒜))
⊢ ∀ (n : ℕ), T n ∈ 𝒜

Tactic:
have T_mem (n) : T n ∈ 𝒜 := by
      simpa using h𝒜.biUnion_mem {k | k ≤ n}.toFinset (fun k _ ↦ S.set_mem k)
-- 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 ∈ 𝒜
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa using measure_biUnion_lt_top {k | k ≤ n}.toFinset.finite_toSet
        (fun k _ ↦ S.finite k)

Premises used: MeasureTheory.measure_biUnion_lt_top, setOf, LE.le, Set.toFinset, MeasureTheory.Measure.FiniteSpanningSetsIn.finite, Finset.finite_toSet
-- 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 ∈ 𝒜
⊢ ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have T_finite (n) : μ (T n) < ∞ := by
      simpa using measure_biUnion_lt_top {k | k ≤ n}.toFinset.finite_toSet
        (fun k _ ↦ S.finite k)
-- 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∞)
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ

Tactic:
have T_spanning : ⋃ n, T n = univ := S.spanning ▸ iUnion_accumulate
-- 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
⊢ Monotone.{0, u_1} (β := Set X) fun (n : ℕ) ↦ T n ∩ s

Tactic:
have mono : Monotone (fun n ↦ (T n) ∩ s) := fun m n hmn ↦ inter_subset_inter_left s
        (biUnion_subset_biUnion_left fun k hkm ↦ Nat.le_trans hkm hmn)
-- 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
⊢ 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∞)

Tactic:
have := tendsto_measure_iUnion_atTop (μ := μ) mono
-- 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∞)
rw :
  ∀
    (this :
      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))))),
    ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
hf : ∀ (i : ℕ), Ne (α := ℝ≥0∞) (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) i) ∞
hx : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
rw [← tendsto_toReal_iff] at this

Premises used: ENNReal.tendsto_toReal_iff
-- 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
    (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))))
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
⊢ ε / 2 > 0

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 :
  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))))
rcases :
  ∀ (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),
    ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

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

Premises used: Metric.tendsto_atTop, HDiv.hDiv, Iff.mp, OfNat.ofNat
-- 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
    (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
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ (T N) < ∞) := Fact.mk <| T_finite N
-- 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∞))
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∞))
rcases :
  ∀ (t : Set X) (t_mem : t ∈ 𝒜) (ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)),
    ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases (Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite
        (μ.restrict (T N)) h𝒜 hgen).approx s ms
        (ne_of_lt (lt_of_le_of_lt (μ.restrict_apply_le _ s) hμs.lt_top))
        (ε / 2) (by linarith [ε_pos])
        with ⟨t, t_mem, ht⟩

Premises used: MeasureTheory.Measure.MeasureDense.approx, lt_of_le_of_lt, MeasureTheory.Measure.restrict, HDiv.hDiv, MeasureTheory.Measure.restrict_apply_le, MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite, Ne.lt_top, OfNat.ofNat, ne_of_lt
-- 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)
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
⟨t ∩ T N, h𝒜.inter_mem t_mem (T_mem N), ?_⟩

Premises used: Inter.inter, And.intro, Exists.intro, MeasureTheory.IsSetAlgebra.inter_mem
-- 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)
refine : (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ T N)) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine ⟨t ∩ T N, h𝒜.inter_mem t_mem (T_mem N), ?_⟩
-- 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 :
  (μ : (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∞)
⊢ (μ : (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∞)

Tactic:
rw [← symmDiff_of_le (inter_subset_left ..), symmDiff_comm _ s,
                inter_symmDiff_distrib_right]

Premises used: symmDiff_comm, Set.inter_subset_left, Set.inter_symmDiff_distrib_right, symmDiff_of_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)
⊢ (μ : (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:
measure_symmDiff_le _ _ _

Premises used: MeasureTheory.measure_symmDiff_le