-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem exists_open_superset_measure_lt_top' (h : IsCompact s)
    (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)) : ∃ U ⊇ s, IsOpen U ∧ μ U < ∞

Proof state:
case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen U ∧ μ U < ⊤

Tactic:
rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩

Result:
case refine_4.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx✝ : x ∈ s
U : Set α
hU : μ U < ⊤
hx : x ∈ U
hUo : IsOpen U
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen U ∧ μ U < ⊤

Proof state:
case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen U ∧ μ U < ⊤

Tactic:
intro x hx

Result:
case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen U ∧ μ U < ⊤

Proof state:
case refine_4.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx✝ : x ∈ s
U : Set α
hU : μ U < ⊤
hx : x ∈ U
hUo : IsOpen U
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen U ∧ μ U < ⊤

Tactic:
exact ⟨U, nhdsWithin_le_nhds (hUo.mem_nhds hx), U, Subset.rfl, hUo, hU⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ s, IsOpen U ∧ μ U < ⊤

Tactic:
refine IsCompact.induction_on h ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ ∅, IsOpen U ∧ μ U < ⊤

case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (∃ U ⊇ t, IsOpen U ∧ μ U < ⊤) → ∃ U ⊇ s, IsOpen U ∧ μ U < ⊤

case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, (∃ U ⊇ s, IsOpen U ∧ μ U < ⊤) → (∃ U ⊇ t, IsOpen U ∧ μ U < ⊤) → ∃ U ⊇ s ∪ t, IsOpen U ∧ μ U < ⊤

case refine_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen U ∧ μ U < ⊤

Proof state:
case refine_2
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, s ⊆ t → (∃ U ⊇ t, IsOpen U ∧ μ U < ⊤) → ∃ U ⊇ s, IsOpen U ∧ μ U < ⊤

Tactic:
rintro s t hst ⟨U, htU, hUo, hU⟩

Result:
case refine_2.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ x ∈ s✝, μ.FiniteAtFilter (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen U
hU : μ U < ⊤
⊢ ∃ U ⊇ s, IsOpen U ∧ μ U < ⊤

Proof state:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∅ ⊇ ∅ ∧ IsOpen ∅ ∧ μ ∅ < ⊤

Tactic:
simp [Superset]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∀ ⦃s t : Set α⦄, (∃ U ⊇ s, IsOpen U ∧ μ U < ⊤) → (∃ U ⊇ t, IsOpen U ∧ μ U < ⊤) → ∃ U ⊇ s ∪ t, IsOpen U ∧ μ U < ⊤

Tactic:
rintro s t ⟨U, hsU, hUo, hU⟩ ⟨V, htV, hVo, hV⟩

Result:
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ 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 ⊇ s ∪ t, IsOpen U ∧ μ U < ⊤

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ x ∈ s✝, μ.FiniteAtFilter (𝓝 x)
s t : Set α
hst : s ⊆ t
U : Set α
htU : U ⊇ t
hUo : IsOpen U
hU : μ U < ⊤
⊢ ∃ U ⊇ s, IsOpen U ∧ μ U < ⊤

Tactic:
exact ⟨U, hst.trans htU, hUo, hU⟩

Result:
no goals

Proof state:
case refine_3.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s✝ : Set α
h : IsCompact s✝
hμ : ∀ 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 ⊇ s ∪ t, IsOpen U ∧ μ U < ⊤

Tactic:
refine
  ⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
    (measure_union_le _ _).trans_lt <| ENNReal.add_lt_top.2 ⟨hU, hV⟩⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ ∅, IsOpen U ∧ μ U < ⊤

Tactic:
use ∅

Result:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∅ ⊇ ∅ ∧ IsOpen ∅ ∧ μ ∅ < ⊤