awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
⊢ MeasurableSpace.generateFrom (countableGeneratingSet X) = m

Tactic:
have hgen := generateFrom_countableGeneratingSet (α := X)
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
⊢ 𝒜.Countable

Tactic:
have count_𝒜 : 𝒜.Countable :=
      countable_union.2 ⟨h, countable_iff_exists_subset_range.2
        ⟨μ.toFiniteSpanningSetsIn.set, fun _ hx ↦ hx⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
⟨generateSetAlgebra 𝒜, countable_generateSetAlgebra count_𝒜,
      Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite isSetAlgebra_generateSetAlgebra
      { set := μ.toFiniteSpanningSetsIn.set
        set_mem := fun n ↦ self_subset_generateSetAlgebra (𝒜 := 𝒜) <| Or.inr ⟨n, rfl⟩
        finite := μ.toFiniteSpanningSetsIn.finite
        spanning := μ.toFiniteSpanningSetsIn.spanning }
      (le_antisymm ?_ (generateFrom_le (fun s hs ↦ ?_)))⟩

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.set, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, MeasureTheory.Measure.FiniteSpanningSetsIn.spanning, MeasureTheory.countable_generateSetAlgebra, MeasureTheory.Measure.FiniteSpanningSetsIn.finite, MeasureTheory.self_subset_generateSetAlgebra, MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite, le_antisymm, MeasureTheory.isSetAlgebra_generateSetAlgebra, And.intro, Exists.intro, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.generateSetAlgebra, Or.inr, rfl, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
refine_1 : m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)
refine_2 : ∀ (s : Set X) (hs : s ∈ generateSetAlgebra 𝒜), MeasurableSet s
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
refine ⟨generateSetAlgebra 𝒜, countable_generateSetAlgebra count_𝒜,
      Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite isSetAlgebra_generateSetAlgebra
      { set := μ.toFiniteSpanningSetsIn.set
        set_mem := fun n ↦ self_subset_generateSetAlgebra (𝒜 := 𝒜) <| Or.inr ⟨n, rfl⟩
        finite := μ.toFiniteSpanningSetsIn.finite
        spanning := μ.toFiniteSpanningSetsIn.spanning }
      (le_antisymm ?_ (generateFrom_le (fun s hs ↦ ?_)))⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
refine_1 : MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)
⊢ m ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Tactic:
rw [← hgen]
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
⊢ MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Tactic:
generateFrom_mono <| le_trans self_subset_generateSetAlgebra <|
        generateSetAlgebra_mono <| subset_union_left ..

Premises used: MeasurableSpace.generateFrom_mono, Set.subset_union_left, MeasureTheory.self_subset_generateSetAlgebra, MeasureTheory.generateSetAlgebra_mono, le_trans
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
⊢ MeasurableSpace.generateFrom (countableGeneratingSet X) ≤ MeasurableSpace.generateFrom (generateSetAlgebra 𝒜)

Tactic:
exact generateFrom_mono <| le_trans self_subset_generateSetAlgebra <|
        generateSetAlgebra_mono <| subset_union_left ..

Premises used: MeasurableSpace.generateFrom_mono, Set.subset_union_left, MeasureTheory.self_subset_generateSetAlgebra, MeasureTheory.generateSetAlgebra_mono, le_trans
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
t_mem : t ∈ 𝒜
refine_2 : ∀ (t_mem : t ∈ countableGeneratingSet X), MeasurableSet t
refine_2₁ : ∀ (n : ℕ), MeasurableSet (μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n)
⊢ MeasurableSet t

Tactic:
rcases t_mem with t_mem | ⟨n, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
t_mem : t ∈ countableGeneratingSet X
⊢ MeasurableSet t

Tactic:
hgen ▸ measurableSet_generateFrom t_mem

Premises used: MeasurableSpace.measurableSet_generateFrom, Eq.rec
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
t_mem : t ∈ countableGeneratingSet X
⊢ MeasurableSet t

Tactic:
exact hgen ▸ measurableSet_generateFrom t_mem
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s : Set X
n : ℕ
⊢ MeasurableSet (μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n)

Tactic:
μ.toFiniteSpanningSetsIn.set_mem n

Premises used: MeasurableSet, Set.Mem, setOf, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s : Set X
n : ℕ
⊢ MeasurableSet (μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n)

Tactic:
exact μ.toFiniteSpanningSetsIn.set_mem n

Premises used: MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s : Set X
⊢ MeasurableSet.{u_1} (α := X) ∅

Tactic:
MeasurableSet.empty

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s : Set X
⊢ MeasurableSet.{u_1} (α := X) ∅

Tactic:
exact MeasurableSet.empty

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
hs : generateSetAlgebra 𝒜 t
t_mem : MeasurableSet t
⊢ MeasurableSet tᶜ

Tactic:
MeasurableSet.compl t_mem

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t : Set X
hs : generateSetAlgebra 𝒜 t
t_mem : MeasurableSet t
⊢ MeasurableSet tᶜ

Tactic:
exact MeasurableSet.compl t_mem

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t u : Set X
hs : generateSetAlgebra 𝒜 t
ht : generateSetAlgebra 𝒜 u
t_mem : MeasurableSet t
u_mem : MeasurableSet u
⊢ MeasurableSet (t ∪ u)

Tactic:
MeasurableSet.union t_mem u_mem

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s t u : Set X
hs : generateSetAlgebra 𝒜 t
ht : generateSetAlgebra 𝒜 u
t_mem : MeasurableSet t
u_mem : MeasurableSet u
⊢ MeasurableSet (t ∪ u)

Tactic:
exact MeasurableSet.union t_mem u_mem

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
inst : CountablyGenerated X
inst_1 : SigmaFinite μ
h : (countableGeneratingSet X).Countable
hgen : MeasurableSpace.generateFrom (countableGeneratingSet X) = m
𝒜 : Set (Set X) :=
  countableGeneratingSet X ∪
    {x : Set X | ∃ (n : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n = x}
count_𝒜 : 𝒜.Countable
s : Set X
hs : s ∈ generateSetAlgebra 𝒜
refine_2 : ∀ (t : Set X) (t_mem : t ∈ 𝒜), MeasurableSet t
refine_2₁ : MeasurableSet.{u_1} (α := X) ∅
refine_2₂ : ∀ (t : Set X), generateSetAlgebra 𝒜 t → ∀ (t_mem : MeasurableSet t), MeasurableSet tᶜ
refine_2₃ :
  ∀ (t u : Set X),
    generateSetAlgebra 𝒜 t →
      generateSetAlgebra 𝒜 u → ∀ (t_mem : MeasurableSet t) (u_mem : MeasurableSet u), MeasurableSet (t ∪ u)
⊢ MeasurableSet s

Tactic:
induction hs with
      | base t t_mem =>
        rcases t_mem with t_mem | ⟨n, rfl⟩
        · exact hgen ▸ measurableSet_generateFrom t_mem
        · exact μ.toFiniteSpanningSetsIn.set_mem n
      | empty => exact MeasurableSet.empty
      | compl t _ t_mem => exact MeasurableSet.compl t_mem
      | union t u _ _ t_mem u_mem => exact MeasurableSet.union t_mem u_mem

Premises used: MeasurableSet.empty, Compl.compl, rfl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
⊢ IsSeparable (μ.restrict μ.sigmaFiniteSet)

Tactic:
have := isSeparable_of_sigmaFinite (μ.restrict μ.sigmaFiniteSet)
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
rcases :
  ∀ (𝒜 : Set (Set X)) (count_𝒜 : 𝒜.Countable) (h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜),
    ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
rcases exists_countable_measureDense (μ.restrict μ.sigmaFiniteSet) with ⟨𝒜, count_𝒜, h𝒜⟩

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.sigmaFiniteSet, MeasureTheory.exists_countable_measureDense
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
⟨ℬ, count_𝒜.image (fun s ↦ s ∩ μ.sigmaFiniteSet), ?_, ?_⟩

Premises used: MeasureTheory.Measure.sigmaFiniteSet, Set.Countable.image, Inter.inter, MeasureTheory.Measure.MeasureDense.mk, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
refine_1 : ∀ s ∈ ℬ, MeasurableSet s
refine_2 :
  ∀ (s : Set X),
    MeasurableSet s →
      Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∀ (ε : ℝ), 0 < ε → ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜

Tactic:
refine ⟨ℬ, count_𝒜.image (fun s ↦ s ∩ μ.sigmaFiniteSet), ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
s_mem : s ∈ 𝒜
⊢ MeasurableSet (s ∩ μ.sigmaFiniteSet)

Tactic:
(h𝒜.measurable s s_mem).inter measurableSet_sigmaFiniteSet

Premises used: MeasureTheory.measurableSet_sigmaFiniteSet, MeasureTheory.Measure.MeasureDense.measurable, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
s_mem : s ∈ 𝒜
⊢ MeasurableSet (s ∩ μ.sigmaFiniteSet)

Tactic:
exact (h𝒜.measurable s s_mem).inter measurableSet_sigmaFiniteSet

Premises used: MeasureTheory.measurableSet_sigmaFiniteSet, MeasureTheory.Measure.MeasureDense.measurable, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
refine_2 :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
refine_2₁ :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases restrict_compl_sigmaFiniteSet_eq_zero_or_top μ s with hs | hs

Premises used: MeasureTheory.restrict_compl_sigmaFiniteSet_eq_zero_or_top
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have : (μ.restrict μ.sigmaFiniteSet) s ≠ ∞ :=
          ne_top_of_le_ne_top hμs <| μ.restrict_le_self _
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this_1 : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  ∀ (t : Set X) (t_mem : t ∈ 𝒜) (ht : (μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε),
    ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases h𝒜.approx s ms this ε ε_pos with ⟨t, t_mem, ht⟩

Premises used: MeasureTheory.Measure.MeasureDense.approx
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this_1 : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
⟨t ∩ μ.sigmaFiniteSet, ⟨t, t_mem, rfl⟩, ?_⟩

Premises used: MeasureTheory.Measure.sigmaFiniteSet, Inter.inter, And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.Measure.SeparableMeasure
Goal:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜_1 : Set (Set X)
inst_1 : CountablyGenerated X
inst_2 : SFinite μ
this_1 : IsSeparable (μ.restrict μ.sigmaFiniteSet)
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜
ℬ : Set (Set X) := {x : Set X | ∃ s ∈ 𝒜, s ∩ μ.sigmaFiniteSet = x}
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
refine_2 : (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine ⟨t ∩ μ.sigmaFiniteSet, ⟨t, t_mem, rfl⟩, ?_⟩