awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ (μ.sigmaFiniteSetᶜ ∩ t)) : ℝ≥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]
-- 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
rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ (μ.sigmaFiniteSetᶜ ∩ t)) : ℝ≥0∞) =
    0
rw₅ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ μ.sigmaFiniteSetᶜ ∩ t) : ℝ≥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∞) (∅ ∩ 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]
-- 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
rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ (μ.sigmaFiniteSetᶜ ∩ t)) : ℝ≥0∞) =
    0
rw₅ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ μ.sigmaFiniteSetᶜ ∩ t) : ℝ≥0∞) =
    0
rw₆ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (∅ ∩ t) : ℝ≥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∞) ∅ : ℝ≥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
rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ (μ.sigmaFiniteSetᶜ ∩ t)) : ℝ≥0∞) =
    0
rw₅ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ μ.sigmaFiniteSetᶜ ∩ t) : ℝ≥0∞) =
    0
rw₆ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞) = 0
rw₇ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ∅ : ℝ≥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
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
rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ (μ.sigmaFiniteSetᶜ ∩ t)) : ℝ≥0∞) =
    0
rw₅ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSet ∩ μ.sigmaFiniteSetᶜ ∩ t) : ℝ≥0∞) =
    0
rw₆ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (∅ ∩ t) : ℝ≥0∞) = 0
rw₇ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ∅ : ℝ≥0∞) = 0
rw₈ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
have rw₉ : Eq (α := ℝ≥0∞) 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 ε
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) : ℝ≥0∞)
    (⊥ : ℝ≥0∞)
have μ₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
  0
Tactic: calc
            μ ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)))
              ≤ μ ((μ.sigmaFiniteSetᶜ ∩ s) ∪ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) :=
                measure_mono symmDiff_subset_union
            _ ≤ μ (μ.sigmaFiniteSetᶜ ∩ s) + μ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) :=
                measure_union_le _ _
            _ = 0 := by
                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 (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_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 ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
have this₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : μ (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) = 0 := by
          rw [diff_eq_compl_inter, inter_symmDiff_distrib_left, ← ENNReal.bot_eq_zero, eq_bot_iff]
          calc
            μ ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)))
              ≤ μ ((μ.sigmaFiniteSetᶜ ∩ s) ∪ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) :=
                measure_mono symmDiff_subset_union
            _ ≤ μ (μ.sigmaFiniteSetᶜ ∩ s) + μ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) :=
                measure_union_le _ _
            _ = 0 := by
                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_2 : 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 ε
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
have refine_2 : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) <
  ENNReal.ofReal ε
Tactic: rwa [← measure_inter_add_diff _ measurableSet_sigmaFiniteSet, this, add_zero,
          inter_symmDiff_distrib_right, inter_assoc, inter_self, ← inter_symmDiff_distrib_right,
          ← μ.restrict_apply' measurableSet_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_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_2 : 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 ε
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) <
    ENNReal.ofReal ε
rwa : Measure X
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
have refine_2₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) : ℝ≥0∞)
    (0 : ℝ≥0∞) <
  ENNReal.ofReal ε
Tactic: rwa [← measure_inter_add_diff _ measurableSet_sigmaFiniteSet, this, add_zero,
          inter_symmDiff_distrib_right, inter_assoc, inter_self, ← inter_symmDiff_distrib_right,
          ← μ.restrict_apply' measurableSet_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_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_2 : 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 ε
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) <
    ENNReal.ofReal ε
rwa : Measure X
refine_2₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) : ℝ≥0∞)
      (0 : ℝ≥0∞) <
    ENNReal.ofReal ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
have refine_2₂ : (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) < ENNReal.ofReal ε
Tactic: rwa [← measure_inter_add_diff _ measurableSet_sigmaFiniteSet, this, add_zero,
          inter_symmDiff_distrib_right, inter_assoc, inter_self, ← inter_symmDiff_distrib_right,
          ← μ.restrict_apply' measurableSet_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_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_2 : 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 ε
this : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) <
    ENNReal.ofReal ε
rwa : Measure X
refine_2₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) : ℝ≥0∞)
      (0 : ℝ≥0∞) <
    ENNReal.ofReal ε
refine_2₂ : (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) ∩ μ.sigmaFiniteSet) < ENNReal.ofReal ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
have refine_2₃ : (μ : (a : Set X) → ℝ≥0∞) ((s ∩ μ.sigmaFiniteSet) ∆ (t ∩ μ.sigmaFiniteSet ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
Tactic: rwa [← measure_inter_add_diff _ measurableSet_sigmaFiniteSet, this, add_zero,
          inter_symmDiff_distrib_right, inter_assoc, inter_self, ← inter_symmDiff_distrib_right,
          ← μ.restrict_apply' measurableSet_sigmaFiniteSet]