case inl
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
H : ↑↑μ A = ⊤
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U ≤ ↑↑μ A + ε

case inr
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
H : ↑↑μ A ≠ ⊤
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U ≤ ↑↑μ A + ε
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U ≤ ↑↑μ A + ε
rcases eq_or_ne (μ A) ∞ with (H | H)
no goals
case inl
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
H : ↑↑μ A = ⊤
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U ≤ ↑↑μ A + ε
exact ⟨univ, subset_univ _, isOpen_univ, by simp only [H, _root_.top_add, le_top]⟩
no goals
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
H : ↑↑μ A = ⊤
⊢ ↑↑μ univ ≤ ↑↑μ A + ε
simp only [H, _root_.top_add, le_top]
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
H : ↑↑μ A ≠ ⊤
U : Set α
AU : U ⊇ A
U_open : IsOpen U
hU : ↑↑μ U < ↑↑μ A + ε
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U ≤ ↑↑μ A + ε
case inr
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
H : ↑↑μ A ≠ ⊤
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U ≤ ↑↑μ A + ε
rcases A.exists_isOpen_lt_add H hε with ⟨U, AU, U_open, hU⟩
no goals
case inr.intro.intro.intro
α : Type u_1
β : Type ?u.11634
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ✝ : Measure α
A : Set α
μ : Measure α
inst✝ : OuterRegular μ
ε : ℝ≥0∞
hε : ε ≠ 0
H : ↑↑μ A ≠ ⊤
U : Set α
AU : U ⊇ A
U_open : IsOpen U
hU : ↑↑μ U < ↑↑μ A + ε
⊢ ∃ U, U ⊇ A ∧ IsOpen U ∧ ↑↑μ U ≤ ↑↑μ A + ε
exact ⟨U, AU, U_open, hU.le⟩