-- 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 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)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = ⟨t, tinT⟩
⊢ ⋂ i, closure (g' i) ⊆ t

Tactic:
refine iInter_subset_of_subset n <| (clg'_sub_g n).trans ?_

Result:
case 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)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = ⟨t, tinT⟩
⊢ ↑(g n) ⊆ t

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 univ
t_cl : IsClosed t
T_open : ∀ t ∈ ∅, IsOpen t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover ∅ t

Tactic:
exact t.hasSeparatingCover_empty_left

Result:
no goals

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 univ
t_cl : IsClosed t
T_open : ∀ t ∈ ∅, IsOpen t
T_count : ∅.Countable
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover s t

Tactic:
rw [(s.disjoint_univ).mp 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 ∅ 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)
⊢ t = ⋂ i, closure (g' i)

Tactic:
apply (subset_iInter fun n ↦ (clt_sub_g' n).trans subset_closure).antisymm

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)
t : Set X
tinT : t ∈ T
⊢ ⋂ i, closure (g' i) ⊆ t

Tactic:
obtain ⟨n, gn⟩ := g_surj ⟨t, tinT⟩

Result:
case 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)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = ⟨t, tinT⟩
⊢ ⋂ i, closure (g' i) ⊆ t

Proof state:
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 : ℕ
⊢ t ⊆ interior (closure (g' n))

Tactic:
rw [← closure_eq_iff_isClosed.mpr t_cl] at clt_sub_g'

Result:
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 : ℕ), closure t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure (g' i)
n : ℕ
⊢ t ⊆ interior (closure (g' n))

Proof state:
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

Tactic:
refine fun n ↦ ⟨isOpen_compl_iff.mpr isClosed_closure, ?_⟩

Result:
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 : ℕ
⊢ Disjoint (closure (closure (g' n))ᶜ) t

Proof state:
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 : ℕ), closure t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure (g' n) ⊆ ↑(g n)
clg'_int : t = ⋂ i, closure (g' i)
n : ℕ
⊢ t ⊆ interior (closure (g' n))

Tactic:
exact subset_closure.trans <| (clt_sub_g' n).trans <| (g'_open n).subset_interior_closure

Result:
no goals