-- Mathlib/Topology/Separation/GDelta.lean
theorem Disjoint.hasSeparatingCover_closed_gdelta_right {s t : Set X} [NormalSpace X]
    (st_dis : Disjoint s t) (t_cl : IsClosed t) (t_gd : IsGδ t) : HasSeparatingCover s t

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure (g' i)
⊢ s ⊆ ⋃ n, (fun n => (closure (g' n))ᶜ) n ∧
    ∀ (n : ℕ), IsOpen ((fun n => (closure (g' n))ᶜ) n) ∧ Disjoint (closure ((fun n => (closure (g' n))ᶜ) n)) t

Tactic:
constructor

Result:
case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure (g' i)
⊢ s ⊆ ⋃ n, (closure (g' n))ᶜ

case h.right
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure (g' i)
⊢ ∀ (n : ℕ), IsOpen (closure (g' n))ᶜ ∧ Disjoint (closure (closure (g' n))ᶜ) t

Proof state:
case intro.intro.intro.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
⊢ HasSeparatingCover s t

Tactic:
obtain ⟨g, g_surj⟩ := T_count.exists_surjective T_nonempty

Result:
case intro.intro.intro.inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
⊢ HasSeparatingCover s t

Proof state:
case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure (g' i)
⊢ s ⊆ ⋃ n, (closure (g' n))ᶜ

Tactic:
rw [← compl_iInter, subset_compl_comm, ← clg'_int]

Result:
case h.left
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure (g' i)
⊢ t ⊆ sᶜ

Proof state:
case intro.intro.intro.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T_open : ∀ t ∈ ∅, IsOpen t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover s t

Tactic:
rw [T_int, sInter_empty] at st_dis

Result:
case intro.intro.intro.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s univ
t_cl : IsClosed t
T_open : ∀ t ∈ ∅, IsOpen t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover s t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure (g' i) ⊆ t

Tactic:
rw [T_int]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure (g' i) ⊆ ⋂₀ T

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
⊢ ⋂ i, closure (g' i) ⊆ ⋂₀ T

Tactic:
refine subset_sInter fun t tinT ↦ ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t✝ : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t✝
t_cl : IsClosed t✝
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t✝ = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t✝ ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
t : Set X
tinT : t ∈ T
⊢ ⋂ i, closure (g' i) ⊆ t

Proof state:
case intro.intro.intro.inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
⊢ HasSeparatingCover s t

Tactic:
choose g' g'_open clt_sub_g' clg'_sub_g using fun n ↦ by
  apply normal_exists_closure_subset t_cl (T_open (g n).1 (g n).2)
  rw [T_int]
  exact sInter_subset_of_mem (g n).2

Result:
case intro.intro.intro.inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → ↑T
g_surj : Surjective g
g' : ℕ → Set X
g'_open : ∀ (n : ℕ), IsOpen (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
⊢ HasSeparatingCover s t

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
t_gd : IsGδ t
⊢ HasSeparatingCover s t

Tactic:
obtain ⟨T, T_open, T_count, T_int⟩ := t_gd

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen t
T_count : T.Countable
T_int : t = ⋂₀ T
⊢ HasSeparatingCover s t