awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
have hBU : ⋃ n, s ∩ B n = s := by rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)

Tactic:
rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]

Premises used: MeasureTheory.monotone_spanningSets, monotone_const, Monotone.inter, Monotone.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)

Tactic:
have : μ s = ⨆ n, μ (s ∩ B n) := by
    rw [← (monotone_const.inter (monotone_spanningSets μ)).measure_iUnion, hBU]
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
⊢ r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)

Tactic:
rw [this] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)
⊢ ⋃ (n : ℕ), s ∩ B n = s

Tactic:
rw [this] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
hr₁ : r < ⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n)
hBU₁ : ⋃ (n : ℕ), s ∩ B n = s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨆ (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞)

Tactic:
rw [this] at hr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
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
⊢ ∃ 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⟩

Premises used: Iff.mp, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
⟨s ∩ B n, inter_subset_left, ⟨hs.inter (measurableSet_spanningSets μ n), ?_⟩, hn⟩

Premises used: MeasureTheory.measurableSet_spanningSets, Set.inter_subset_left, Inter.inter, And.intro, Exists.intro, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
refine : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ K ⊆ s,
    (fun (s : Set α) ↦ MeasurableSet s ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) K ∧
      r < (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
refine ⟨s ∩ B n, inter_subset_left, ⟨hs.inter (measurableSet_spanningSets μ n), ?_⟩, hn⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
((measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top μ n)).ne

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Regular
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)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ B n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ((measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top μ n)).ne

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
have : ∀ (this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)), p ∅
⊢ p ∅

Tactic:
have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
⊢ ∃ K ⊆ univ, p K ∧ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
H isOpen_univ _ this

Premises used: isOpen_univ
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
obtain : ∀ (K : Set α) (hK : p K), p ∅
⊢ p ∅

Tactic:
obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this

Premises used: Set.univ, isOpen_univ
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
K : Set α
hK : p K
⊢ p ∅

Tactic:
simpa using hd hK isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 ∅

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
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 ∅
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)
⊢ ∃ (ε : ℝ≥0∞),
    ε ≠ 0 ∧ ε + ε ≤ (μ : (a : Set α) → ℝ≥0∞) s ∧ r = HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε)

Tactic:
use (μ s - r) / 2

Premises used: HSub.hSub, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 ∅
⊢ 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:
simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, tsub_eq_zero_iff_le]

Premises used: LT.lt.le, tsub_eq_zero_iff_le, ENNReal.sub_sub_cancel, ENNReal.add_halves
-- Module: Mathlib.MeasureTheory.Measure.Regular
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 ∅
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
⊢ ∃ K ⊆ s, p K ∧ r < (μ : (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]

Premises used: MeasureTheory.Measure.InnerRegularWRT.rfl, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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
⊢ ∃ 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⟩

Premises used: MeasurableSet.exists_isOpen_diff_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
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) < ε
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
⊢ ∃ 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'⟩

Premises used: Set.exists_isOpen_lt_of_lt, SDiff.sdiff
-- Module: Mathlib.MeasureTheory.Measure.Regular
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' < ε
⊢ U \ U' ⊆ s

Tactic:
replace hsU' := diff_subset_comm.1 hsU'
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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
⊢ ∃ 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⟩

Premises used: LT.lt.ne, MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
⟨K \ U', fun x hx => hsU' ⟨hKU hx.1, hx.2⟩, hd hKc hU'o, ENNReal.sub_lt_of_lt_add hεs ?_⟩

Premises used: SDiff.sdiff, And.right, And.left, And.intro, ENNReal.sub_lt_of_lt_add, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) ε
refine : (μ : (a : Set α) → ℝ≥0∞) s < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) (ε + ε)
⊢ ∃ K ⊆ s, p K ∧ HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε + ε) < (μ : (a : Set α) → ℝ≥0∞) K

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 ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) ε
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
μ.mono hsU

Premises used: MeasureTheory.OuterMeasure.mono, MeasureTheory.Measure.toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
hKr
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) ε
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∞) +
      ε
grw₁ : Set α
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∞) +
      ε
grw₃ : Set α
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥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]

Premises used: tsub_le_iff_right, Iff.mp, MeasureTheory.le_measure_diff