awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
⊢ ⋃ (n : ℕ), s ∩ B n = s
have rw : s ∩ ⋃ (i : ℕ), B i = s
Tactic: rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
rw : s ∩ ⋃ (i : ℕ), B i = s
⊢ ⋃ (n : ℕ), s ∩ B n = s
have rw₁ : s ∩ univ = s
Tactic: rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
rw : s ∩ ⋃ (i : ℕ), B i = s
rw₁ : s ∩ univ = s
⊢ ⋃ (n : ℕ), s ∩ B n = s
have rw₂ : s = s
Tactic: rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
⊢ ∃ K ⊆ s,
    (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) K ∧
      r < (μ : (a : Set α) → ℝ≥0∞) K
have hBU : ⋃ (n : ℕ), s ∩ B n = s
Tactic: have hBU : ⋃ n, s ∩ B n = s := by rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ (n : ℕ), s ∩ B n = s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ spanningSets μ i) : ℝ≥0∞)
Tactic: rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ (n : ℕ), s ∩ B n = s
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s ∩ spanningSets μ i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ (n : ℕ), s ∩ B n = s
⊢ ∃ K ⊆ s,
    (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) K ∧
      r < (μ : (a : Set α) → ℝ≥0∞) K
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)
Tactic: have : μ s = ⨆ n, μ (s ∩ B n) := by
    rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
B : ℕ → Set α := spanningSets μ
hBU : ⋃ (n : ℕ), s ∩ B n = s
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)
⊢ ∃ K ⊆ s,
    (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) K ∧
      r < (μ : (a : Set α) → ℝ≥0∞) K
have hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)
Tactic: rw [this] at hr
Cleared hypotheses: hr, hBU, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)
hBU : ⋃ (n : ℕ), s ∩ B n = s
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)
⊢ ∃ K ⊆ s,
    (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) K ∧
      r < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (n : ℕ) (hn : r < (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)),
  ∃ K ⊆ s,
    (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) K ∧
      r < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
B : ℕ → Set α := spanningSets μ
hr : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)
hBU : ⋃ (n : ℕ), s ∩ B n = s
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)
n : ℕ
hn : r < (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)
⊢ ∃ K ⊆ s,
    (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) K ∧
      r < (μ : (a : Set α) → ℝ≥0∞) K
have refine : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨s ∩ B n, inter_subset_left, ⟨hs.inter (measurableSet_spanningSets μ n), ?_⟩, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
⊢ p ∅
have have : ∀ (this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)), p ∅
Tactic: have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ p ∅
have obtain : ∀ (K : Set α) (hK : p K), p ∅
Tactic: obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have h0 : p ∅
Tactic: have h0 : p ∅ := by
    have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
    obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
    simpa using hd hK isOpen_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
h0 : p ∅
⊢ ∃ (ε : ℝ≥0∞),
    ε ≠ 0 ∧ ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s ∧ r = HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε)
have h : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) r / 2 ≠ 0 ∧
  HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) r / 2 +
        HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) r / 2 ≤
      (μ : (a : Set α) → ℝ≥0∞) s ∧
    r =
      HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) r / 2 +
          HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) r / 2)
Tactic: use (μ s - r) / 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
h0 : p ∅
⊢ ∃ K ⊆ s, p K ∧ r < (μ : (a : Set α) → ℝ≥0∞) K
have obtain : ∀ (ε : ℝ≥0∞) (hε : ε ≠ 0) (hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s)
  (hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s),
  ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: obtain ⟨ε, hε, hεs, rfl⟩ : ∃ ε ≠ 0, ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
    use (μ s - r) / 2
    simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, tsub_eq_zero_iff_le]
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (U : Set α) (hsU : U ⊇ s) (hUo : IsOpen[inst_1] U)
  (hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) (hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε),
  ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases hs.exists_isOpen_diff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε
⊢ ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (U' : Set α) (hsU' : U' ⊇ U \ s) (hU'o : IsOpen[inst_1] U') (hμU' : (μ : (a : Set α) → ℝ≥0∞) U' < ε),
  ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases (U \ s).exists_isOpen_lt_of_lt _ hμU with ⟨U', hsU', hU'o, hμU'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε
U' : Set α
hsU' : U' ⊇ U \ s
hU'o : IsOpen[inst_1] U'
hμU' : (μ : (a : Set α) → ℝ≥0∞) U' < ε
⊢ ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
have hsU'₁ : U \ U' ⊆ s
Tactic: replace hsU' := diff_subset_comm.1 hsU'
Cleared hypotheses: hsU'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst_1] U'
hμU' : (μ : (a : Set α) → ℝ≥0∞) U' < ε
hsU' : U \ U' ⊆ s
⊢ ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
have rcases : ∀ (K : Set α) (hKU : K ⊆ U) (hKc : p K)
  (hKr : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε),
  ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
Tactic: rcases H.exists_subset_lt_add h0 hUo hUt.ne hε with ⟨K, hKU, hKc, hKr⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst_1] U'
hμU' : (μ : (a : Set α) → ℝ≥0∞) U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K
have refine : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) (ε + ε)
Tactic: refine ⟨K \ U', fun x hx => hsU' ⟨hKU hx.1, hx.2⟩, hd hKc hU'o, ENNReal.sub_lt_of_lt_add hεs ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst_1] U'
hμU' : (μ : (a : Set α) → ℝ≥0∞) U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U' : ℝ≥0∞) +
      ε
have grw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U' : ℝ≥0∞) + ε ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U' : ℝ≥0∞) + ε
Tactic: grw [tsub_le_iff_right.1 le_measure_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst_1] U'
hμU' : (μ : (a : Set α) → ℝ≥0∞) U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) (ε + ε)
have μ₁ : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U' : ℝ≥0∞) + ε
Tactic: calc
    μ s ≤ μ U := μ.mono hsU
    _ < μ K + ε := hKr
    _ ≤ μ (K \ U') + μ U' + ε := by grw [tsub_le_iff_right.1 le_measure_diff]
    _ ≤ μ (K \ U') + ε + ε := by gcongr
    _ = μ (K \ U') + (ε + ε) := add_assoc _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst_1 : TopologicalSpace α
inst_2 : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst_1]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst_1] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s
hr : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
hUt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hμU : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst_1] U'
hμU' : (μ : (a : Set α) → ℝ≥0∞) U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
μ₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U' : ℝ≥0∞) +
      ε
⊢ (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) (ε + ε)
have μ₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U' : ℝ≥0∞) + ε ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ε + ε
Tactic: calc
    μ s ≤ μ U := μ.mono hsU
    _ < μ K + ε := hKr
    _ ≤ μ (K \ U') + μ U' + ε := by grw [tsub_le_iff_right.1 le_measure_diff]
    _ ≤ μ (K \ U') + ε + ε := by gcongr
    _ = μ (K \ U') + (ε + ε) := add_assoc _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
⊢ μ.WeaklyRegular
have hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hfin : ∀ {s}, μ s ≠ ∞ := @(measure_ne_top μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ s,
            ∃ U ⊇ s,
              IsClosed[inst_1] F ∧
                IsOpen[inst_1] U ∧
                  (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                    (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ μ.WeaklyRegular
have outerRegular : ∀ (s : Set α) (hs : MeasurableSet s) (r : ℝ≥0∞) (hr : r > (μ : (a : Set α) → ℝ≥0∞) s),
  ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
Tactic: refine
      { outerRegular := fun s hs r hr => ?_
        innerRegular := H }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ s,
            ∃ U ⊇ s,
              IsClosed[inst_1] F ∧
                IsOpen[inst_1] U ∧
                  (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                    (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have rcases : ∀ (r' : ℝ≥0∞) (hsr' : (μ : (a : Set α) → ℝ≥0∞) s < r') (hr'r : r' < r),
  ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
Tactic: rcases exists_between hr with ⟨r', hsr', hr'r⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ s,
            ∃ U ⊇ s,
              IsClosed[inst_1] F ∧
                IsOpen[inst_1] U ∧
                  (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                    (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > (μ : (a : Set α) → ℝ≥0∞) s
r' : ℝ≥0∞
hsr' : (μ : (a : Set α) → ℝ≥0∞) s < r'
hr'r : r' < r
⊢ ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
have rcases : ∀ (U : Set α) (hsU : U ⊇ s) (hUo : IsOpen[inst_1] U)
  (H :
    (μ : (a : Set α) → ℝ≥0∞) U ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HSub.hSub (β := ℝ≥0∞) r' ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))),
  ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
Tactic: rcases this s hs _ (tsub_pos_iff_lt.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩