awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
have obtain : ∀ (D : Set (Set α)) (D_count : D.Countable) (DC : D ⊆ C)
  (hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)) (Dne : D.Nonempty),
  ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
Tactic: obtain ⟨D, D_count, DC, hD, Dne⟩ :
          ∃ D : Set (Set α), D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0 ∧ D.Nonempty := by
        rcases h'C with ⟨D, D_count, DC, hD⟩
        refine ⟨D ∪ {∅}, D_count.union (by simp), ?_⟩
        simp only [union_subset_iff, DC, singleton_subset_iff, true_and, and_true, hC.empty_mem]
        simp only [union_singleton, sUnion_insert, empty_union, insert_nonempty, and_true, hD]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Dne : D.Nonempty
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
have obtain : ∀ (f : ℕ → Set α) (hf : D = range f), ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
Tactic: obtain ⟨f, hf⟩ : ∃ f : ℕ → Set α, D = Set.range f := Set.Countable.exists_eq_range D_count Dne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Dne : D.Nonempty
f : ℕ → Set α
hf : D = range f
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
have fC : ∀ (n : ℕ), accumulate f n ∈ C
Tactic: have fC n : Set.accumulate f n ∈ C := hC.accumulate_mem (fun n ↦ DC (by simp [hf])) n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Dne : D.Nonempty
f : ℕ → Set α
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ) atTop (𝓝 0)
have this : ⋃₀ D = ⋃ (n : ℕ), accumulate f n
Tactic: have : ⋃₀ D = ⋃ n, Set.accumulate f n := by simp [hf, iUnion_accumulate]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Dne : D.Nonempty
f : ℕ → Set α
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ (n : ℕ), accumulate f n
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ) atTop (𝓝 0)
have hD₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this, accumulate]] at hD
Cleared hypotheses: hD, hf, fC, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
Dne : D.Nonempty
f : ℕ → Set α
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ (n : ℕ), accumulate f n
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ) atTop (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ : ℝ≥0∞)) atTop
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ)) : Filter ℝ≥0∞)
Tactic: rw [← hD]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
Dne : D.Nonempty
f : ℕ → Set α
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ (n : ℕ), accumulate f n
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ)) : Filter ℝ≥0∞)
have apply : ∀ (i : ℕ), NullMeasurableSet (accumulate f i)ᶜ μ
Tactic: apply tendsto_measure_iInter_atTop (fun i ↦ ?_)
          (fun i j hij ↦ by simpa using monotone_accumulate hij) ⟨0, by simp⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
Dne : D.Nonempty
f : ℕ → Set α
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ (n : ℕ), accumulate f n
i : ℕ
⊢ NullMeasurableSet (accumulate f i)ᶜ μ
have h₁ : MeasurableSet (accumulate f i)ᶜ
Tactic: apply MeasurableSet.nullMeasurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
Dne : D.Nonempty
f : ℕ → Set α
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : ⋃₀ D = ⋃ (n : ℕ), accumulate f n
i : ℕ
⊢ MeasurableSet (accumulate f i)ᶜ
have h₁ : MeasurableSet (accumulate f i)ᶜ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Dne : D.Nonempty
f : ℕ → Set α
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
have this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ) atTop (𝓝 0)
Tactic: have : Tendsto (fun n ↦ μ (Set.accumulate f n)ᶜ) atTop (𝓝 0) := by
        have : ⋃₀ D = ⋃ n, Set.accumulate f n := by simp [hf, iUnion_accumulate]
        rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this, accumulate]] at hD
        rw [← hD]
        apply tendsto_measure_iInter_atTop (fun i ↦ ?_)
          (fun i j hij ↦ by simpa using monotone_accumulate hij) ⟨0, by simp⟩
        apply MeasurableSet.nullMeasurableSet
        rw [h]
        exact (measurableSet_generateFrom (fC i)).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Dne : D.Nonempty
f : ℕ → Set α
hf : D = range f
fC : ∀ (n : ℕ), accumulate f n ∈ C
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ) atTop (𝓝 0)
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
have obtain : ∀ (n : ℕ) (hn : (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ < ε / 2), ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
Tactic: obtain ⟨n, hn⟩ : ∃ n, μ (accumulate f n)ᶜ < ε / 2 :=
        ((tendsto_order.1 this).2 _ (ENNReal.half_pos εpos.ne')).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε
have obtain : ∀ (t' : Set α) (t'C : t' ∈ C) (ht' : (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2),
  ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε
Tactic: obtain ⟨t', t'C, ht'⟩ : ∃ t' ∈ C, μ (t'ᶜ) < ε / 2 := by
      obtain ⟨D, D_count, DC, hD, Dne⟩ :
          ∃ D : Set (Set α), D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0 ∧ D.Nonempty := by
        rcases h'C with ⟨D, D_count, DC, hD⟩
        refine ⟨D ∪ {∅}, D_count.union (by simp), ?_⟩
        simp only [union_subset_iff, DC, singleton_subset_iff, true_and, and_true, hC.empty_mem]
        simp only [union_singleton, sUnion_insert, empty_union, insert_nonempty, and_true, hD]
      obtain ⟨f, hf⟩ : ∃ f : ℕ → Set α, D = Set.range f := Set.Countable.exists_eq_range D_count Dne
      have fC n : Set.accumulate f n ∈ C := hC.accumulate_mem (fun n ↦ DC (by simp [hf])) n
      have : Tendsto (fun n ↦ μ (Set.accumulate f n)ᶜ) atTop (𝓝 0) := by
        have : ⋃₀ D = ⋃ n, Set.accumulate f n := by simp [hf, iUnion_accumulate]
        rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this, accumulate]] at hD
        rw [← hD]
        apply tendsto_measure_iInter_atTop (fun i ↦ ?_)
          (fun i j hij ↦ by simpa using monotone_accumulate hij) ⟨0, by simp⟩
        apply MeasurableSet.nullMeasurableSet
        rw [h]
        exact (measurableSet_generateFrom (fC i)).compl
      obtain ⟨n, hn⟩ : ∃ n, μ (accumulate f n)ᶜ < ε / 2 :=
        ((tendsto_order.1 this).2 _ (ENNReal.half_pos εpos.ne')).exists
      exact ⟨accumulate f n, fC n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
t' : Set α
t'C : t' ∈ C
ht' : (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε
have refine : (μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) < ε
Tactic: refine ⟨t' \ t, hC.diff_mem t'C tC, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
t' : Set α
t'C : t' ∈ C
ht' : (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s ∪ t'ᶜ) : ℝ≥0∞)
have h₁ : (t' \ t) ∆ sᶜ ⊆ t ∆ s ∪ t'ᶜ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
t' : Set α
t'C : t' ∈ C
ht' : (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
⊢ (μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) < ε
have calc : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s ∪ t'ᶜ) : ℝ≥0∞)
Tactic: calc μ ((t' \ t) ∆ sᶜ)
      _ ≤ μ (t ∆ s ∪ t'ᶜ) := by gcongr; grind
      _ ≤ μ (t ∆ s) + μ (t'ᶜ) := measure_union_le _ _
      _ < ε / 2 + ε / 2 := by gcongr
      _ = ε := ENNReal.add_halves ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
t' : Set α
t'C : t' ∈ C
ht' : (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
calc :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s ∪ t'ᶜ) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) < ε
have calc₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t'ᶜ : ℝ≥0∞) <
  ε / 2 + ε / 2
Tactic: calc μ ((t' \ t) ∆ sᶜ)
      _ ≤ μ (t ∆ s ∪ t'ᶜ) := by gcongr; grind
      _ ≤ μ (t ∆ s) + μ (t'ᶜ) := measure_union_le _ _
      _ < ε / 2 + ε / 2 := by gcongr
      _ = ε := ENNReal.add_halves ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
have rcases : ∀ (δ : ℕ → ℝ≥0∞) (δpos : ∀ (i : ℕ), 0 < δ i) (hδ : ∑' (i : ℕ), δ i < ε / 2),
  ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
Tactic: rcases ENNReal.exists_pos_sum_of_countable' (ENNReal.half_pos εpos.ne').ne' ℕ with ⟨δ, δpos, hδ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
have A : ∀ (i : ℕ), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ f i) < δ i
Tactic: have A i : ∃ t ∈ C, μ (t ∆ (f i)) < δ i := hf i _ (δpos i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
A : ∀ (i : ℕ), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ f i) < δ i
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
have choose! : ∀ (t : (i : ℕ) → Set α) (tC : ∀ (i : ℕ), t i ∈ C) (ht : ∀ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) < δ i),
  ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
Tactic: choose! t tC ht using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : (i : ℕ) → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) < δ i
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
have this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
Tactic: have : Tendsto (fun n ↦ μ (⋃ i ∈ Ici n, f i)) atTop (𝓝 0) :=
      tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint
        (fun i ↦ (f_meas i).nullMeasurableSet) f_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε_1 : ℝ≥0∞
hε : 0 < ε_1
f : ℕ → Set α
f_disj : Pairwise (Function.onFun Disjoint f)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf :
  ∀ (i : ℕ),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      (f i) ⋯
ε : ℝ≥0∞
εpos : 0 < ε
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε / 2
t : (i : ℕ) → Set α
tC : ∀ (i : ℕ), t i ∈ C
ht : ∀ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t i ∆ f i) < δ i
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i)) atTop (𝓝 0)
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
have obtain : ∀ (n : ℕ) (hn : (μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Ici n, f i) < ε / 2),
  ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
Tactic: obtain ⟨n, hn⟩ : ∃ n, μ (⋃ i ∈ Ici n, f i) < ε / 2 :=
      ((tendsto_order.1 this).2 _ (ENNReal.half_pos εpos.ne')).exists