-- Mathlib/Topology/Separation/Hausdorff.lean
/-- In a `T2Space X`, for disjoint closed sets `s t` such that `closure sᶜ` is compact,
there are neighbourhoods that separate `s` and `t`. -/
lemma SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed [T2Space X] {s : Set X}
    {t : Set X} (H1 : IsClosed s) (H2 : IsCompact (closure sᶜ)) (H3 : IsClosed t)
    (H4 : Disjoint s t) : SeparatedNhds s t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s ∩ closure sᶜ) t

Tactic:
refine .of_isCompact_isCompact ?_ ht (disjoint_of_subset_left inter_subset_left H4)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ IsCompact (s ∩ closure sᶜ)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ IsCompact (s ∩ closure sᶜ)

Tactic:
exact H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
⊢ SeparatedNhds s t

Tactic:
have ht : IsCompact t := .of_isClosed_subset H2 H3 <| H4.subset_compl_left.trans subset_closure

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds s t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s \ interior s) t

Tactic:
rw [← H1.frontier_eq, frontier_eq_closure_inter_closure, H1.closure_eq]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s ∩ closure sᶜ) t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s \ interior s ∪ interior s) t

Tactic:
refine .union_left ?_ ⟨interior s, sᶜ, isOpen_interior, H1.isOpen_compl, le_rfl,
  H4.subset_compl_left, disjoint_compl_right.mono_left interior_subset⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s \ interior s) t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds s t

Tactic:
rw [← diff_union_of_subset (interior_subset (s := s))]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s t : Set X
H1 : IsClosed s
H2 : IsCompact (closure sᶜ)
H3 : IsClosed t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s \ interior s ∪ interior s) t