awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
obtain :
  ∀ (U : Set α) (hKU : K ⊆ U) (hUo : IsOpen[inst_1] U) (hμU : (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r),
    ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
obtain ⟨U, hKU, hUo, hμU⟩ : ∃ U, K ⊆ U ∧ IsOpen U ∧ μ.restrict V U < r :=
    exists_isOpen_lt_of_lt K r <| (restrict_apply_le _ _).trans_lt hr

Premises used: MeasureTheory.Measure.restrict_apply_le, Set.exists_isOpen_lt_of_lt, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
⟨U ∩ V, subset_inter hKU hKV, hUo.inter hVo, ?_⟩

Premises used: Inter.inter, Set.subset_inter, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r
refine : (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r
⊢ ∃ (U : Set α), K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < r

Tactic:
refine ⟨U ∩ V, subset_inter hKU hKV, hUo.inter hVo, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
r : ℝ≥0∞
hr : (μ : (a : Set α) → ℝ≥0∞) K < r
V : Set α
hKV : V ⊇ K
hVo : IsOpen[inst_1] V
hμV : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ.restrict V : (a : Set α) → ℝ≥0∞) U < r
rwa rwa₁ rwa₂ rwa₃ : ∀ (hμU : (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r), (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r
⊢ (μ : (a : Set α) → ℝ≥0∞) (U ∩ V) < r

Tactic:
rwa [restrict_apply hUo.measurableSet] at hμU

Premises used: MeasureTheory.Measure.restrict_apply, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
a :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
a₁ :
  LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
a :
  ∀ (i : Set α) (i_1 : K ⊆ i) (i_2 : IsOpen[inst_1] i),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
    (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
simp only [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (i : Set α) (i_1 : K ⊆ i) (i_2 : IsOpen[inst_1] i),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)

Tactic:
fun U KU _ ↦ measure_mono KU

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (i : Set α) (i_1 : K ⊆ i) (i_2 : IsOpen[inst_1] i),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)

Tactic:
exact fun U KU _ ↦ measure_mono KU

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
a :
  ∀ (c : ℝ≥0∞),
    (μ : (a : Set α) → ℝ≥0∞) K < c →
      ⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U < c
⊢ LE.le (α := ℝ≥0∞) (⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
apply le_of_forall_gt

Premises used: le_of_forall_gt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ∀ (c : ℝ≥0∞),
    (μ : (a : Set α) → ℝ≥0∞) K < c →
      ⨅ (U : Set α), ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst_1] U), (μ : (a : Set α) → ℝ≥0∞) U < c

Tactic:
simpa only [iInf_lt_iff, exists_prop, exists_and_left] using hK.exists_isOpen_lt_of_lt

Premises used: exists_and_left, exists_prop, iInf_lt_iff, IsCompact.exists_isOpen_lt_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
K : Set α
hK : IsCompact K
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ (U : Set α),
    K ⊆ U ∧ IsOpen[inst_1] U ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
hK.exists_isOpen_lt_of_lt _ (ENNReal.lt_add_right hK.measure_lt_top.ne hε)

Premises used: ENNReal.lt_add_right, IsCompact.measure_lt_top, IsCompact.exists_isOpen_lt_of_lt, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ε / 2 ≠ 0

Tactic:
have : ε / 2 ≠ 0 := (ENNReal.half_pos hε).ne'
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
rcases :
  ∀ (K : Set α) (hKs : K ⊆ s) (hKco : IsCompact K) (hKcl : IsClosed[inst_1] K)
    (hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2),
    ∃ (U : Set α),
      IsOpen[inst_1] U ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
rcases hs.exists_isCompact_isClosed_diff_lt hμs this with ⟨K, hKs, hKco, hKcl, hμK⟩

Premises used: MeasurableSet.exists_isCompact_isClosed_diff_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
rcases :
  ∀ (U : Set α) (hKU : K ⊆ U) (hUo : IsOpen[inst_1] U)
    (hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)),
    ∃ (U : Set α),
      IsOpen[inst_1] U ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
rcases hKco.exists_isOpen_lt_add (μ := μ) this with ⟨U, hKU, hUo, hμU⟩

Premises used: IsCompact.exists_isOpen_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
⟨U, hUo, hμU.trans_le le_top, ?_⟩

Premises used: LT.lt.trans_le, le_top, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
refine : (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
refine ⟨U, hUo, hμU.trans_le le_top, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ U) : ℝ≥0∞) <
    ε / 2 + ε / 2
⊢ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
rw [← ENNReal.add_halves ε, measure_symmDiff_eq hUo.nullMeasurableSet hs.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, IsOpen.nullMeasurableSet, ENNReal.add_halves, MeasureTheory.measure_symmDiff_eq
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
xz : (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε / 2
yw : (μ : (a : Set α) → ℝ≥0∞) (s \ U) < ε / 2
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ U) : ℝ≥0∞) <
    ε / 2 + ε / 2

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ K) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
apply : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (U \ K) < ε / 2

Tactic:
apply measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU

Premises used: MeasureTheory.measure_diff_lt_of_lt_add, IsClosed.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ne_top_of_le_ne_top hμs (by gcongr)

Premises used: ne_top_of_le_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (U \ K) : ℝ≥0∞)
μ₂ : (μ : (a : Set α) → ℝ≥0∞) (U \ K) < ε / 2
⊢ (μ : (a : Set α) → ℝ≥0∞) (U \ s) < ε / 2

Tactic:
calc
      μ (U \ s) ≤ μ (U \ K) := by gcongr
      _ < ε / 2 := by
        apply measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU
        exact ne_top_of_le_ne_top hμs (by gcongr)

Premises used: SDiff.sdiff, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ LE.le (α := WithTop ℝ≥0) ((μ : (a : Set α) → ℝ≥0∞) (s \ U) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ K) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst_1] K
hμK : (μ : (a : Set α) → ℝ≥0∞) (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst_1] U
hμU : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (ε / 2)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s \ U) < ε / 2

Tactic:
exact lt_of_le_of_lt (by gcongr) hμK

Premises used: lt_of_le_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hs : NullMeasurableSet s μ
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
rcases :
  ∀ (t : Set α) (htm : MeasurableSet t) (hst : s =ᶠ[ae μ] t),
    ∃ (U : Set α),
      IsOpen[inst_1] U ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
rcases hs with ⟨t, htm, hst⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [← measure_congr hst]

Premises used: MeasureTheory.measure_congr
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
rcases :
  ∀ (U : Set α) (hUo : IsOpen[inst_1] U) (hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hUs : (μ : (a : Set α) → ℝ≥0∞) (U ∆ t) < ε),
    ∃ (U : Set α),
      IsOpen[inst_1] U ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
rcases htm.exists_isOpen_symmDiff_lt (by rwa [← measure_congr hst]) hε with ⟨U, hUo, hμU, hUs⟩

Premises used: MeasurableSet.exists_isOpen_symmDiff_lt
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
U : Set α
hUo : IsOpen[inst_1] U
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUs : (μ : (a : Set α) → ℝ≥0∞) (U ∆ t) < ε
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
⟨U, hUo, hμU, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegularCompactLTTop
inst_3 : IsLocallyFiniteMeasure μ
inst_4 : R1Space α
inst_5 : BorelSpace α
s : Set α
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
U : Set α
hUo : IsOpen[inst_1] U
hμU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hUs : (μ : (a : Set α) → ℝ≥0∞) (U ∆ t) < ε
refine : (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε
⊢ ∃ (U : Set α),
    IsOpen[inst_1] U ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ (μ : (a : Set α) → ℝ≥0∞) (U ∆ s) < ε

Tactic:
refine ⟨U, hUo, hμU, ?_⟩