awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
h : μ.support = μ.supportᶜᶜ
⊢ μ.support =
    ⋂₀ {t : Set X | IsClosed[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) tᶜ : ENNReal) (0 : ENNReal)}
have h₁ : Eq.{u_1 + 1} (α := Set X)
  (⋂₀ {t : Set X | IsClosed[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) tᶜ : ENNReal) (0 : ENNReal)})
  (⋃₀ {t : Set X | IsOpen[inst] t ∧ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) t : ENNReal) (0 : ENNReal)})ᶜ
Tactic: convert! congr($(compl_support_eq_sUnion (μ := μ))ᶜ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
h : IsLindelof μ.supportᶜ
⊢ μ.support ∈ ae μ
have refine : ∀ (s : X) (hs : s ∈ μ.supportᶜ), ∃ t ∈ 𝓝[μ.supportᶜ] s, tᶜ ∈ ae μ
Tactic: refine compl_compl μ.support ▸ h.compl_mem_sets_of_nhdsWithin fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
x : X
⊢ x ∈ (μ.restrict s).support ↔
    ∃ᶠ (u : Set X) in (𝓝[s] x).smallSets, LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) u : ENNReal)
have 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)
Tactic: rw [nhds_basis_opens x |>.mem_measureSupport,
    (nhdsWithin_basis_open x s).frequently_smallSets pos_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
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
⊢ x ∈ (μ.restrict s).support
have rw : ∀ (i : Set X),
  x ∈ i ∧ IsOpen[inst] i → LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) (i ∩ s) : ENNReal)
Tactic: rw [mem_support_restrict, (nhdsWithin_basis_open x s).frequently_smallSets pos_mono]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (hypothesis)
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 ∩ s) : ENNReal)
have hxμ₁ : ∀ (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μ
Cleared hypotheses: hxμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
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
⊢ LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) (u ∩ s) : ENNReal)
have apply : LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) (u ∩ interior s) : ENNReal)
  ((μ : (a : Set X) → ENNReal) (u ∩ s) : ENNReal)
Tactic: apply hxμ (u ∩ interior s) ⟨⟨hxu, hxs⟩, hu.inter isOpen_interior⟩ |>.trans_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
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
⊢ LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) (u ∩ interior s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) (u ∩ s) : ENNReal)
have h : interior s ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
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
have refine : closure[inst] s ∈ ae (μ.restrict s)
Tactic: refine Set.subset_inter (support_subset_of_isClosed isClosed_closure ?_)
    (support_mono restrict_le_self)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
⊢ closure[inst] s ∈ ae (μ.restrict s)
have rw : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) ((closure[inst] s)ᶜ ∩ s) : ENNReal) (0 : ENNReal)
Tactic: rw [mem_ae_iff, μ.restrict_apply isClosed_closure.isOpen_compl.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Support (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : OpensMeasurableSpace X
s : Set X
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) ((closure[inst] s)ᶜ ∩ s) : ENNReal) (0 : ENNReal)
have h : (closure[inst] s)ᶜ ∩ s = ∅
Tactic: convert! μ.empty
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
⊢ IsTightMeasureSet S ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have 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ᶜ ≤ ε
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
⊢ (∀ (ε : ℝ≥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ᶜ ≤ ε
have 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ᶜ ≤ ε
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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ᶜ ≤ ε
⊢ (∀ (ε : ℝ≥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ᶜ ≤ ε
have 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 ≤ ε
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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 < ε
⊢ ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have 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ᶜ ≤ ε
Tactic: obtain ⟨A, ⟨K, h1, h2⟩, hA⟩ := h ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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 < ε
⊢ ∃ (s : Set 𝓧),
    (∃ (t : Set 𝓧), IsCompact t ∧ tᶜ ⊆ s) ∧ ∀ t ⊆ s, ∀ (i : Measure 𝓧) (i_1 : i ∈ S), (i : (a : Set 𝓧) → ℝ≥0∞) t ≤ ε
have 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 ≤ ε
Tactic: obtain ⟨K, h1, h2⟩ := h ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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
⊢ IsTightMeasureSet (𝓧 := 𝓧) (m𝓧 := m𝓧) {μ}
have rw : ∀ (ε : ℝ≥0∞),
  0 < ε →
    ∃ (K : Set 𝓧),
      IsCompact K ∧
        ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
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
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have hεr' : r - ε < r
Tactic: have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) hεr.ne_bot hε.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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 𝓧),
    IsCompact K ∧ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have 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ᶜ ≤ ε
Tactic: obtain ⟨K, _, ⟨hK_compact, hK_closed⟩, hKμ⟩ := h .univ (r - ε) hεr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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ᶜ ≤ ε
have inl : ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: refine ⟨K, hK_compact, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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
⊢ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inl : (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: simp only [mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
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
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have inl : (μ : (a : Set 𝓧) → ℝ≥0∞) univ ≤ HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: rw [measure_compl hK_closed.measurableSet (measure_ne_top μ _), tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
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
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) univ ≤ HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)
have hKμ₁ : 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μ
Cleared hypotheses: hKμ, hK_compact, hK_closed
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (hypothesis)
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
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
have x : ε < r ∨ r ≤ ε
Tactic: cases lt_or_ge ε r with
  | inl hεr =>
    have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) hεr.ne_bot hε.ne'
    obtain ⟨K, _, ⟨hK_compact, hK_closed⟩, hKμ⟩ := h .univ (r - ε) hεr'
    refine ⟨K, hK_compact, ?_⟩
    simp only [mem_singleton_iff, forall_eq]
    rw [measure_compl hK_closed.measurableSet (measure_ne_top μ _), tsub_le_iff_right]
    rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ
    exact hKμ.le
  | inr hεr => exact ⟨∅, isCompact_empty, by simpa⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : T2Space 𝓧
inst_2 : OpensMeasurableSpace 𝓧
inst_3 : IsFiniteMeasure μ
h : μ.InnerRegular
⊢ IsTightMeasureSet (𝓧 := 𝓧) (m𝓧 := m𝓧) {μ}
have refine : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
Tactic: refine isTightMeasureSet_singleton_of_innerRegularWRT ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : T2Space 𝓧
inst_2 : OpensMeasurableSpace 𝓧
inst_3 : IsFiniteMeasure μ
h : μ.InnerRegular
s : Set 𝓧
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (μ : (a : Set 𝓧) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) K ∧ r < (μ : (a : Set 𝓧) → ℝ≥0∞) K
have obtain : ∀ (K : Set 𝓧) (hKs : K ⊆ s) (hK_compact : IsCompact K) (hμK : r < (μ : (a : Set 𝓧) → ℝ≥0∞) K),
  ∃ K ⊆ s, (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) K ∧ r < (μ : (a : Set 𝓧) → ℝ≥0∞) K
Tactic: obtain ⟨K, hKs, hK_compact, hμK⟩ := h.innerRegular hs r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : CompactSpace 𝓧
⊢ IsTightMeasureSet S
have simp : ∀ (s : Set ℝ≥0∞), Membership.mem (γ := Filter ℝ≥0∞) (𝓝 0) s → 0 ∈ s
Tactic: simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot, tendsto_pure_left, iSup_apply,
    measure_empty, ENNReal.iSup_zero, ciSup_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ IsTightMeasureSet (S ∪ T)
have rw : Tendsto (β := ℝ≥0∞) ((⨆ x ∈ S, (⇑x : (a : Set 𝓧) → ℝ≥0∞)) ⊔ ⨆ x ∈ T, (⇑x : (a : Set 𝓧) → ℝ≥0∞)) (cocompact 𝓧).smallSets
  (𝓝 0)
Tactic: rw [IsTightMeasureSet, iSup_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ Tendsto (β := ℝ≥0∞) ((⨆ x ∈ S, (⇑x : (a : Set 𝓧) → ℝ≥0∞)) ⊔ ⨆ x ∈ T, (⇑x : (a : Set 𝓧) → ℝ≥0∞))
    (cocompact 𝓧).smallSets (𝓝 0)
have h : Eq (α := ℝ≥0∞) 0 (max 0 0)
Tactic: convert! Tendsto.sup_nhds hS hT
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : IsTightMeasureSet S
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
⊢ IsTightMeasureSet (m𝓧 := inst_2) (Measure.map f '' S)
have rw : ∀ (hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε) {f : 𝓧 → 𝓨}
  (hf : Continuous[inst, inst_1] f) (ε : ℝ≥0∞),
  0 < ε →
    ∃ (K : Set 𝓨),
      IsCompact K ∧
        ∀ (μ : Measure 𝓨),
          Membership.mem (γ := Set (Measure 𝓨)) (Measure.map f '' S) μ → (μ : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le] at hS ⊢
Cleared hypotheses: hS, f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓨),
        IsCompact K ∧
          ∀ (μ : Measure 𝓨),
            Membership.mem (γ := Set (Measure 𝓨)) (Measure.map f '' S) μ → (μ : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε
have simp : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓨), IsCompact K ∧ ∀ a ∈ S, ((Measure.map f a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (K : Set 𝓨), IsCompact K ∧ ∀ a ∈ S, ((Measure.map f a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε
have obtain : ∀ (K : Set 𝓧) (hK_compact : IsCompact K) (hKS : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε),
  ∃ (K : Set 𝓨), IsCompact K ∧ ∀ a ∈ S, ((Measure.map f a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε
Tactic: obtain ⟨K, hK_compact, hKS⟩ := hS ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∃ (K : Set 𝓨), IsCompact K ∧ ∀ a ∈ S, ((Measure.map f a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε
have refine : ∀ (μ : Measure 𝓧) (hμS : μ ∈ S), ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
Tactic: refine ⟨f '' K, hK_compact.image hf, fun μ hμS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
⊢ ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
have pos : ∀ (hf_meas : AEMeasurable f μ), ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
Tactic: by_cases hf_meas : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
pos : ∀ (hf_meas : AEMeasurable f μ), ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
⊢ ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
have neg : ∀ (hf_meas : ¬AEMeasurable f μ), ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
Tactic: by_cases hf_meas : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
have pos : (μ : (a : Set 𝓧) → ℝ≥0∞) (f ⁻¹' (f '' K)ᶜ) ≤ ε
Tactic: rw [Measure.map_apply_of_aemeasurable hf_meas (hK_compact.image hf).measurableSet.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tight (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : TopologicalSpace 𝓨
inst_2 : MeasurableSpace 𝓨
inst_3 : OpensMeasurableSpace 𝓨
inst_4 : T2Space 𝓨
hS : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (K : Set 𝓧), IsCompact K ∧ ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
f : 𝓧 → 𝓨
hf : Continuous[inst, inst_1] f
ε : ℝ≥0∞
hε : 0 < ε
K : Set 𝓧
hK_compact : IsCompact K
hKS : ∀ μ ∈ S, (μ : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε
μ : Measure 𝓧
hμS : μ ∈ S
hf_meas : AEMeasurable f μ
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) (f ⁻¹' (f '' K)ᶜ) ≤ ε
have pos : f ⁻¹' (f '' K)ᶜ ⊆ Kᶜ
Tactic: refine (measure_mono ?_).trans (hKS μ hμS)