awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ε / 2 > 0
have linarith₂ : ε / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ε / 2 > 0
have linarith₃ : ε / 2 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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))))
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have 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 ε
Tactic: rcases Metric.tendsto_atTop.1 this (ε / 2) (by linarith [ε_pos]) with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
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
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have this₁ : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (T N) : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have : Fact (μ (T N) < ∞) := Fact.mk <| T_finite N
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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∞))
⊢ 0 < ε / 2
have linarith : ε / 2 ≤ 0 → 2 / 2 = 1
Tactic: linarith [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ 0 < ε / 2
have linarith₁ : ε / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ 0 < ε / 2
have linarith₂ : ε / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ 0 < ε / 2
have linarith₃ : ε / 2 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have 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 ε
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
have refine : (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ T N)) < ENNReal.ofReal ε
Tactic: refine ⟨t ∩ T N, h𝒜.inter_mem t_mem (T_mem N), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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∞)
have 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∞)
Tactic: rw [← symmDiff_of_le (inter_subset_left ..), symmDiff_comm _ s,
                inter_symmDiff_distrib_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ 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)
have ac : (μ : (a : Set X) → ℝ≥0∞) (s \ (s ∩ T N)) < ENNReal.ofReal (ε / 2)
Tactic: apply ENNReal.add_lt_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ 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)
have bd : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t ∩ T N) < ENNReal.ofReal (ε / 2)
Tactic: apply ENNReal.add_lt_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 \ (s ∩ T N)) < ENNReal.ofReal (ε / 2)
have ac : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N)) < ε / 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) s) - ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N)) < ε / 2
have ac : dist (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 ..)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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∞) s)) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N))) < ε / 2
have ac : dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (univ ∩ s))) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N))) <
  ε / 2
Tactic: nth_rw 1 [← univ_inter s]