case intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s✝ : Set α
ε r✝ : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
r : ℝ≥0∞
hr : r < ↑↑μ s
⊢ ∃ K, K ⊆ s ∧ p K ∧ r < ↑↑μ K
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s : Set α
ε r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
⊢ InnerRegular μ p fun s => MeasurableSet s ∧ ↑↑μ s ≠ ⊤
rintro s ⟨hs, hμs⟩ r hr
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
case intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s✝ : Set α
ε r✝ : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
r : ℝ≥0∞
hr : r < ↑↑μ s
⊢ ∃ K, K ⊆ s ∧ p K ∧ r < ↑↑μ K
obtain ⟨ε, hε, hεs, rfl⟩ : ∃ (ε : _)(_ : ε ≠ 0), ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
  use (μ s - r) / 2
  simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, le_add_right]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
rcases hs.exists_isOpen_diff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hsU' : U' ⊇ U \ s
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
rcases (U \ s).exists_isOpen_lt_of_lt _ hμU with ⟨U', hsU', hU'o, hμU'⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hsU' : U' ⊇ U \ s
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
replace hsU' := diff_subset_comm.1 hsU'
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
rcases H.exists_subset_lt_add h0 hUo hUt.ne hε with ⟨K, hKU, hKc, hKr⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ↑↑μ s < ↑↑μ (K \ U') + (ε + ε)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ∃ K, K ⊆ s ∧ p K ∧ ↑↑μ s - (ε + ε) < ↑↑μ K
refine' ⟨K \ U', fun x hx => hsU' ⟨hKU hx.1, hx.2⟩, hd hKc hU'o, ENNReal.sub_lt_of_lt_add hεs _⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ↑↑μ s < ↑↑μ (K \ U') + (ε + ε)
calc
  μ s ≤ μ U := μ.mono hsU
  _ < μ K + ε := hKr
  _ ≤ μ (K \ U') + μ U' + ε := (add_le_add_right (tsub_le_iff_right.1 le_measure_diff) _)
  _ ≤ μ (K \ U') + ε + ε := by
    apply add_le_add_right; apply add_le_add_left
    exact hμU'.le
  _ = μ (K \ U') + (ε + ε) := add_assoc _ _ _
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s✝ : Set α
ε r✝ : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
r : ℝ≥0∞
hr : r < ↑↑μ s
⊢ ∃ x, (↑↑μ s - r) / 2 + (↑↑μ s - r) / 2 ≤ ↑↑μ s ∧ r = ↑↑μ s - ((↑↑μ s - r) / 2 + (↑↑μ s - r) / 2)
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s✝ : Set α
ε r✝ : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
r : ℝ≥0∞
hr : r < ↑↑μ s
⊢ ∃ ε x, ε + ε ≤ ↑↑μ s ∧ r = ↑↑μ s - (ε + ε)
use (μ s - r) / 2
no goals
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U s✝ : Set α
ε r✝ : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
r : ℝ≥0∞
hr : r < ↑↑μ s
⊢ ∃ x, (↑↑μ s - r) / 2 + (↑↑μ s - r) / 2 ≤ ↑↑μ s ∧ r = ↑↑μ s - ((↑↑μ s - r) / 2 + (↑↑μ s - r) / 2)
simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, le_add_right]
case bc
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ↑↑μ (K \ U') + ↑↑μ U' ≤ ↑↑μ (K \ U') + ε
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ↑↑μ (K \ U') + ↑↑μ U' + ε ≤ ↑↑μ (K \ U') + ε + ε
apply add_le_add_right
case bc.bc
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ↑↑μ U' ≤ ε
case bc
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ↑↑μ (K \ U') + ↑↑μ U' ≤ ↑↑μ (K \ U') + ε
apply add_le_add_left
no goals
case bc.bc
α : Type u_1
β : Type ?u.35639
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
p q : Set α → Prop
U✝ s✝ : Set α
ε✝ r : ℝ≥0∞
inst✝ : OuterRegular μ
H : InnerRegular μ p IsOpen
h0 : p ∅
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
ε : ℝ≥0∞
hεs : ε + ε ≤ ↑↑μ s
hr : ↑↑μ s - (ε + ε) < ↑↑μ s
hε : ε ≠ 0
U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hUt : ↑↑μ U < ⊤
hμU : ↑↑μ (U \ s) < ε
U' : Set α
hU'o : IsOpen U'
hμU' : ↑↑μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : ↑↑μ U < ↑↑μ K + ε
⊢ ↑↑μ U' ≤ ε
exact hμU'.le