case intro.intro.intro
α : Type u_1
β : Type ?u.8664
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
r : ℝ≥0∞
hr : ↑↑μ A < r
U : Set α
hAU : U ⊇ toMeasurable μ A
hUo : IsOpen U
hU : ↑↑?m.8932 U < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U < r
α : Type u_1
β : Type ?u.8664
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
r : ℝ≥0∞
hr : ↑↑μ A < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U < r
rcases OuterRegular.outerRegular (measurableSet_toMeasurable μ A) r
    (by rwa [measure_toMeasurable]) with
  ⟨U, hAU, hUo, hU⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.8664
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
r : ℝ≥0∞
hr : ↑↑μ A < r
U : Set α
hAU : U ⊇ toMeasurable μ A
hUo : IsOpen U
hU : ↑↑?m.8932 U < r
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U < r
exact ⟨U, (subset_toMeasurable _ _).trans hAU, hUo, hU⟩
no goals
α : Type u_1
β : Type ?u.8664
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : OuterRegular μ
A : Set α
r : ℝ≥0∞
hr : ↑↑μ A < r
⊢ r > ↑↑μ (toMeasurable μ A)
rwa [measure_toMeasurable]