awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ε
rw :
  LE.le (α := ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) : ℝ≥0∞)
    (⊥ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet) \ μ.sigmaFiniteSet) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [diff_eq_compl_inter, inter_symmDiff_distrib_left, ← ENNReal.bot_eq_zero, eq_bot_iff]

Premises used: Set.inter_symmDiff_distrib_left, ENNReal.bot_eq_zero, Set.diff_eq_compl_inter, eq_bot_iff
-- 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 ε
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet))) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s ∪ μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞)

Tactic:
measure_mono symmDiff_subset_union

Premises used: Set.symmDiff_subset_union, MeasureTheory.measure_mono
-- 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 ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s ∪ μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞)

Tactic:
measure_union_le _ _

Premises used: MeasureTheory.measure_union_le
-- 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 ε
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
rw₉ rw₁₀ : Eq (α := ℝ≥0∞) 0 0
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ 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]

Premises used: MeasureTheory.Measure.restrict_apply, Set.empty_inter, MeasureTheory.measure_empty, zero_add, Set.inter_comm, Set.inter_compl_self, Set.inter_assoc
-- 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 ε
μ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ s) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (μ.sigmaFiniteSetᶜ ∩ (t ∩ μ.sigmaFiniteSet)) : ℝ≥0∞) =
    0
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) ((μ.sigmaFiniteSetᶜ ∩ s) ∆ (μ.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]

Premises used: Compl.compl, MeasureTheory.Measure.sigmaFiniteSet, Set.symmDiff_subset_union, Inter.inter, MeasureTheory.measure_mono, Union.union, DFunLike.coe, symmDiff, MeasureTheory.measure_union_le
-- 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 ε
⊢ 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]
-- 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_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 ε
refine_2₃ :
  (μ : (a : Set X) → ℝ≥0∞) ((s ∩ μ.sigmaFiniteSet) ∆ (t ∩ μ.sigmaFiniteSet ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
refine_2₄ :
  (μ : (a : Set X) → ℝ≥0∞) ((s ∩ μ.sigmaFiniteSet) ∆ (t ∩ (μ.sigmaFiniteSet ∩ μ.sigmaFiniteSet))) < ENNReal.ofReal ε
refine_2₅ : (μ : (a : Set X) → ℝ≥0∞) ((s ∩ μ.sigmaFiniteSet) ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
refine_2₆ : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t ∩ μ.sigmaFiniteSet) < ENNReal.ofReal ε
refine_2₇ refine_2₈ refine_2₉ refine_2₁₀ : (μ.restrict μ.sigmaFiniteSet : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.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]

Premises used: Set.inter_self, MeasureTheory.measurableSet_sigmaFiniteSet, MeasureTheory.measure_inter_add_diff, Set.inter_symmDiff_distrib_right, add_zero, MeasureTheory.Measure.restrict_apply', Set.inter_assoc
-- 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∞)
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
False.elim <| hμs ?_

Premises used: False.elim
-- 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∞)
refine_2 : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε

Tactic:
refine False.elim <| hμs ?_

Premises used: False.elim
-- 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∞)
refine_2 :
  LE.le (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [eq_top_iff, ← hs]

Premises used: eq_top_iff
-- 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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
μ.restrict_le_self _

Premises used: MeasureTheory.Measure.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 : 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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact μ.restrict_le_self _

Premises used: MeasureTheory.Measure.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 ≠ ∞)
𝒜 : Set (Set X)
hμ : IsSeparable μ
obtain : ∀ (𝒜 : Set (Set X)) (count_𝒜 : 𝒜.Countable) (h𝒜 : μ.MeasureDense 𝒜), IsSeparable μ.completion
⊢ IsSeparable μ.completion

Tactic:
obtain ⟨𝒜, count_𝒜, h𝒜⟩ := exists_countable_measureDense μ

Premises used: 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)
hμ : IsSeparable μ
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
⊢ IsSeparable μ.completion

Tactic:
⟨𝒜, count_𝒜, h𝒜.completion⟩

Premises used: MeasureTheory.Measure.MeasureDense.completion, MeasureTheory.IsSeparable.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)
hμ : IsSeparable μ
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
⊢ IsSeparable μ.completion

Tactic:
exact ⟨𝒜, count_𝒜, h𝒜.completion⟩
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
⊢ _root_.SecondCountableTopology ↥(Lp E p μ)

Tactic:
@UniformSpace.secondCountable_of_separable _ _ _ ?_

Premises used: UniformSpace.secondCountable_of_separable
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
refine : SeparableSpace ↥(Lp E p μ)
⊢ _root_.SecondCountableTopology ↥(Lp E p μ)

Tactic:
refine @UniformSpace.secondCountable_of_separable _ _ _ ?_

Premises used: UniformSpace.secondCountable_of_separable
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
rcases : ∀ (𝒜 : Set (Set X)) (count_𝒜 : 𝒜.Countable) (h𝒜 : μ.MeasureDense 𝒜), SeparableSpace ↥(Lp E p μ)
⊢ SeparableSpace ↥(Lp E p μ)

Tactic:
rcases exists_countable_measureDense μ with ⟨𝒜, count_𝒜, h𝒜⟩

Premises used: 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 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
⊢ μ.MeasureDense {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}

Tactic:
have h𝒜₀ := Measure.MeasureDense.fin_meas h𝒜
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
h𝒜₀ : μ.MeasureDense {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
⊢ let 𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)};
  μ.MeasureDense 𝒜₀

Tactic:
set 𝒜₀ := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
⊢ 𝒜₀.Countable

Tactic:
have count_𝒜₀ : 𝒜₀.Countable := count_𝒜.mono fun _ ⟨h, _⟩ ↦ h
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
⊢ LT.lt (α := ℝ≥0∞) 0 1

Tactic:
simp
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
⊢ p ≠ 0

Tactic:
have p_ne_zero : p ≠ 0 := ne_of_gt <| lt_of_lt_of_le (by simp) one_le_p.elim
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
rcases : ∀ (u : Set E) (countable_u : u.Countable) (dense_u : Dense u), SeparableSpace ↥(Lp E p μ)
⊢ SeparableSpace ↥(Lp E p μ)

Tactic:
rcases exists_countable_dense E with ⟨u, countable_u, dense_u⟩

Premises used: TopologicalSpace.exists_countable_dense