awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
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 < ε
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
have this : Filter.Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ ((μ : (a : Set X) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)) Filter.atTop
  (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
Tactic: have := tendsto_measure_iUnion_accumulate (μ := μ) (f := f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
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 (β := ℝ≥0∞) (fun (i : ℕ) ↦ ((μ : (a : Set X) → ℝ≥0∞) (accumulate f i) : ℝ≥0∞)) Filter.atTop
    (nhds ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
have 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))))
Tactic: rw [← tendsto_toReal_iff (fun _ ↦ measure_ne_top _ _) (measure_ne_top _ _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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))))
⊢ ε / 2 > 0
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)
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))))
linarith : ε / 2 ≤ 0 → 2 / 2 = 1
⊢ ε / 2 > 0
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)
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))))
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)
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))))
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)
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))))
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
have iUnion : ∀ (N : ℕ)
  (hN :
    ∀ n ≥ N,
      dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (accumulate f n)))
          (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ℕ), f i))) <
        ε / 2),
  ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
Tactic: rcases Metric.tendsto_atTop.1 this (ε / 2) (by linarith [ε_pos]) with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
n : ℕ
⊢ 0 < 2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1
have linarith : 2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ≤ 0 →
  HMul.hMul (α := ℝ) 2 (-1) + 2 * HSub.hSub (α := ℝ) 0 (↑N : ℝ) + (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
n : ℕ
linarith :
  2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ≤ 0 →
    HMul.hMul (α := ℝ) 2 (-1) + 2 * HSub.hSub (α := ℝ) 0 (↑N : ℝ) + (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 - 0) = 0
⊢ 0 < 2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1
have linarith₁ : 2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
have iUnion : ∀ (g : (n : ℕ) → Set X) (g_mem : ∀ (n : ℕ), g n ∈ 𝒜)
  (hg : ∀ (n : ℕ), μ.real (f n ∆ g n) < ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)),
  ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
Tactic: choose g g_mem hg using fun n ↦ (hf n).2 (ε / (2 * (N + 1))) (div_pos ε_pos (by linarith))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
have iUnion : μ.real ((⋃ (i : ℕ), f i) ∆ ⋃ n ∈ Finset.range (N + 1), g n) < ε
Tactic: refine ⟨⋃ n ∈ Finset.range (N + 1), g n, h𝒜.biUnion_mem _ (fun i _ ↦ g_mem i), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ ENNReal.toReal
      ((μ : (a : Set X) → ℝ≥0∞)
        (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
          (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
    ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n))
have rw : ENNReal.toReal
    ((μ : (a : Set X) → ℝ≥0∞)
      (((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) ∪
        (⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) ≤
  (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n) : ℝ≥0∞)).toReal
Tactic: rw [← toReal_add (measure_ne_top _ _) (measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε
have rw : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
    ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
  ε / 2 + ε / 2
Tactic: rw [← 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)
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)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2 + ε / 2
have h₁ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2
Tactic: apply _root_.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)
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)
h₁ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) +
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2 + ε / 2
have h₂ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) < ε / 2
Tactic: apply _root_.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)
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)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2
have h₁ : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)) -
    ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n)) <
  ε / 2
Tactic: rw [measure_diff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
h₁ :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)) -
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n)) <
    ε / 2
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2
have h₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
  ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n) : ℝ≥0∞)
Tactic: rw [measure_diff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
h₁ :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)) -
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n)) <
    ε / 2
h₂ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n) : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2
have h₃ : Subset.{u_1} (α := Set X) (⋃ n ∈ Finset.range (N + 1), f n) (⋃ (n : ℕ), f n)
Tactic: rw [measure_diff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
h₁ :
  ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)) -
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n)) <
    ε / 2
h₂ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n) : ℝ≥0∞)
h₃ : Subset.{u_1} (α := Set X) (⋃ n ∈ Finset.range (N + 1), f n) (⋃ (n : ℕ), f n)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ (n : ℕ), f n) \ ⋃ n ∈ Finset.range (N + 1), f n)) < ε / 2
have h₄ : NullMeasurableSet (⋃ n ∈ Finset.range (N + 1), f n) μ
Tactic: rw [measure_diff (h_fin := measure_ne_top _ _),
                    toReal_sub_of_le (ha := measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)) -
      ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n)) <
    ε / 2
have h₁ : dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
    (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f 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)
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)
⊢ dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
      (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n))) <
    ε / 2
have h₁ : dist (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), f n)))
    (ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), ⋃ (_ : n ≤ N), f n))) <
  ε / 2
Tactic: simp only [Finset.mem_range, Nat.lt_add_one_iff]