case intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.141263
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
K : Set α
hK : IsCompact K
K' : Set α
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.141263
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
K : Set α
hK : IsCompact K
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
rcases exists_compact_superset hK with ⟨K', hK', hKK'⟩
no goals
case intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
γ : Type ?u.141263
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : T2Space α
K : Set α
hK : IsCompact K
K' : Set α
hK' : IsCompact K'
hKK' : K ⊆ interior K'
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
refine'
  ⟨interior K', isOpen_interior, hKK', isCompact_closure_of_subset_compact hK' interior_subset⟩