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)
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)
⊢ μ.real (⋃ n ∈ Finset.range (N + 1), f n ∆ g n) ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n)
have simp_rw : ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (⋃ n ∈ Finset.range (N + 1), f n ∆ g n)) ≤
  ENNReal.toReal (∑ a ∈ Finset.range (N + 1), (μ : (a : Set X) → ℝ≥0∞) (f a ∆ g a))
Tactic: simp_rw [measureReal_def, ← toReal_sum (fun _ _ ↦ 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)
⊢ ∑ n ∈ Finset.range (N + 1), ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) ≤ ε / 2
have simp : HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * (ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) ≤ ε / 2
Tactic: simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul,
                            Nat.cast_add, Nat.cast_one]
-- 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)
⊢ HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * (ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) ≤ ε / 2
have rw : ε / 2 * (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 * (1 / HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) ≤ ε / 2
Tactic: rw [div_mul_eq_div_mul_one_div, ← mul_assoc, mul_comm ((N : ℝ) + 1),
                            mul_assoc]
-- 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)
⊢ 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)
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)
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)
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)
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)
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)
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)
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 ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2
have n : μ.real (⋃ n ∈ Finset.range (N + 1), f n ∆ g n) ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n)
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 _
-- 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)
n : μ.real (⋃ n ∈ Finset.range (N + 1), f n ∆ g n) ≤ ∑ n ∈ Finset.range (N + 1), μ.real (f n ∆ g n)
⊢ ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) ((⋃ n ∈ Finset.range (N + 1), f n) ∆ ⋃ n ∈ Finset.range (N + 1), g n)) <
    ε / 2
have n₁ : ∑ n ∈ Finset.range (N + 1), ε / (2 * HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) ≤ ε / 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 _
-- 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
ms : MeasurableSet s
this : MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (s ∆ t) < ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have rcases : ∀ (t : Set X) (t_mem : t ∈ 𝒜) (hμst : μ.real (s ∆ t) < ε), ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
Tactic: rcases this.2 ε ε_pos with ⟨t, t_mem, hμst⟩
-- 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 ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have T_mem : ∀ (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)
-- 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 ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have T_finite : ∀ (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)
-- 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 ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have T_spanning : Eq.{u_1 + 1} (α := Set X) (⋃ (n : ℕ), T n) univ
Tactic: have T_spanning : ⋃ n, T n = univ := S.spanning ▸ iUnion_accumulate
-- 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
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have mono : 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)
-- 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
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have 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∞)
Tactic: have := tendsto_measure_iUnion_atTop (μ := μ) mono
-- 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 (α := ℕ) (β := ℝ≥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∞)
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have 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 ε
Tactic: rw [← tendsto_toReal_iff] 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)
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 ε
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have hf : ∀ (i : ℕ), Ne (α := ℝ≥0∞) (Function.comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) (fun (n : ℕ) ↦ T n ∩ s) i) ∞
Tactic: rw [← tendsto_toReal_iff] at this
-- 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 (α := ℕ) (β := ℝ≥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) ∞
⊢ ∃ t ∈ 𝒜, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have hx : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (n : ℕ), T n ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← tendsto_toReal_iff] at this
-- 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))))
⊢ ε / 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)
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
⊢ ε / 2 > 0
have linarith₁ : ε / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [ε_pos]