awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
⊢ edist s t = ENNReal.ofReal ((fun (s t : MeasuredSets μ) ↦ μ.real ((↑s : Set α) ∆ (↑t : Set α))) s t)

Tactic:
simp [Measure.real, MeasuredSets.edist_def]

Premises used: MeasureTheory.Measure.real, MeasureTheory.MeasuredSets.edist_def
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
⊢ dist s t = μ.real ((↑s : Set α) ∆ (↑t : Set α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
grw :
  μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)).toReal
h₂ : Ne (α := ℝ≥0∞) (edist s t) ∞
⊢ μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤ dist s t

Tactic:
grw [dist_edist, ← sub_le_edist]

Premises used: MeasureTheory.MeasuredSets.sub_le_edist, dist_edist
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
⊢ μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)).toReal

Tactic:
ENNReal.le_toReal_sub (measure_ne_top _ _)

Premises used: ENNReal.le_toReal_sub, MeasureTheory.Measure.real, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
⊢ Ne (α := ℝ≥0∞) (edist s t) ∞

Tactic:
edist_ne_top _ _

Premises used: edist_ne_top
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
⊢ μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)).toReal

Tactic:
exacts [ENNReal.le_toReal_sub (measure_ne_top _ _), edist_ne_top _ _]

Premises used: ENNReal.le_toReal_sub, MeasureTheory.measure_ne_top, edist_ne_top
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ LipschitzWith (β := ℝ) 1 fun (s : MeasuredSets μ) ↦ μ.real (↑s : Set α)

Tactic:
.of_le_add fun s t ↦ sub_le_iff_le_add'.mp <| real_sub_real_le_dist s t

Premises used: MeasureTheory.MeasuredSets.real_sub_real_le_dist, LipschitzWith.of_le_add, sub_le_iff_le_add', 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 : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
apply : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ∅) < ε
apply₁ :
  ∀ (t : Set α) (ht : t ∈ C),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      t ⋯
apply₂ :
  ∀ (t : Set α) (htm : MeasurableSet t),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
        t htm →
      (fun (s : Set α) (hs : MeasurableSet s) ↦
          ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
        tᶜ ⋯
apply₃ :
  ∀ (f : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f) →
      ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)),
        (∀ (i : ℕ),
            (fun (s : Set α) (hs : MeasurableSet s) ↦
                ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
              (f i) ⋯) →
          (fun (s : Set α) (hs : MeasurableSet s) ↦
              ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
            (⋃ (i : ℕ), f i) ⋯
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε

Tactic:
apply MeasurableSpace.induction_on_inter (C := fun s hs ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    ∃ t ∈ C, μ (t ∆ s) < ε) h hC.isSetSemiring.isPiSystem ?_ ?_ ?_ ?_ s hs ε hε

Premises used: MeasureTheory.IsSetSemiring.isPiSystem, MeasureTheory.IsSetRing.isSetSemiring, MeasurableSpace.induction_on_inter
-- 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
ε : ℝ≥0∞
εpos : 0 < ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (∅ ∆ ∅) < ε

Tactic:
simp [εpos]
-- 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
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ∅) < ε

Tactic:
exact ⟨∅, hC.empty_mem, by simp [εpos]⟩
-- 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 : s ∈ C
ε : ℝ≥0∞
εpos : 0 < ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∆ s) < ε

Tactic:
simp [εpos]
-- 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 : s ∈ C
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε

Tactic:
exact ⟨s, hs, by simp [εpos]⟩
-- 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 ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2

Tactic:
h's _ (ENNReal.half_pos εpos.ne')

Premises used: LT.lt.ne', ENNReal.half_pos
-- 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 < ε
obtain :
  ∀ (t : Set α) (tC : t ∈ C) (ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2),
    ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε

Tactic:
obtain ⟨t, tC, ht⟩ : ∃ t ∈ C, μ (t ∆ s) < ε / 2 := h's _ (ENNReal.half_pos εpos.ne')

Premises used: LT.lt.ne', ENNReal.half_pos
-- 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
rcases :
  ∀ (D : Set (Set α)) (D_count : D.Countable) (DC : D ⊆ C)
    (hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ (D : Set (Set α)),
      D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ D.Nonempty
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ D.Nonempty

Tactic:
rcases h'C with ⟨D, D_count, DC, hD⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
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∞)
⊢ Set.Countable (α := Set α) {∅}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
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∞)
refine : D ∪ {∅} ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {∅}))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (D ∪ {∅}).Nonempty
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ D.Nonempty

Tactic:
refine ⟨D ∪ {∅}, D_count.union (by simp), ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
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∞)
simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {∅}))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (D ∪ {∅}).Nonempty
⊢ D ∪ {∅} ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {∅}))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (D ∪ {∅}).Nonempty

Tactic:
simp only [union_subset_iff, DC, singleton_subset_iff, true_and, and_true, hC.empty_mem]

Premises used: Set.singleton_subset_iff, and_true, Set.union_subset_iff, MeasureTheory.IsSetRing.empty_mem, true_and
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {∅}))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (D ∪ {∅}).Nonempty

Tactic:
simp only [union_singleton, sUnion_insert, empty_union, insert_nonempty, and_true, hD]

Premises used: Set.insert_nonempty, and_true, Set.sUnion_insert, Set.empty_union, Set.union_singleton
-- 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 :
  ∀ (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
⊢ ∃ 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]

Premises used: Set
-- 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 α), D = range f

Tactic:
Set.Countable.exists_eq_range D_count Dne

Premises used: Set.Countable.exists_eq_range
-- 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
obtain : ∀ (f : ℕ → Set α) (hf : D = range f), ∃ t' ∈ C, (μ : (a : Set α) → ℝ≥0∞) t'ᶜ < ε / 2
⊢ ∃ 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

Premises used: Set.Countable.exists_eq_range
-- 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
n_1 n : ℕ
⊢ f n ∈ D

Tactic:
simp [hf]
-- 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
⊢ ∀ (n : ℕ), accumulate f n ∈ C

Tactic:
have fC n : Set.accumulate f n ∈ C := hC.accumulate_mem (fun n ↦ DC (by simp [hf])) n
-- 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
⊢ ⋃₀ D = ⋃ (n : ℕ), accumulate f n

Tactic:
simp [hf, iUnion_accumulate]

Premises used: Set.iUnion_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
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
⊢ ⋃₀ D = ⋃ (n : ℕ), accumulate f n

Tactic:
have : ⋃₀ D = ⋃ n, Set.accumulate f n := by simp [hf, iUnion_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
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
⊢ (⋃₀ D)ᶜ = ⋂ (n : ℕ), (accumulate f n)ᶜ

Tactic:
simp [this, accumulate]

Premises used: Set.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
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
⊢ 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
-- 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 : ⋃₀ D = ⋃ (n : ℕ), accumulate f n
hD₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ D = range f

Tactic:
rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this, accumulate]] at 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
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
hD₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
hf₁ : D = range f
⊢ ∀ (n : ℕ), accumulate f n ∈ C

Tactic:
rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this, accumulate]] at 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
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
hD₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), (accumulate f n)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
hf₁ : D = range f
fC₁ : ∀ (n : ℕ), accumulate f n ∈ C
⊢ ⋃₀ D = ⋃ (n : ℕ), accumulate f n

Tactic:
rw [show (⋃₀ D)ᶜ = ⋂ n, (Set.accumulate f n)ᶜ by simp [this, accumulate]] at hD