awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
hK_compact₁ : IsCompact K
⊢ IsClosed[inst] 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
-- 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 < HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) univ ≤ HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
hKμ.le

Premises used: LT.lt.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
hεr' : r - ε < r
K : Set 𝓧
left : K ⊆ univ
hKμ : r < HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)
hK_compact : IsCompact K
hK_closed : IsClosed[inst] K
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) univ ≤ HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set 𝓧) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
exact hKμ.le

Premises used: LT.lt.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 ≤ ε
⊢ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) ∅ᶜ ≤ ε

Tactic:
simpa
-- 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 ≤ ε
⊢ ∃ (K : Set 𝓧),
    IsCompact K ∧ ∀ (μ_1 : Measure 𝓧), Membership.mem (γ := Set (Measure 𝓧)) {μ} μ_1 → (μ_1 : (a : Set 𝓧) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
exact ⟨∅, isCompact_empty, by simpa⟩
-- 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
⊢ ε < 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⟩

Premises used: forall_eq, tsub_le_iff_right, add_comm, Set.mem_singleton_iff, lt_or_ge
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : T2Space 𝓧
inst_2 : OpensMeasurableSpace 𝓧
inst_3 : IsFiniteMeasure μ
h : μ.InnerRegular
⊢ IsTightMeasureSet (𝓧 := 𝓧) (m𝓧 := m𝓧) {μ}

Tactic:
isTightMeasureSet_singleton_of_innerRegularWRT ?_

Premises used: MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
inst : TopologicalSpace 𝓧
inst_1 : T2Space 𝓧
inst_2 : OpensMeasurableSpace 𝓧
inst_3 : IsFiniteMeasure μ
h : μ.InnerRegular
refine : μ.InnerRegularWRT (fun (s : Set 𝓧) ↦ IsCompact s ∧ IsClosed[inst] s) MeasurableSet
⊢ IsTightMeasureSet (𝓧 := 𝓧) (m𝓧 := m𝓧) {μ}

Tactic:
refine isTightMeasureSet_singleton_of_innerRegularWRT ?_

Premises used: MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
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
⊢ ∃ 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

Premises used: MeasureTheory.Measure.InnerRegular.innerRegular
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 : 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:
⟨K, hKs, ⟨hK_compact, hK_compact.isClosed⟩, hμK⟩

Premises used: And.intro, Exists.intro, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 : 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:
exact ⟨K, hKs, ⟨hK_compact, hK_compact.isClosed⟩, hμK⟩
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
α : Type u_3
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : IsCompletelyPseudoMetrizableSpace α
inst_3 : SecondCountableTopology α
inst_4 : BorelSpace α
μ : Measure α
inst_5 : IsFiniteMeasure μ
⊢ IsTightMeasureSet (𝓧 := α) (m𝓧 := inst) {μ}

Tactic:
isTightMeasureSet_singleton_of_innerRegularWRT
    (innerRegular_isCompact_isClosed_measurableSet_of_finite _)

Premises used: MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT, MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : CompactSpace 𝓧
simp : ∀ (s : Set ℝ≥0∞), Membership.mem (γ := Filter ℝ≥0∞) (𝓝 0) s → 0 ∈ s
⊢ IsTightMeasureSet S

Tactic:
simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot, tendsto_pure_left, iSup_apply,
    measure_empty, ENNReal.iSup_zero, ciSup_const]

Premises used: Filter.tendsto_pure_left, MeasureTheory.measure_empty, Filter.smallSets_bot, MeasureTheory.IsTightMeasureSet, ENNReal.iSup_zero, Filter.cocompact_eq_bot, ciSup_const, iSup_apply
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : CompactSpace 𝓧
⊢ ∀ (s : Set ℝ≥0∞), Membership.mem (γ := Filter ℝ≥0∞) (𝓝 0) s → 0 ∈ s

Tactic:
fun _ ↦ mem_of_mem_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
inst_1 : CompactSpace 𝓧
⊢ ∀ (s : Set ℝ≥0∞), Membership.mem (γ := Filter ℝ≥0∞) (𝓝 0) s → 0 ∈ s

Tactic:
exact fun _ ↦ mem_of_mem_nhds

Premises used: mem_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hT : IsTightMeasureSet T
hST : S ⊆ T
x : Set 𝓧
⊢ LE.le (α := (fun (a : Set 𝓧) ↦ ℝ≥0∞) x) 0 ((⨆ μ ∈ S, (⇑μ : (a : Set 𝓧) → ℝ≥0∞)) x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
rw :
  Tendsto (β := ℝ≥0∞) ((⨆ x ∈ S, (⇑x : (a : Set 𝓧) → ℝ≥0∞)) ⊔ ⨆ x ∈ T, (⇑x : (a : Set 𝓧) → ℝ≥0∞))
    (cocompact 𝓧).smallSets (𝓝 0)
⊢ IsTightMeasureSet (S ∪ T)

Tactic:
rw [IsTightMeasureSet, iSup_union]

Premises used: MeasureTheory.IsTightMeasureSet, iSup_union
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : Set 𝓧) ↦ max ((⨆ μ ∈ S, (⇑μ : (a : Set 𝓧) → ℝ≥0∞)) i) ((⨆ μ ∈ T, (⇑μ : (a : Set 𝓧) → ℝ≥0∞)) i))
    (cocompact 𝓧).smallSets (𝓝 (max 0 0))

Tactic:
Tendsto.sup_nhds hS hT

Premises used: Filter.Tendsto.sup_nhds
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
h : Eq (α := ℝ≥0∞) 0 (max 0 0)
⊢ Tendsto (β := ℝ≥0∞) ((⨆ x ∈ S, (⇑x : (a : Set 𝓧) → ℝ≥0∞)) ⊔ ⨆ x ∈ T, (⇑x : (a : Set 𝓧) → ℝ≥0∞))
    (cocompact 𝓧).smallSets (𝓝 0)

Tactic:
convert! Tendsto.sup_nhds hS hT

Premises used: Filter.Tendsto.sup_nhds
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S T : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ Eq (α := ℝ≥0∞) 0 (max 0 0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
S : Set (Measure 𝓧)
inst : TopologicalSpace 𝓧
hS : IsTightMeasureSet S
T : Set (Measure 𝓧)
⊢ IsTightMeasureSet (S ∩ T)

Tactic:
hS.subset inter_subset_left

Premises used: MeasureTheory.IsTightMeasureSet.subset, Set.inter_subset_left
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
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ᶜ ≤ ε
⊢ IsTightMeasureSet (m𝓧 := inst_2) (Measure.map f '' S)

Tactic:
rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le] at hS ⊢

Premises used: MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le
-- Module: Mathlib.MeasureTheory.Measure.Tight
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
simp :
  ∀ (ε : ℝ≥0∞),
    0 < ε → ∃ (K : Set 𝓨), IsCompact K ∧ ∀ a ∈ S, ((Measure.map f a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      ∃ (K : Set 𝓨),
        IsCompact K ∧
          ∀ (μ : Measure 𝓨),
            Membership.mem (γ := Set (Measure 𝓨)) (Measure.map f '' S) μ → (μ : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: and_imp, Set.mem_image, forall_exists_index, forall_apply_eq_imp_iff₂
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 < ε
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ᶜ ≤ ε
⊢ ∃ (K : Set 𝓨), IsCompact K ∧ ∀ a ∈ S, ((Measure.map f a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
obtain ⟨K, hK_compact, hKS⟩ := hS ε hε
-- Module: Mathlib.MeasureTheory.Measure.Tight
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ᶜ ≤ ε

Tactic:
⟨f '' K, hK_compact.image hf, fun μ hμS ↦ ?_⟩

Premises used: And.intro, Exists.intro, Set.image, IsCompact.image
-- Module: Mathlib.MeasureTheory.Measure.Tight
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ᶜ ≤ ε
refine : ∀ (μ : Measure 𝓧) (hμS : μ ∈ S), ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
⊢ ∃ (K : Set 𝓨), IsCompact K ∧ ∀ a ∈ S, ((Measure.map f a : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) Kᶜ ≤ ε

Tactic:
refine ⟨f '' K, hK_compact.image hf, fun μ hμS ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)ᶜ ≤ ε
neg : ∀ (hf_meas : ¬AEMeasurable f μ), ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε
⊢ ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε

Tactic:
by_cases hf_meas : AEMeasurable f μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)ᶜ ≤ ε

Tactic:
simp [Measure.map_of_not_aemeasurable hf_meas]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 μ
pos : (μ : (a : Set 𝓧) → ℝ≥0∞) (f ⁻¹' (f '' K)ᶜ) ≤ ε
⊢ ((Measure.map f μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) (f '' K)ᶜ ≤ ε

Tactic:
rw [Measure.map_apply_of_aemeasurable hf_meas (hK_compact.image hf).measurableSet.compl]

Premises used: MeasurableSet.compl, MeasureTheory.Measure.map_apply_of_aemeasurable, IsCompact.image, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Tight
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)ᶜ) ≤ ε

Tactic:
(measure_mono ?_).trans (hKS μ hμS)

Premises used: MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 μ
pos : f ⁻¹' (f '' K)ᶜ ⊆ Kᶜ
⊢ (μ : (a : Set 𝓧) → ℝ≥0∞) (f ⁻¹' (f '' K)ᶜ) ≤ ε

Tactic:
refine (measure_mono ?_).trans (hKS μ hμS)

Premises used: MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 μ
pos : K ⊆ f ⁻¹' f '' K
⊢ f ⁻¹' (f '' K)ᶜ ⊆ Kᶜ

Tactic:
simp only [preimage_compl, compl_subset_compl]

Premises used: Set.compl_subset_compl, Set.preimage_compl
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 μ
⊢ K ⊆ f ⁻¹' f '' K

Tactic:
subset_preimage_image f K

Premises used: Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.Measure.Tight
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 μ
⊢ K ⊆ f ⁻¹' f '' K

Tactic:
exact subset_preimage_image f K

Premises used: Set.subset_preimage_image
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0∞
hε : 0 < ε
hεbound : ε ≤ 1
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0∞
hε : 0 < ε
hεbound : ε ≤ 1
⊢ ε ≠ ∞

Tactic:
have εfin : ε ≠ ∞ := ne_top_of_le_ne_top (by simp) hεbound
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0∞
hε : 0 < ε
hεbound : ε ≤ 1
εfin : ε ≠ ∞
⊢ ε ≠ ∞

Tactic:
εfin
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0∞
hε : 0 < ε
hεbound : ε ≤ 1
εfin : ε ≠ ∞
lift :
  ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ≥0∞)) (hεbound : (↑ε : ℝ≥0∞) ≤ 1),
    ∃ (k : ℕ), ∀ μ ∈ S, 1 - (↑ε : ℝ≥0∞) < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)
⊢ ∃ (k : ℕ), ∀ μ ∈ S, 1 - ε < (↑((μ : (a : Set 𝓧) → ℝ≥0) (⋃ (i : ℕ), ⋃ (_ : i ≤ k), U i)) : ℝ≥0∞)

Tactic:
lift ε to ℝ≥0 using εfin
-- Module: Mathlib.MeasureTheory.Measure.Tight
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst : PseudoMetricSpace 𝓧
inst_1 : OpensMeasurableSpace 𝓧
inst_2 : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
U : ℕ → Set 𝓧
O : ∀ (i : ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
Cov : Eq.{u_1 + 1} (α := Set 𝓧) (⋃ (i : ℕ), U i) univ
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
ε : ℝ≥0
hε : 0 < (↑ε : ℝ≥0∞)
hεbound : (↑ε : ℝ≥0∞) ≤ 1
⊢ ∃ (ε' : ℝ) (hε' : 0 ≤ ε'), ε = NNReal.mk ε' hε'

Tactic:
⟨↑ε, ε.2, rfl⟩

Premises used: Exists.intro, NNReal.toReal, rfl, Subtype.property