awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
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
⊢ MeasurableSet t
have refine_2₁ : ∀ (n : ℕ), MeasurableSet (μ.toFiniteSpanningSetsIn.set (C := {s : Set X | MeasurableSet s}) n)
Tactic: rcases t_mem with t_mem | ⟨n, rfl⟩
Cleared hypotheses: t, t_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 𝒜
⊢ MeasurableSet s
have refine_2 : ∀ (t : Set X) (t_mem : t ∈ 𝒜), MeasurableSet t
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ MeasurableSet s
have refine_2₁ : MeasurableSet.{u_1} (α := X) ∅
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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) ∅
⊢ MeasurableSet s
have refine_2₂ : ∀ (t : Set X), generateSetAlgebra 𝒜 t → ∀ (t_mem : MeasurableSet t), MeasurableSet tᶜ
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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ᶜ
⊢ MeasurableSet s
have refine_2₃ : ∀ (t u : Set X),
  generateSetAlgebra 𝒜 t →
    generateSetAlgebra 𝒜 u → ∀ (t_mem : MeasurableSet t) (u_mem : MeasurableSet u), MeasurableSet (t ∪ u)
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
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 μ
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have this : IsSeparable (μ.restrict μ.sigmaFiniteSet)
Tactic: have := isSeparable_of_sigmaFinite (μ.restrict μ.sigmaFiniteSet)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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)
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have rcases : ∀ (𝒜 : Set (Set X)) (count_𝒜 : 𝒜.Countable) (h𝒜 : (μ.restrict μ.sigmaFiniteSet).MeasureDense 𝒜),
  ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
Tactic: rcases exists_countable_measureDense (μ.restrict μ.sigmaFiniteSet) with ⟨𝒜, count_𝒜, h𝒜⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 𝒜
have refine_1 : ∀ s ∈ ℬ, MeasurableSet s
Tactic: refine ⟨ℬ, count_𝒜.image (fun s ↦ s ∩ μ.sigmaFiniteSet), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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
⊢ ∃ (𝒜 : Set (Set X)), 𝒜.Countable ∧ μ.MeasureDense 𝒜
have 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 ε
Tactic: refine ⟨ℬ, count_𝒜.image (fun s ↦ s ∩ μ.sigmaFiniteSet), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 < ε
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have refine_2 : ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
Tactic: rcases restrict_compl_sigmaFiniteSet_eq_zero_or_top μ s with hs | hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have refine_2₁ : ∀ (hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
Tactic: rcases restrict_compl_sigmaFiniteSet_eq_zero_or_top μ s with hs | hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
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∞)
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have this₁ : 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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have 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 ε
Tactic: rcases h𝒜.approx s ms this ε ε_pos with ⟨t, t_mem, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
have refine_2 : (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
Tactic: refine ⟨t ∩ μ.sigmaFiniteSet, ⟨t, t_mem, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞)
  ((μ : (a : Set X) → ℝ≥0∞) ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) : ℝ≥0∞) (⊥ : ℝ≥0∞)
Tactic: rw [diff_eq_compl_inter, inter_symmDiff_distrib_left, ← ENNReal.bot_eq_zero, eq_bot_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
  0
Tactic: rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm,
                  ← inter_assoc, inter_compl_self, empty_inter, measure_empty, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
  0
Tactic: rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm,
                  ← inter_assoc, inter_compl_self, empty_inter, measure_empty, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
  0
Tactic: rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm,
                  ← inter_assoc, inter_compl_self, empty_inter, measure_empty, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
have rw₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ t ∩ μ.sigmaFiniteSet) : ℝ≥0∞) =
  0
Tactic: rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm,
                  ← inter_assoc, inter_compl_self, empty_inter, measure_empty, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
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 ε
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
rw₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ t ∩ μ.sigmaFiniteSet) : ℝ≥0∞) =
    0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
have rw₄ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ (μ.sigmaFiniteSetᶜ ∩ t)) : ℝ≥0∞) =
  0
Tactic: rw [inter_comm, ← μ.restrict_apply ms, hs, ← inter_assoc, inter_comm,
                  ← inter_assoc, inter_compl_self, empty_inter, measure_empty, zero_add]