-- Mathlib/Topology/Separation/Regular.lean
theorem exists_open_between_and_isCompact_closure [LocallyCompactSpace X] [RegularSpace X]
    {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
    ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed L
KL : K ⊆ interior L
LU : L ⊆ U
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

Tactic:
have A : closure (interior L) ⊆ L := by
  apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq)

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure (interior L) ⊆ L
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure (interior L) ⊆ L
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

Tactic:
refine ⟨interior L, isOpen_interior, KL, A.trans LU, ?_⟩

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure (interior L) ⊆ L
⊢ IsCompact (closure (interior L))

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

Tactic:
rcases exists_compact_closed_between hK hU hKU with ⟨L, L_compact, L_closed, KL, LU⟩

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed L
KL : K ⊆ interior L
LU : L ⊆ U
⊢ ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed L
KL : K ⊆ interior L
LU : L ⊆ U
A : closure (interior L) ⊆ L
⊢ IsCompact (closure (interior L))

Tactic:
exact L_compact.closure_of_subset interior_subset

Result:
no goals

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
L : Set X
L_compact : IsCompact L
L_closed : IsClosed L
KL : K ⊆ interior L
LU : L ⊆ U
⊢ closure (interior L) ⊆ L

Tactic:
apply (closure_mono interior_subset).trans (le_of_eq L_closed.closure_eq)

Result:
no goals