awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
h : IsLindelof μ.supportᶜ
refine : ∀ (s : X) (hs : s ∈ μ.supportᶜ), ∃ t ∈ 𝓝[μ.supportᶜ] s, tᶜ ∈ ae μ
⊢ μ.support ∈ ae μ

Tactic:
refine compl_compl μ.support ▸ h.compl_mem_sets_of_nhdsWithin fun s hs ↦ ?_
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
h : IsLindelof μ.supportᶜ
s : X
hs : s ∈ μ.supportᶜ
⊢ ∃ t ∈ 𝓝[μ.supportᶜ] s, tᶜ ∈ ae μ

Tactic:
simpa [compl_mem_ae_iff, isOpen_compl_support.nhdsWithin_eq hs]
    using notMem_support_iff_exists.mp hs

Premises used: IsOpen.nhdsWithin_eq, MeasureTheory.Measure.notMem_support_iff_exists, Iff.mp, MeasureTheory.Measure.isOpen_compl_support, MeasureTheory.compl_mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : HereditarilyLindelofSpace X
⊢ μ.support ∈ ae μ

Tactic:
support_mem_ae_of_isLindelof <| HereditarilyLindelofSpace.isLindelof μ.supportᶜ

Premises used: MeasureTheory.Measure.support_mem_ae_of_isLindelof, Compl.compl, MeasureTheory.Measure.support, HereditarilyLindelofSpace.isLindelof
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : HereditarilyLindelofSpace X
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) μ.supportᶜ : ENNReal) (0 : ENNReal)

Tactic:
support_mem_ae

Premises used: Set.Mem, setOf, MeasureTheory.Measure.support_mem_ae
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : HereditarilyLindelofSpace X
⊢ NullMeasurableSet μ.supportᶜ μ

Tactic:
NullMeasurableSet.of_null measure_compl_support

Premises used: MeasureTheory.NullMeasurableSet.of_null, MeasureTheory.Measure.measure_compl_support
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : HereditarilyLindelofSpace X
⊢ NullMeasurableSet μ.support μ

Tactic:
NullMeasurableSet.compl_iff.mp nullMeasurableSet_compl_support

Premises used: MeasureTheory.NullMeasurableSet.compl_iff, Iff.mp, MeasureTheory.Measure.nullMeasurableSet_compl_support
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : HereditarilyLindelofSpace X
hμ : μ ≠ 0
⊢ μ.support.Nonempty

Tactic:
Nonempty.right <| nonempty_inter_support_of_pos <| measure_univ_pos.mpr hμ

Premises used: Iff.mpr, Set.Nonempty.right, MeasureTheory.Measure.measure_univ_pos, MeasureTheory.Measure.nonempty_inter_support_of_pos
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : HereditarilyLindelofSpace X
⊢ μ.support.Nonempty ↔ μ ≠ 0

Tactic:
⟨fun h e ↦ (not_nonempty_iff_eq_empty.mpr <| congrArg Measure.support e |>.trans
    <| support_zero) h, fun h ↦ nonempty_support h⟩

Premises used: Iff.mpr, congrArg, Set.not_nonempty_iff_eq_empty, MeasureTheory.Measure.nonempty_support, MeasureTheory.Measure.support, Iff.intro, MeasureTheory.Measure.support_zero, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : HereditarilyLindelofSpace X
⊢ μ.support = ∅ ↔ μ = 0

Tactic:
simp [← Set.not_nonempty_iff_eq_empty, not_congr nonempty_support_iff]

Premises used: MeasureTheory.Measure.nonempty_support_iff, Set.not_nonempty_iff_eq_empty, not_congr
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
rw :
  (∀ (i : Set X),
      x ∈ i ∧ IsOpen[inst] i →
        LT.lt (α := ENNReal) (0 : ENNReal) ((μ.restrict s : (a : Set X) → ENNReal) i : ENNReal)) ↔
    ∀ (i : Set X),
      x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) (i ∩ s) : ENNReal)
⊢ x ∈ (μ.restrict s).support ↔
    ∃ᶠ (u : Set X) in (𝓝[s] x).smallSets, LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) u : ENNReal)

Tactic:
rw [nhds_basis_opens x |>.mem_measureSupport,
    (nhdsWithin_basis_open x s).frequently_smallSets pos_mono]

Premises used: Filter.HasBasis.frequently_smallSets, MeasureTheory.pos_mono, nhds_basis_opens, Filter.HasBasis.mem_measureSupport
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
⊢ (∀ (i : Set X),
      x ∈ i ∧ IsOpen[inst] i →
        LT.lt (α := ENNReal) (0 : ENNReal) ((μ.restrict s : (a : Set X) → ENNReal) i : ENNReal)) ↔
    ∀ (i : Set X),
      x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) (i ∩ s) : ENNReal)

Tactic:
grind [IsOpen.measurableSet, restrict_apply]

Premises used: MeasureTheory.Measure.restrict_apply, IsOpen.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ : x ∈ μ.support
rw :
  ∀ (i : Set X),
    x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) (i ∩ s) : ENNReal)
⊢ x ∈ (μ.restrict s).support

Tactic:
rw [mem_support_restrict, (nhdsWithin_basis_open x s).frequently_smallSets pos_mono]

Premises used: Filter.HasBasis.frequently_smallSets, MeasureTheory.pos_mono, MeasureTheory.Measure.mem_support_restrict
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ : x ∈ μ.support
⊢ ∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)

Tactic:
rw [(nhds_basis_opens x).mem_measureSupport] at hxμ

Premises used: nhds_basis_opens, Filter.HasBasis.mem_measureSupport
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ :
  ∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)
u : Set X
hxu : x ∈ u
hu : IsOpen[inst] u
apply :
  LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) (u ∩ interior s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (u ∩ s) : ENNReal)
⊢ LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) (u ∩ s) : ENNReal)

Tactic:
apply hxμ (u ∩ interior s) ⟨⟨hxu, hxs⟩, hu.inter isOpen_interior⟩ |>.trans_le

Premises used: isOpen_interior, Inter.inter, LT.lt.trans_le, And.intro, interior, IsOpen.inter
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ :
  ∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)
u : Set X
hxu : x ∈ u
hu : IsOpen[inst] u
h : interior s ⊆ s
⊢ LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) (u ∩ interior s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (u ∩ s) : ENNReal)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ :
  ∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)
u : Set X
hxu : x ∈ u
hu : IsOpen[inst] u
⊢ interior s ⊆ s

Tactic:
interior_subset

Premises used: interior_subset
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
hxs : x ∈ interior s
hxμ :
  ∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) i : ENNReal)
u : Set X
hxu : x ∈ u
hu : IsOpen[inst] u
⊢ interior s ⊆ s

Tactic:
exact interior_subset

Premises used: interior_subset
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
⊢ (μ.restrict s).support ⊆ closure[inst] s ∩ μ.support

Tactic:
Set.subset_inter (support_subset_of_isClosed isClosed_closure ?_)
    (support_mono restrict_le_self)

Premises used: MeasureTheory.Measure.support_mono, Set.subset_inter, MeasureTheory.Measure.restrict_le_self, isClosed_closure, MeasureTheory.Measure.support_subset_of_isClosed
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
refine : closure[inst] s ∈ ae (μ.restrict s)
⊢ (μ.restrict s).support ⊆ closure[inst] s ∩ μ.support

Tactic:
refine Set.subset_inter (support_subset_of_isClosed isClosed_closure ?_)
    (support_mono restrict_le_self)

Premises used: MeasureTheory.Measure.support_mono, Set.subset_inter, MeasureTheory.Measure.restrict_le_self, isClosed_closure, MeasureTheory.Measure.support_subset_of_isClosed
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
rw : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) ((closure[inst] s)ᶜ ∩ s) : ENNReal) (0 : ENNReal)
⊢ closure[inst] s ∈ ae (μ.restrict s)

Tactic:
rw [mem_ae_iff, μ.restrict_apply isClosed_closure.isOpen_compl.measurableSet]

Premises used: IsClosed.isOpen_compl, MeasureTheory.Measure.restrict_apply, IsOpen.measurableSet, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
⊢ μ.measureOf ∅ = 0

Tactic:
μ.empty

Premises used: MeasureTheory.OuterMeasure.empty, MeasureTheory.Measure.toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
h : (closure[inst] s)ᶜ ∩ s = ∅
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) ((closure[inst] s)ᶜ ∩ s) : ENNReal) (0 : ENNReal)

Tactic:
convert! μ.empty

Premises used: MeasureTheory.OuterMeasure.empty, MeasureTheory.Measure.toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
⊢ (closure[inst] s)ᶜ ∩ s = ∅

Tactic:
subset_closure.disjoint_compl_left.eq_bot

Premises used: subset_closure, HasSubset.Subset.disjoint_compl_left, Disjoint.eq_bot
-- Module: Mathlib.MeasureTheory.Measure.Support
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
⊢ (closure[inst] s)ᶜ ∩ s = ∅

Tactic:
exact subset_closure.disjoint_compl_left.eq_bot

Premises used: subset_closure, HasSubset.Subset.disjoint_compl_left, Disjoint.eq_bot
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
simp :
  (∀ (ε : ℝ≥0∞),
      0 < ε →
        ∃ (s : Set 𝓧),
          (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧
            ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ IsTightMeasureSet S ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
simp only [IsTightMeasureSet, ENNReal.tendsto_nhds ENNReal.zero_ne_top, gt_iff_lt, zero_add,
    iSup_apply, mem_Icc, tsub_le_iff_right, zero_le, iSup_le_iff, true_and, eventually_smallSets,
    mem_cocompact]

Premises used: zero_le, ENNReal.zero_ne_top, Filter.eventually_smallSets, zero_add, tsub_le_iff_right, MeasureTheory.IsTightMeasureSet, ENNReal.tendsto_nhds, gt_iff_lt, Set.mem_Icc, iSup_le_iff, iSup_apply, true_and, Filter.mem_cocompact
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
refine_1 :
  ∀
    (h :
      ∀ (ε : ℝ≥0∞),
        0 < ε →
          ∃ (s : Set 𝓧),
            (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧
              ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε)
    (ε : ℝ≥0∞) (hε : 0 < ε), ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
refine_2 :
  ∀ (h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε) (ε : ℝ≥0∞)
    (hε : 0 < ε),
    ∃ (s : Set 𝓧),
      (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
⊢ (∀ (ε : ℝ≥0∞),
      0 < ε →
        ∃ (s : Set 𝓧),
          (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧
            ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (s : Set 𝓧),
        (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
refine_1 :
  ∀ (A : Set 𝓧) (hA : ∀ t ⊆ A, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε) (K : Set 𝓧)
    (h1 : IsCompact K) (h2 : Kᶜ ⊆ A), ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
obtain ⟨A, ⟨K, h1, h2⟩, hA⟩ := h ε hε
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (s : Set 𝓧),
        (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
A : Set 𝓧
hA : ∀ t ⊆ A, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
K : Set 𝓧
h1 : IsCompact K
h2 : Kᶜ ⊆ A
⊢ ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
⟨K, h1, hA Kᶜ h2⟩

Premises used: Compl.compl, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (s : Set 𝓧),
        (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
A : Set 𝓧
hA : ∀ t ⊆ A, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
K : Set 𝓧
h1 : IsCompact K
h2 : Kᶜ ⊆ A
⊢ ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
exact ⟨K, h1, hA Kᶜ h2⟩
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
refine_2 :
  ∀ (K : Set 𝓧) (h1 : IsCompact K) (h2 : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε),
    ∃ (s : Set 𝓧),
      (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
⊢ ∃ (s : Set 𝓧),
    (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε

Tactic:
obtain ⟨K, h1, h2⟩ := h ε hε
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
h1 : IsCompact K
h2 : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∃ (s : Set 𝓧),
    (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε

Tactic:
⟨Kᶜ, ⟨K, h1, subset_rfl⟩, fun A hA μ hμS ↦ (μ.mono hA).trans (h2 μ hμS)⟩

Premises used: Compl.compl, MeasureTheory.OuterMeasure.mono, MeasureTheory.Measure.toOuterMeasure, And.intro, Exists.intro, LE.le.trans, subset_rfl
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
h1 : IsCompact K
h2 : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∃ (s : Set 𝓧),
    (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε

Tactic:
exact ⟨Kᶜ, ⟨K, h1, subset_rfl⟩, fun A hA μ hμS ↦ (μ.mono hA).trans (h2 μ hμS)⟩
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
rw :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ IsTightMeasureSet (𝓧 := 𝓧) (m𝓧 := m𝓧) {μ}

Tactic:
rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le]

Premises used: MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
⊢ r - ε < r

Tactic:
have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) hεr.ne_bot hε.ne'
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
hεr' : r - ε < r
inl :
  ∀ K ⊆ univ,
    ∀ (hKμ : r - ε < (μ : (a : Set 𝓧) → ℝ≥0∞) K) (hK_compact : IsCompact K) (hK_closed : IsClosed[inst] K),
      ∃ (K : Set 𝓧),
        IsCompact K ∧
          ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
obtain ⟨K, _, ⟨hK_compact, hK_closed⟩, hKμ⟩ := h .univ (r - ε) hεr'

Premises used: HSub.hSub, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
hεr' : r - ε < r
K : Set 𝓧
left : K ⊆ univ
hKμ : r - ε < (μ : (a : Set 𝓧) → ℝ≥0∞) K
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
⟨K, hK_compact, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
hεr' : r - ε < r
K : Set 𝓧
left : K ⊆ univ
hKμ : r - ε < (μ : (a : Set 𝓧) → ℝ≥0∞) K
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
inl : ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
refine ⟨K, hK_compact, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
hεr' : r - ε < r
K : Set 𝓧
left : K ⊆ univ
hKμ : r - ε < (μ : (a : Set 𝓧) → ℝ≥0∞) K
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
inl : (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
simp only [mem_singleton_iff, forall_eq]

Premises used: forall_eq, Set.mem_singleton_iff
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
hεr' : r - ε < r
K : Set 𝓧
left : K ⊆ univ
hKμ : r - ε < (μ : (a : Set 𝓧) → ℝ≥0∞) K
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
inl : (μ : (a : Set 𝓧) → ℝ≥0∞) univ ≤ HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
rw [measure_compl hK_closed.measurableSet (measure_ne_top μ _), tsub_le_iff_right]

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_ne_top, IsClosed.measurableSet, tsub_le_iff_right
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
hεr' : r - ε < r
K : Set 𝓧
left : K ⊆ univ
hKμ : r - ε < (μ : (a : Set 𝓧) → ℝ≥0∞) K
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
⊢ r < HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ

Premises used: LT.lt.le, add_comm, ENNReal.sub_lt_iff_lt_right, ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := (μ : (a : Set 𝓧) → ℝ≥0∞) univ
hεr : ε < r
hεr' : r - ε < r
K : Set 𝓧
left : K ⊆ univ
hKμ : r - ε < (μ : (a : Set 𝓧) → ℝ≥0∞) K
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
hKμ₁ : r < HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)
⊢ IsCompact K

Tactic:
rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ

Premises used: LT.lt.le, add_comm, ENNReal.sub_lt_iff_lt_right, ne_top_of_lt