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_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∞) (univ ∩ s))) (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∩ T N))) <
    ε / 2
have ac : dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (T N ∩ s)))
    (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), T i ∩ s))) <
  ε / 2
Tactic: rw [inter_comm s, dist_comm, ← T_spanning, iUnion_inter _ T]
-- 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)
⊢ 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∞))
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
⊢ 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∞))
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
⊢ 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∞))
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
⊢ 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 : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N) : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) = ENNReal.ofReal ε
have rw : ENNReal.ofReal (ε / 2 + ε / 2) = ENNReal.ofReal ε
Tactic: rw [← ofReal_add (by linarith [ε_pos]) (by linarith [ε_pos]), add_halves]
-- 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)
rw : ENNReal.ofReal (ε / 2 + ε / 2) = ENNReal.ofReal ε
⊢ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) = ENNReal.ofReal ε
have rw₁ : ENNReal.ofReal ε = ENNReal.ofReal ε
Tactic: rw [← ofReal_add (by linarith [ε_pos]) (by linarith [ε_pos]), add_halves]
-- 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)) < ENNReal.ofReal ε
have μ₁ : (μ : (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: 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]
-- 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∞)
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ T N)) < ENNReal.ofReal ε
have μ₂ : 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: 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]
-- 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∞)
μ₂ :
  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)
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ T N)) < ENNReal.ofReal ε
have μ₃ : ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) = 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have h : (countableGeneratingSet X).Countable
Tactic: have h := countable_countableGeneratingSet (α := X)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
Tactic: have hgen := generateFrom_countableGeneratingSet (α := X)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have count_𝒜 : 𝒜.Countable
Tactic: have count_𝒜 : 𝒜.Countable :=
      countable_union.2 ⟨h, countable_iff_exists_subset_range.2
        ⟨μ.toFiniteSpanningSetsIn.set, fun _ hx ↦ hx⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have refine_1 : m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)
Tactic: refine ⟨generateSetAlgebra 𝒜, countable_generateSetAlgebra count_𝒜,
      Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite isSetAlgebra_generateSetAlgebra
      { set := μ.toFiniteSpanningSetsIn.set
        set_mem := fun n ↦ self_subset_generateSetAlgebra (𝒜 := 𝒜) <| Or.inr ⟨n, rfl⟩
        finite := μ.toFiniteSpanningSetsIn.finite
        spanning := μ.toFiniteSpanningSetsIn.spanning }
      (le_antisymm ?_ (generateFrom_le (fun s hs ↦ ?_)))⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
refine_1 : m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have refine_2 : ∀ (s : Set X) (hs : s ∈ generateSetAlgebra 𝒜), MeasurableSet s
Tactic: refine ⟨generateSetAlgebra 𝒜, countable_generateSetAlgebra count_𝒜,
      Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite isSetAlgebra_generateSetAlgebra
      { set := μ.toFiniteSpanningSetsIn.set
        set_mem := fun n ↦ self_subset_generateSetAlgebra (𝒜 := 𝒜) <| Or.inr ⟨n, rfl⟩
        finite := μ.toFiniteSpanningSetsIn.finite
        spanning := μ.toFiniteSpanningSetsIn.spanning }
      (le_antisymm ?_ (generateFrom_le (fun s hs ↦ ?_)))⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
⊢ m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)
have refine_1 : MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)
Tactic: rw [← hgen]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
t_mem : t ∈ 𝒜
⊢ MeasurableSet t
have refine_2 : ∀ (t_mem : t ∈ countableGeneratingSet X), MeasurableSet t
Tactic: rcases t_mem with t_mem | ⟨n, rfl⟩
Cleared hypotheses: t_mem