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_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 ε
⊢ (μ : (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]
-- 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 ε
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 ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
have refine_2₅ : (μ : (a : Set X) → ℝ≥0∞) ((s ∩ μ.sigmaFiniteSet) ∆ (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]
-- 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 ε
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 ε
⊢ (μ : (a : Set X) → ℝ≥0∞) (s ∆ (t ∩ μ.sigmaFiniteSet)) < ENNReal.ofReal ε
have refine_2₆ : (μ : (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]
-- 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 < ε
hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ t ∈ ℬ, (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have refine_2 : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine False.elim <| hμs ?_
-- 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 < ε
hs : Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_2 : LE.le (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [eq_top_iff, ← 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 ≠ ∞)
𝒜 : Set (Set X)
hμ : IsSeparable μ
⊢ IsSeparable μ.completion
have obtain : ∀ (𝒜 : Set (Set X)) (count_𝒜 : 𝒜.Countable) (h𝒜 : μ.MeasureDense 𝒜), IsSeparable μ.completion
Tactic: obtain ⟨𝒜, count_𝒜, h𝒜⟩ := exists_countable_measureDense μ
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
⊢ _root_.SecondCountableTopology ↥(Lp E p μ)
have refine : SeparableSpace ↥(Lp E p μ)
Tactic: refine @UniformSpace.secondCountable_of_separable _ _ _ ?_
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
⊢ SeparableSpace ↥(Lp E p μ)
have rcases : ∀ (𝒜 : Set (Set X)) (count_𝒜 : 𝒜.Countable) (h𝒜 : μ.MeasureDense 𝒜), SeparableSpace ↥(Lp E p μ)
Tactic: rcases exists_countable_measureDense μ with ⟨𝒜, count_𝒜, h𝒜⟩
-- 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 : IsSeparable μ
inst_2 : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
⊢ SeparableSpace ↥(Lp E p μ)
have h𝒜₀ : μ.MeasureDense {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
Tactic: have h𝒜₀ := Measure.MeasureDense.fin_meas h𝒜
-- 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 : 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 𝒜₀
⊢ SeparableSpace ↥(Lp E p μ)
have count_𝒜₀ : 𝒜₀.Countable
Tactic: have count_𝒜₀ : 𝒜₀.Countable := count_𝒜.mono fun _ ⟨h, _⟩ ↦ h
-- 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 : 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
⊢ SeparableSpace ↥(Lp E p μ)
have p_ne_zero : p ≠ 0
Tactic: have p_ne_zero : p ≠ 0 := ne_of_gt <| lt_of_lt_of_le (by simp) one_le_p.elim
-- 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 : 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
⊢ SeparableSpace ↥(Lp E p μ)
have rcases : ∀ (u : Set E) (countable_u : u.Countable) (dense_u : Dense u), SeparableSpace ↥(Lp E p μ)
Tactic: rcases exists_countable_dense E with ⟨u, countable_u, dense_u⟩
-- 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 : 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
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
⊢ SeparableSpace ↥(Lp E p μ)
have refine_1 : D.Countable
Tactic: refine ⟨D, ?_, ?_⟩
-- 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 : 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
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
refine_1 : D.Countable
⊢ SeparableSpace ↥(Lp E p μ)
have refine_2 : Dense D
Tactic: refine ⟨D, ?_, ?_⟩
-- 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 : 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
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
⊢ D.Countable
have this : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
Tactic: have := count_𝒜₀.to_subtype
-- 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 : 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
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
⊢ D.Countable
have this₁ : Countable.{u_2 + 1} (↑u : Type u_2)
Tactic: have := countable_u.to_subtype
-- 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 : 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
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this_1 : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
this : Countable.{u_2 + 1} (↑u : Type u_2)
n : ℕ
d : Fin n → (↑u : Type u_2)
s : Fin n → (↑𝒜₀ : Type u_1)
⊢ key n d s ∈ range f
have w : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))
Tactic: use ⟨n, (d, s)⟩
-- 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 : 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
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this_1 : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
this : Countable.{u_2 + 1} (↑u : Type u_2)
n : ℕ
d : Fin n → (↑u : Type u_2)
s : Fin n → (↑𝒜₀ : Type u_1)
w : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))
⊢ key n d s ∈ range f
have h : f (Sigma.mk (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) n (d, s)) =
  key n d s
Tactic: use ⟨n, (d, s)⟩
-- 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 : 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
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (d : Fin n → (↑u : Type u_2)) → (s : Fin n → (↑𝒜₀ : Type u_1)) → ↥(Lp E p μ) :=
  fun (n : ℕ) (d : Fin n → (↑u : Type u_2)) (s : Fin n → (↑𝒜₀ : Type u_1)) ↦
    ∑ i : Fin n, indicatorConstLp (s := (↑(s i) : Set X)) p ⋯ ⋯ (↑(d i) : E)
D : Set ↥(Lp E p μ) :=
  {s : ↥(Lp E p μ) | ∃ (n : ℕ) (d : Fin n → (↑u : Type u_2)) (t : Fin n → (↑𝒜₀ : Type u_1)), s = key n d t}
f : (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) → ↥(Lp E p μ) :=
  fun (nds : (n : ℕ) × Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))) ↦
    key (nds.fst (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))))
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).1
      nds.snd (β := fun (n : ℕ) ↦ Prod.{u_2, u_1} (Fin n → (↑u : Type u_2)) (Fin n → (↑𝒜₀ : Type u_1))).2
this_1 : Countable.{u_1 + 1} (↑𝒜₀ : Type u_1)
this : Countable.{u_2 + 1} (↑u : Type u_2)
⊢ D.Countable
have this₁ : D ⊆ range f
Tactic: have : D ⊆ range f := by
      rintro - ⟨n, d, s, rfl⟩
      use ⟨n, (d, s)⟩