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
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ 𝒜,
    Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have rcases : ∀ (t : Set X) (t_mem : t ∈ 𝒜) (ht : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε),
  ∃ t ∈ 𝒜,
    Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
Tactic: rcases h𝒜.approx s ms hμs ε ε_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 ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
⊢ Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs c = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs c = x})
have inl : Subset (α := Set ↥(Lp E p μ))
  {x : ↥(Lp E p μ) |
    ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
      indicatorConstLp (s := s) p hs hμs 0 = x}
  (closure
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p sorry hμs 0 = x})
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
inl :
  Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs 0 = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs 0 = x})
⊢ Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs c = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs c = x})
have inr : ∀ (hc : c ≠ 0),
  Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs c = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p sorry hμs c = x})
Tactic: obtain rfl | hc := eq_or_ne c 0
-- 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𝒜 : μ.MeasureDense 𝒜
⊢ Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs 0 = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs 0 = x})
have inl : Subset (α := Set ↥(Lp E p μ))
  {x : ↥(Lp E p μ) |
    ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
      indicatorConstLp (s := s) p hs hμs 0 = x}
  {x : ↥(Lp E p μ) |
    ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
      indicatorConstLp (s := s) p sorry hμs 0 = x}
Tactic: refine Subset.trans ?_ subset_closure
-- 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𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p ⋯ hμs 0 = x}
    (indicatorConstLp (s := s) p ms hμs 0)
have inl : ∀ (t : Set X) (ht : t ∈ 𝒜) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Membership.mem (γ := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p sorry hμs 0 = x}
    (indicatorConstLp (s := s) p ms hμs 0)
Tactic: obtain ⟨t, ht, hμt⟩ := h𝒜.nonempty'
-- 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𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p ⋯ hμs 0 = x}
    (indicatorConstLp (s := s) p ms hμs 0)
have inl : Eq (α := ↥(Lp E p μ)) (indicatorConstLp (s := t) p sorry hμt 0) (indicatorConstLp (s := s) p ms hμs 0)
Tactic: refine ⟨t, ht, hμt, ?_⟩
-- 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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
⊢ Subset (α := Set ↥(Lp E p μ))
    {x : ↥(Lp E p μ) |
      ∃ (s : Set X) (hs : MeasurableSet s) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
        indicatorConstLp (s := s) p hs hμs c = x}
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs c = x})
have p_pos : 0 < p
Tactic: have p_pos : 0 < p := 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 ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set ↥(Lp E p μ))
    (closure
      {x : ↥(Lp E p μ) |
        ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
          indicatorConstLp (s := s) p ⋯ hμs c = x})
    (indicatorConstLp (s := s) p ms hμs c)
have inr : ∀ (ε : ℝ) (hε : ε > 0),
  ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p sorry hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) p ms hμs c) b < ε
Tactic: refine Metric.mem_closure_iff.2 fun ε 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 ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
⊢ ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p ⋯ hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) p ms hμs c) b < ε
have aux : 0 < (ε / ‖c‖) ^ p.toReal
Tactic: have aux : 0 < (ε / ‖c‖) ^ p.toReal := rpow_pos_of_pos (div_pos hε (norm_pos_iff.2 hc)) _
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
⊢ ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p ⋯ hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) p ms hμs c) b < ε
have inr : ∀ (t : Set X) (ht : t ∈ 𝒜) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)),
  ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p sorry hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) p ms hμs c) b < ε
Tactic: obtain ⟨t, ht, hμt, hμst⟩ := h𝒜.fin_meas_approx ms hμs ((ε / ‖c‖) ^ p.toReal) aux
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ∃ (b : ↥(Lp E p μ)),
    Membership.mem (γ := Set ↥(Lp E p μ))
        {x : ↥(Lp E p μ) |
          ∃ (s : Set X) (hs : s ∈ 𝒜) (hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
            indicatorConstLp (s := s) p ⋯ hμs c = x}
        b ∧
      dist (indicatorConstLp (s := s) p ms hμs c) b < ε
have inr : dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs c) (indicatorConstLp (s := t) p sorry hμt c) < ε
Tactic: refine ⟨indicatorConstLp p (h𝒜.measurable t ht) hμt c,
      ⟨t, ht, hμt, 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 ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ dist (α := ↥(Lp E p μ)) (indicatorConstLp (s := s) p ms hμs c) (indicatorConstLp (s := t) p ⋯ hμt c) < ε
have inr : ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ε
Tactic: rw [dist_indicatorConstLp_eq_norm, norm_indicatorConstLp p_pos.ne.symm p_ne_top.elim]
-- 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)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)
have this : 0 < p.toReal
Tactic: have := toReal_pos p_pos.ne.symm p_ne_top.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 ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
this : 0 < p.toReal
⊢ ‖c‖ * ENNReal.toReal ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t)) ^ (1 / p.toReal) <
    ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)
have hbc : ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal) ≠ ∞
Tactic: gcongr
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε
have rw : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ (1 / p.toReal) = ε
Tactic: rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
rw : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ (1 / p.toReal) = ε
⊢ ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε
have rw₁ : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ p.toReal⁻¹ = ε
Tactic: rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
rw : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ (1 / p.toReal) = ε
rw₁ : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ p.toReal⁻¹ = ε
⊢ ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε
have rw₂ : ‖c‖ * (ε / ‖c‖) = ε
Tactic: rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
rw : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ (1 / p.toReal) = ε
rw₁ : ‖c‖ * ((ε / ‖c‖) ^ p.toReal) ^ p.toReal⁻¹ = ε
rw₂ : ‖c‖ * (ε / ‖c‖) = ε
⊢ ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε
have rw₃ : ε = ε
Tactic: rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ε
have have : ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)
Tactic: calc
      ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal)
        < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) := by
          have := toReal_pos p_pos.ne.symm p_ne_top.elim
          rw [measureReal_def]
          gcongr
          exact ofReal_ne_top
      _ = ε := by
        rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]
-- 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𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
have : ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)
⊢ ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ε
have have₁ : ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) = ε
Tactic: calc
      ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal)
        < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) := by
          have := toReal_pos p_pos.ne.symm p_ne_top.elim
          rw [measureReal_def]
          gcongr
          exact ofReal_ne_top
      _ = ε := by
        rw [toReal_ofReal (by positivity),
          one_div, Real.rpow_rpow_inv (by positivity) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne',
          mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ (t : Set X),
    Membership.mem (γ := Set (Set X))
        {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} t ∧
      (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have rcases : ∀ (t : Set X) (t_mem : t ∈ 𝒜) (hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hμst : (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε),
  ∃ (t : Set X),
    Membership.mem (γ := Set (Set X))
        {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)} t ∧
      (μ : (a : Set X) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
Tactic: rcases Measure.MeasureDense.fin_meas_approx h𝒜 ms hμs ε ε_pos with ⟨t, t_mem, hμt, hμst⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (hypothesis)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
⊢ MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (s ∆ t) < ε
have ms₁ : MeasurableSet s
Tactic: rw [hgen] at ms
Cleared hypotheses: ms
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
ht_1 : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε
⊢ MeasurableSet tᶜ ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε
have compl : ∀ (ε : ℝ) (ε_pos : 0 < ε), ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε
Tactic: refine ⟨ht.1.compl, fun ε ε_pos ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s t : Set X
ht_1 : MeasurableSet t
ht : MeasurableSet t ∧ ∀ (ε : ℝ), 0 < ε → ∃ t_1 ∈ 𝒜, μ.real (t ∆ t_1) < ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε
have compl : ∀ (u : Set X) (u_mem : u ∈ 𝒜) (hμtcu : μ.real (t ∆ u) < ε), ∃ t_1 ∈ 𝒜, μ.real (tᶜ ∆ t_1) < ε
Tactic: obtain ⟨u, u_mem, hμtcu⟩ := ht.2 ε ε_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
inst : IsFiniteMeasure μ
h𝒜 : IsSetAlgebra 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
f : ℕ → Set X
hs : ∀ (n : ℕ), MeasurableSet (f n)
hf : ∀ (n : ℕ), MeasurableSet (f n) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real (f n ∆ t) < ε
⊢ MeasurableSet.{u_1} (α := X) (⋃ (i : ℕ), f i) ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
have iUnion : ∀ (ε : ℝ) (ε_pos : 0 < ε), ∃ t ∈ 𝒜, μ.real ((⋃ (i : ℕ), f i) ∆ t) < ε
Tactic: refine ⟨MeasurableSet.iUnion (fun n ↦ (hf n).1), fun ε ε_pos ↦ ?_⟩