-- Mathlib/Topology/Separation/Regular.lean
/-- This technique to witness `HasSeparatingCover` in regular Lindelöf topological spaces
will be used to prove regular Lindelöf spaces are normal. -/
lemma IsClosed.HasSeparatingCover {s t : Set X} [LindelofSpace X] [RegularSpace X]
    (s_cl : IsClosed s) (t_cl : IsClosed t) (st_dis : Disjoint s t) : HasSeparatingCover s t

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
⊢ _root_.HasSeparatingCover s t

Tactic:
rcases isEmpty_or_nonempty X with empty_X | nonempty_X

Result:
case inl
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover s t

case inr
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
⊢ _root_.HasSeparatingCover s t

Proof state:
X✝ : Type u_1
inst✝³ : TopologicalSpace X✝
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
⊢ ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)

Tactic:
obtain ⟨n, nna, ncl, nsubkc⟩ := ((regularSpace_TFAE X).out 0 3 :).mp ‹RegularSpace X› a tᶜ <|
  t_cl.compl_mem_nhds (disjoint_left.mp st_dis ains)

Result:
case intro.intro.intro
X✝ : Type u_1
inst✝³ : TopologicalSpace X✝
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
n : Set X
nna : n ∈ 𝓝 a
ncl : IsClosed n
nsubkc : n ⊆ tᶜ
⊢ ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
⊢ ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)

Tactic:
wlog ains : a ∈ s

Result:
case inr
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [inst_1 : LindelofSpace X] [inst_2 : RegularSpace X],
    IsClosed s →
      IsClosed t → Disjoint s t → Nonempty X → ∀ a ∈ s, ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)
ains : a ∉ s
⊢ ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)

X✝ : Type u_1
inst✝³ : TopologicalSpace X✝
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
⊢ ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)

Proof state:
case intro.intro.intro
X✝ : Type u_1
inst✝³ : TopologicalSpace X✝
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
ains : a ∈ s
n : Set X
nna : n ∈ 𝓝 a
ncl : IsClosed n
nsubkc : n ⊆ tᶜ
⊢ ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)

Tactic:
exact
  ⟨interior n,
   isOpen_interior,
   disjoint_left.mpr fun ⦃_⦄ ain ↦
     nsubkc <| (IsClosed.closure_subset_iff ncl).mpr interior_subset ain,
   fun _ ↦ mem_interior_iff_mem_nhds.mpr nna⟩

Result:
no goals

Proof state:
case inr.intro
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : X → Set X
u_open : ∀ (a : X), IsOpen (u a)
u_dis : ∀ (a : X), Disjoint (closure (u a)) t
u_nhd : ∀ a ∈ s, a ∈ u a
f : ℕ → X
f_cov : s ⊆ ⋃ n, u (f n)
⊢ _root_.HasSeparatingCover s t

Tactic:
exact ⟨u ∘ f, f_cov, fun n ↦ ⟨u_open (f n), u_dis (f n)⟩⟩

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
a : X
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X} [inst_1 : LindelofSpace X] [inst_2 : RegularSpace X],
    IsClosed s →
      IsClosed t → Disjoint s t → Nonempty X → ∀ a ∈ s, ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)
ains : a ∉ s
⊢ ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)

Tactic:
exact ⟨∅, isOpen_empty, SeparatedNhds.empty_left t |>.disjoint_closure_left, fun a ↦ ains a⟩

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
this : ∀ (a : X), ∃ n, IsOpen n ∧ Disjoint (closure n) t ∧ (a ∈ s → a ∈ n)
⊢ _root_.HasSeparatingCover s t

Tactic:
choose u u_open u_dis u_nhd using this

Result:
case inr
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : X → Set X
u_open : ∀ (a : X), IsOpen (u a)
u_dis : ∀ (a : X), Disjoint (closure (u a)) t
u_nhd : ∀ a ∈ s, a ∈ u a
⊢ _root_.HasSeparatingCover s t

Proof state:
case inr
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : X → Set X
u_open : ∀ (a : X), IsOpen (u a)
u_dis : ∀ (a : X), Disjoint (closure (u a)) t
u_nhd : ∀ a ∈ s, a ∈ u a
⊢ _root_.HasSeparatingCover s t

Tactic:
obtain ⟨f, f_cov⟩ := s_cl.isLindelof.indexed_countable_subcover
  u u_open (fun a ainh ↦ mem_iUnion.mpr ⟨a, u_nhd a ainh⟩)

Result:
case inr.intro
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
nonempty_X : Nonempty X
u : X → Set X
u_open : ∀ (a : X), IsOpen (u a)
u_dis : ∀ (a : X), Disjoint (closure (u a)) t
u_nhd : ∀ a ∈ s, a ∈ u a
f : ℕ → X
f_cov : s ⊆ ⋃ n, u (f n)
⊢ _root_.HasSeparatingCover s t

Proof state:
case inl
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover s t

Tactic:
rw [subset_eq_empty (t := s) (fun ⦃_⦄ _ ↦ trivial) (univ_eq_empty_iff.mpr empty_X)]

Result:
case inl
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover ∅ t

Proof state:
case inl
X : Type u_1
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : LindelofSpace X
inst✝ : RegularSpace X
s_cl : IsClosed s
t_cl : IsClosed t
st_dis : Disjoint s t
empty_X : IsEmpty X
⊢ _root_.HasSeparatingCover ∅ t

Tactic:
exact hasSeparatingCovers_iff_separatedNhds.mpr (SeparatedNhds.empty_left t) |>.1

Result:
no goals