awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞) ε
⊢ 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:
gcongr
-- 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∞) ε
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ε + ε =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) (ε + ε)

Tactic:
add_assoc _ _ _

Premises used: add_assoc
-- 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∞) ε
μ₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε ≤
    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∞) +
      ε ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K \ U') : ℝ≥0∞) ε + ε
⊢ (μ : (a : Set α) → ℝ≥0∞) s < 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 _ _ _

Premises used: add_assoc, MeasureTheory.OuterMeasure.mono, SDiff.sdiff, MeasureTheory.Measure.toOuterMeasure, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
⊢ ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hfin : ∀ {s}, μ s ≠ ∞ := @(measure_ne_top μ)
-- Module: Mathlib.MeasureTheory.Measure.Regular
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

Tactic:
{ outerRegular := fun s hs r hr => ?_
        innerRegular := H }

Premises used: MeasureTheory.Measure.WeaklyRegular.mk
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞) ε
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
⊢ μ.WeaklyRegular

Tactic:
refine
      { outerRegular := fun s hs r hr => ?_
        innerRegular := H }
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
rcases :
  ∀ (r' : ℝ≥0∞) (hsr' : (μ : (a : Set α) → ℝ≥0∞) s < r') (hr'r : r' < r),
    ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
rcases exists_between hr with ⟨r', hsr', hr'r⟩

Premises used: exists_between
-- Module: Mathlib.MeasureTheory.Measure.Regular
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
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
⊢ ∃ 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⟩

Premises used: Iff.mpr, tsub_pos_iff_lt, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.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 : 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:
⟨U, hsU, hUo, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.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 : 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∞))
refine : (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ U ⊇ s, IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
refine ⟨U, hsU, hUo, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.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 : 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∞))
⊢ (μ : (a : Set α) → ℝ≥0∞) U ≤ r'

Tactic:
rw [add_tsub_cancel_of_le hsr'.le] at H

Premises used: LT.lt.le, add_tsub_cancel_of_le
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.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 : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
H : (μ : (a : Set α) → ℝ≥0∞) U ≤ r'
⊢ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
H.trans_lt hr'r

Premises used: LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.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 : Set α
hsU : U ⊇ s
hUo : IsOpen[inst_1] U
H : (μ : (a : Set α) → ℝ≥0∞) U ≤ r'
⊢ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
exact H.trans_lt hr'r

Premises used: LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
suffices :
  ∀ (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

Tactic:
suffices ∀ s, MeasurableSet s → ∀ ε, ε ≠ 0 → ∃ F, F ⊆ s ∧ ∃ U, U ⊇ s ∧
      IsClosed F ∧ IsOpen U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε by
    refine
      { outerRegular := fun s hs r hr => ?_
        innerRegular := H }
    rcases exists_between hr with ⟨r', hsr', hr'r⟩
    rcases this s hs _ (tsub_pos_iff_lt.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩
    refine ⟨U, hsU, hUo, ?_⟩
    rw [add_tsub_cancel_of_le hsr'.le] at H
    exact H.trans_lt hr'r
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
isOpen :
  ∀ (U : Set α) (hU : IsOpen[inst_1] U) (ε : ℝ≥0∞),
    ε ≠ 0 →
      ∃ F ⊆ U,
        ∃ U_1 ⊇ U,
          IsClosed[inst_1] F ∧
            IsOpen[inst_1] U_1 ∧
              (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε
compl :
  ∀ (t : Set α) (ht : MeasurableSet t),
    (∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ t,
            ∃ U ⊇ t,
              IsClosed[inst_1] F ∧
                IsOpen[inst_1] U ∧
                  (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                    (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε) →
      ∀ (ε : ℝ≥0∞),
        ε ≠ 0 →
          ∃ F ⊆ tᶜ,
            ∃ U ⊇ tᶜ,
              IsClosed[inst_1] F ∧
                IsOpen[inst_1] U ∧
                  (μ : (a : Set α) → ℝ≥0∞) tᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                    (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ε
iUnion :
  ∀ (f : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f) →
      ∀ (hf : ∀ (i : ℕ), MeasurableSet (f i)),
        (∀ (i : ℕ) (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ f i,
                ∃ U ⊇ f i,
                  IsClosed[inst_1] F ∧
                    IsOpen[inst_1] U ∧
                      (μ : (a : Set α) → ℝ≥0∞) (f i) ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                        (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) ε) →
          ∀ (ε : ℝ≥0∞),
            ε ≠ 0 →
              ∃ F ⊆ ⋃ (i : ℕ), f i,
                ∃ U ⊇ ⋃ (i : ℕ), f i,
                  IsClosed[inst_1] F ∧
                    IsOpen[inst_1] U ∧
                      (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) ≤
                          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
                        (μ : (a : Set α) → ℝ≥0∞) U ≤
                          HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) ε
⊢ ∀ (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∞) ε

Tactic:
apply MeasurableSet.induction_on_open
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
U : Set α
hU : IsOpen[inst_1] U
ε : ℝ≥0∞
hε : ε ≠ 0
isOpen :
  ∀ (F : Set α) (hsF : F ⊆ U) (hFc : IsClosed[inst_1] F)
    (hF : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε),
    ∃ F ⊆ U,
      ∃ U_1 ⊇ U,
        IsClosed[inst_1] F ∧
          IsOpen[inst_1] U_1 ∧
            (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
              (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε
⊢ ∃ F ⊆ U,
    ∃ U_1 ⊇ U,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U_1 ∧
          (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε

Tactic:
rcases H.exists_subset_lt_add isClosed_empty hU hfin hε with ⟨F, hsF, hFc, hF⟩

Premises used: isClosed_empty, MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
U : Set α
hU : IsOpen[inst_1] U
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hsF : F ⊆ U
hFc : IsClosed[inst_1] F
hF : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε
⊢ ∃ F ⊆ U,
    ∃ U_1 ⊇ U,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U_1 ∧
          (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε

Tactic:
⟨F, hsF, U, Subset.rfl, hFc, hU, hF.le, le_self_add⟩

Premises used: LT.lt.le, Set.Subset.rfl, And.intro, Exists.intro, le_self_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
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∞)
U : Set α
hU : IsOpen[inst_1] U
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hsF : F ⊆ U
hFc : IsClosed[inst_1] F
hF : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε
⊢ ∃ F ⊆ U,
    ∃ U_1 ⊇ U,
      IsClosed[inst_1] F ∧
        IsOpen[inst_1] U_1 ∧
          (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε ∧
            (μ : (a : Set α) → ℝ≥0∞) U_1 ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε

Tactic:
exact ⟨F, hsF, U, Subset.rfl, hFc, hU, hF.le, le_self_add⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
μ : Measure α
inst_3 : IsFiniteMeasure μ
H_1 : μ.InnerRegularWRT IsClosed[inst_1] IsOpen[inst_1]
hfin : ∀ {s : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
H :
  ∀ (ε : ℝ≥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∞) ε
ε : ℝ≥0∞
hε : ε ≠ 0
compl :
  ∀ (F : Set α) (hFs : F ⊆ s) (U : Set α) (hsU : U ⊇ s) (hFc : IsClosed[inst_1] F) (hUo : IsOpen[inst_1] U)
    (hF : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) F : ℝ≥0∞) ε)
    (hU : (μ : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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∞) ε
⊢ ∃ 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∞) ε

Tactic:
rcases H ε hε with ⟨F, hFs, U, hsU, hFc, hUo, hF, hU⟩