awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
rw :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ) atTop (𝓝 0)

Tactic:
rw [← hD]
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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 j : ℕ
hij : i ≤ j
⊢ (accumulate f j)ᶜ ≤ (accumulate f i)ᶜ

Tactic:
simpa using monotone_accumulate hij

Premises used: Set.monotone_accumulate
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (accumulate f 0)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
apply : ∀ (i : ℕ), NullMeasurableSet (accumulate f i)ᶜ μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ)) : Filter ℝ≥0∞)

Tactic:
apply tendsto_measure_iInter_atTop (fun i ↦ ?_)
          (fun i j hij ↦ by simpa using monotone_accumulate hij) ⟨0, by simp⟩

Premises used: MeasureTheory.tendsto_measure_iInter_atTop, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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 : ℕ
h₁ : MeasurableSet (accumulate f i)ᶜ
⊢ NullMeasurableSet (accumulate f i)ᶜ μ

Tactic:
apply MeasurableSet.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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 : ℕ
h₁ : MeasurableSet (accumulate f i)ᶜ
⊢ MeasurableSet (accumulate f i)ᶜ

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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)ᶜ

Tactic:
(measurableSet_generateFrom (fC i)).compl

Premises used: MeasurableSpace.measurableSet_generateFrom, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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)ᶜ

Tactic:
exact (measurableSet_generateFrom (fC i)).compl

Premises used: MeasurableSpace.measurableSet_generateFrom, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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)

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
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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)
⊢ ∃ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ < ε / 2

Tactic:
((tendsto_order.1 this).2 _ (ENNReal.half_pos εpos.ne')).exists

Premises used: tendsto_order, LT.lt.ne', Filter.Eventually.exists, And.right, ENNReal.half_pos, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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)
obtain :
  ∀ (n : ℕ) (hn : (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ < ε / 2), ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 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

Premises used: tendsto_order, LT.lt.ne', Filter.Eventually.exists, And.right, ENNReal.half_pos, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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)
n : ℕ
hn : (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ < ε / 2
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2

Tactic:
⟨accumulate f n, fC n, hn⟩

Premises used: Set.accumulate, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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)
n : ℕ
hn : (μ : (a : Set α) → ℝ≥0∞) (accumulate f n)ᶜ < ε / 2
⊢ ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2

Tactic:
exact ⟨accumulate f n, fC n, hn⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
obtain :
  ∀ (t' : Set α) (t'C : t' ∈ C) (ht' : (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2),
    ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε
⊢ ∃ 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⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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ᶜ) < ε

Tactic:
⟨t' \ t, hC.diff_mem t'C tC, ?_⟩

Premises used: SDiff.sdiff, MeasureTheory.IsSetRing.diff_mem, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
refine : (μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε

Tactic:
refine ⟨t' \ t, hC.diff_mem t'C tC, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
h₁ : (t' \ t) ∆ sᶜ ⊆ t ∆ s ∪ t'ᶜ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s ∪ t'ᶜ) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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' \ t) ∆ sᶜ ⊆ t ∆ s ∪ t'ᶜ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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 ∆ s ∪ t'ᶜ) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t'ᶜ : ℝ≥0∞)

Tactic:
measure_union_le _ _

Premises used: MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t'ᶜ : ℝ≥0∞) <
    ε / 2 + ε / 2

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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
⊢ ε / 2 + ε / 2 = ε

Tactic:
ENNReal.add_halves ε

Premises used: ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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∞)
calc₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t'ᶜ : ℝ≥0∞) <
    ε / 2 + ε / 2
⊢ (μ : (a : Set α) → ℝ≥0∞) ((t' \ t) ∆ sᶜ) < ε

Tactic:
calc μ ((t' \ t) ∆ sᶜ)
      _ ≤ μ (t ∆ s ∪ t'ᶜ) := by gcongr; grind
      _ ≤ μ (t ∆ s) + μ (t'ᶜ) := measure_union_le _ _
      _ < ε / 2 + ε / 2 := by gcongr
      _ = ε := ENNReal.add_halves ε

Premises used: Compl.compl, SDiff.sdiff, ENNReal.add_halves, Union.union, DFunLike.coe, symmDiff, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
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 < ε
rcases :
  ∀ (δ : ℕ → ℝ≥0∞) (δpos : ∀ (i : ℕ), 0 < δ i) (hδ : ∑' (i : ℕ), δ i < ε / 2),
    ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ⋃ (i : ℕ), f i) < ε
⊢ ∃ 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δ⟩

Premises used: ENNReal.exists_pos_sum_of_countable', LT.lt.ne', Nat, ENNReal.half_pos