case refine'_1
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤

case refine'_2
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (∃ U x, IsOpen U ∧ ↑↑μ U < ⊤) → ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤

case refine'_3
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, (∃ U x, IsOpen U ∧ ↑↑μ U < ⊤) → (∃ U x, IsOpen U ∧ ↑↑μ U < ⊤) → ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤

case refine'_4
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
refine' IsCompact.induction_on h _ _ _ _
case refine'_1
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∃ x, IsOpen ∅ ∧ ↑↑μ ∅ < ⊤
case refine'_1
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
use ∅
no goals
case refine'_1
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∃ x, IsOpen ∅ ∧ ↑↑μ ∅ < ⊤
simp [Superset]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ (x : α), x ∈ s✝ → FiniteAtFilter μ (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen U
hU : ↑↑μ U < ⊤
⊢ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
case refine'_2
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (∃ U x, IsOpen U ∧ ↑↑μ U < ⊤) → ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
rintro s t hst ⟨U, htU, hUo, hU⟩
no goals
case refine'_2.intro.intro.intro
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ (x : α), x ∈ s✝ → FiniteAtFilter μ (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen U
hU : ↑↑μ U < ⊤
⊢ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
exact ⟨U, hst.trans htU, hUo, hU⟩
case refine'_3.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ (x : α), x ∈ s✝ → FiniteAtFilter μ (𝓝 x)
s t U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hU : ↑↑μ U < ⊤
V : Set α
htV : V ⊇ t
hVo : IsOpen V
hV : ↑↑μ V < ⊤
⊢ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
case refine'_3
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, (∃ U x, IsOpen U ∧ ↑↑μ U < ⊤) → (∃ U x, IsOpen U ∧ ↑↑μ U < ⊤) → ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
rintro s t ⟨U, hsU, hUo, hU⟩ ⟨V, htV, hVo, hV⟩
no goals
case refine'_3.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ (x : α), x ∈ s✝ → FiniteAtFilter μ (𝓝 x)
s t U : Set α
hsU : U ⊇ s
hUo : IsOpen U
hU : ↑↑μ U < ⊤
V : Set α
htV : V ⊇ t
hVo : IsOpen V
hV : ↑↑μ V < ⊤
⊢ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
refine'
  ⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
    (measure_union_le _ _).trans_lt <| ENNReal.add_lt_top.2 ⟨hU, hV⟩⟩
case refine'_4
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
case refine'_4
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
⊢ ∀ (x : α), x ∈ s → ∃ t, t ∈ 𝓝[s] x ∧ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
intro x hx
case refine'_4.intro.intro.intro
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
x : α
hx✝ : x ∈ s
U : Set α
hU : ↑↑μ U < ⊤
hx : x ∈ U
hUo : IsOpen U
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
case refine'_4
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
rcases(hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩
no goals
case refine'_4.intro.intro.intro
α : Type u_1
β : Type ?u.3553252
γ : Type ?u.3553255
δ : Type ?u.3553258
ι : Type ?u.3553261
R : Type ?u.3553264
R' : Type ?u.3553267
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : MeasureTheory.Measure α
s : Set α
h : IsCompact s
hμ : ∀ (x : α), x ∈ s → FiniteAtFilter μ (𝓝 x)
x : α
hx✝ : x ∈ s
U : Set α
hU : ↑↑μ U < ⊤
hx : x ∈ U
hUo : IsOpen U
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∃ U x, IsOpen U ∧ ↑↑μ U < ⊤
exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩