-- Mathlib/MeasureTheory/Measure/Tight.lean
theorem isTightMeasureSet_singleton_of_innerRegularWRT [OpensMeasurableSpace α] [IsFiniteMeasure μ]
    (h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet) :
    IsTightMeasureSet {μ}

Proof state:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r < ε + μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ μ univ ≤ ε + μ K

Tactic:
exact hKμ.le

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
intro ε hε

Result:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
let r := μ Set.univ

Result:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Proof state:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
simp only [mem_singleton_iff, forall_eq]

Result:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ μ Kᶜ ≤ ε

Proof state:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ μ Kᶜ ≤ ε

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

Result:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ μ univ ≤ ε + μ K

Proof state:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
refine ⟨K, hK_compact, ?_⟩

Result:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Proof state:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) (zero_le'.trans_lt hεr).ne'
  hε.ne'

Result:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Proof state:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

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

Result:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε ≥ r
⊢ ∀ μ_1 ∈ {μ}, μ_1 ∅ᶜ ≤ ε

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
⊢ IsTightMeasureSet {μ}

Tactic:
rw [IsTightMeasureSet_iff_exists_isCompact_measure_compl_le]

Result:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
⊢ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Proof state:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε ≥ r
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
exact ⟨∅, isCompact_empty, by simpa⟩

Result:
no goals