case intro.intro.intro
α : Type u_1
β : Type ?u.75620
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFA : F ⊆ A
hFc : IsClosed F
hF : ↑↑μ A < ↑↑μ F + ε
⊢ ∃ F, F ⊆ A ∧ IsClosed F ∧ ↑↑μ (A \ F) < ε
α : Type u_1
β : Type ?u.75620
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ F, F ⊆ A ∧ IsClosed F ∧ ↑↑μ (A \ F) < ε
rcases hA.exists_isClosed_lt_add h'A hε with ⟨F, hFA, hFc, hF⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.75620
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : WeaklyRegular μ
A : Set α
hA : MeasurableSet A
h'A : ↑↑μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFA : F ⊆ A
hFc : IsClosed F
hF : ↑↑μ A < ↑↑μ F + ε
⊢ ∃ F, F ⊆ A ∧ IsClosed F ∧ ↑↑μ (A \ F) < ε
exact
  ⟨F, hFA, hFc,
    measure_diff_lt_of_lt_add hFc.measurableSet hFA (ne_top_of_le_ne_top h'A <| measure_mono hFA)
      hF⟩