case intro.intro.intro
α : Type u_1
β : Type ?u.67344
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ : Measure α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : Regular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKc : IsCompact K
hK : ↑↑μ A < ↑↑μ K + ε
⊢ ∃ K, K ⊆ A ∧ IsCompact K ∧ ↑↑μ (A \ K) < ε
α : Type u_1
β : Type ?u.67344
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ : Measure α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : Regular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ K, K ⊆ A ∧ IsCompact K ∧ ↑↑μ (A \ K) < ε
rcases hA.exists_isCompact_lt_add h'A hε with ⟨K, hKA, hKc, hK⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.67344
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
μ : Measure α
inst✝² : OpensMeasurableSpace α
inst✝¹ : T2Space α
inst✝ : Regular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
K : Set α
hKA : K ⊆ A
hKc : IsCompact K
hK : ↑↑μ A < ↑↑μ K + ε
⊢ ∃ K, K ⊆ A ∧ IsCompact K ∧ ↑↑μ (A \ K) < ε
exact
  ⟨K, hKA, hKc,
    measure_diff_lt_of_lt_add hKc.measurableSet hKA (ne_top_of_le_ne_top h'A <| measure_mono hKA)
      hK⟩