case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U = 0
⊢ ∃ K, K ⊆ U ∧ p K ∧ ↑↑μ U < ↑↑μ K + ε

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U ≠ 0
⊢ ∃ K, K ⊆ U ∧ p K ∧ ↑↑μ U < ↑↑μ K + ε
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
⊢ ∃ K, K ⊆ U ∧ p K ∧ ↑↑μ U < ↑↑μ K + ε
cases' eq_or_ne (μ U) 0 with h₀ h₀
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U = 0
⊢ ↑↑μ U < ↑↑μ ∅ + ε
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U = 0
⊢ ∃ K, K ⊆ U ∧ p K ∧ ↑↑μ U < ↑↑μ K + ε
refine' ⟨∅, empty_subset _, h0, _⟩
no goals
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U = 0
⊢ ↑↑μ U < ↑↑μ ∅ + ε
rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]
case inr.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U ≠ 0
K : Set α
hKU : K ⊆ U
hKc : p K
hrK : ↑↑μ U - ε < ↑↑μ K
⊢ ∃ K, K ⊆ U ∧ p K ∧ ↑↑μ U < ↑↑μ K + ε
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U ≠ 0
⊢ ∃ K, K ⊆ U ∧ p K ∧ ↑↑μ U < ↑↑μ K + ε
rcases H hU _ (ENNReal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩
no goals
case inr.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : InnerRegular μ p q
h0 : p ∅
hU : q U
hμU : ↑↑μ U ≠ ⊤
hε : ε ≠ 0
h₀ : ↑↑μ U ≠ 0
K : Set α
hKU : K ⊆ U
hKc : p K
hrK : ↑↑μ U - ε < ↑↑μ K
⊢ ∃ K, K ⊆ U ∧ p K ∧ ↑↑μ U < ↑↑μ K + ε
exact ⟨K, hKU, hKc, ENNReal.lt_add_of_sub_lt_right (Or.inl hμU) hrK⟩