awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
inst_2 : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst] (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ U i
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), U i)

Tactic:
.biInter (to_countable _) fun n _ => (hU n).2.isGδ

Premises used: Set.Mem, And.right, Set.to_countable, IsOpen.isGδ, IsGδ.biInter
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
inst_2 : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst] (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ U i
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), U i)

Tactic:
exact .biInter (to_countable _) fun n _ => (hU n).2.isGδ
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
s : Set X
inst_2 : T1Space X
hs : s.Finite
⊢ IsGδ s

Tactic:
Finite.induction_on _ hs .empty fun _ _ ↦ .union (.singleton _)

Premises used: Set.Finite.induction_on
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
t_gd : IsGδ t
obtain :
  ∀ (T : Set (Set X)) (T_open : ∀ t ∈ T, IsOpen[inst] t) (T_count : T.Countable) (T_int : t = ⋂₀ T),
    HasSeparatingCover s t
⊢ HasSeparatingCover s t

Tactic:
obtain ⟨T, T_open, T_count, T_int⟩ := t_gd
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
inl :
  ∀ (T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t)
    (T_count : Set.Countable.{u_1} (α := Set X) ∅) (T_int : t = ⋂₀ ∅), HasSeparatingCover s t
inr : ∀ (T_nonempty : T.Nonempty), HasSeparatingCover s t
⊢ HasSeparatingCover s t

Tactic:
rcases T.eq_empty_or_nonempty with rfl | T_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
⊢ Disjoint s univ

Tactic:
rw [T_int, sInter_empty] at st_dis

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
st_dis₁ : Disjoint s univ
⊢ IsClosed[inst] t

Tactic:
rw [T_int, sInter_empty] at st_dis

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
st_dis₁ : Disjoint s univ
t_cl₁ : IsClosed[inst] t
⊢ ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t

Tactic:
rw [T_int, sInter_empty] at st_dis

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
st_dis₁ : Disjoint s univ
t_cl₁ : IsClosed[inst] t
T_open₁ : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
⊢ Set.Countable.{u_1} (α := Set X) ∅

Tactic:
rw [T_int, sInter_empty] at st_dis

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
st_dis₁ : Disjoint s univ
t_cl₁ : IsClosed[inst] t
T_open₁ : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count₁ : Set.Countable.{u_1} (α := Set X) ∅
⊢ t = ⋂₀ ∅

Tactic:
rw [T_int, sInter_empty] at st_dis

Premises used: Set.sInter_empty
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s univ
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
inl : HasSeparatingCover ∅ t
⊢ HasSeparatingCover s t

Tactic:
rw [(s.disjoint_univ).mp st_dis]

Premises used: Set.disjoint_univ, Iff.mp
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s univ
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover ∅ t

Tactic:
t.hasSeparatingCover_empty_left

Premises used: Set.hasSeparatingCover_empty_left
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s univ
t_cl : IsClosed[inst] t
T_open : ∀ (t : Set X), Membership.mem (γ := Set (Set X)) ∅ t → IsOpen[inst] t
T_count : Set.Countable.{u_1} (α := Set X) ∅
T_int : t = ⋂₀ ∅
⊢ HasSeparatingCover ∅ t

Tactic:
exact t.hasSeparatingCover_empty_left

Premises used: Set.hasSeparatingCover_empty_left
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
inr : ∀ (g : ℕ → (↑T : Type u_1)) (g_surj : Surjective g), HasSeparatingCover s t
⊢ HasSeparatingCover s t

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

Premises used: Set.Countable.exists_surjective
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
n : ℕ
apply : t ⊆ (↑(g n) : Set X)
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ t ⊆ u ∧ closure[inst] u ⊆ (↑(g n) : Set X)

Tactic:
apply normal_exists_closure_subset t_cl (T_open (g n).1 (g n).2)

Premises used: normal_exists_closure_subset, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
n : ℕ
rw : ⋂₀ T ⊆ (↑(g n) : Set X)
⊢ t ⊆ (↑(g n) : Set X)

Tactic:
rw [T_int]
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
n : ℕ
⊢ ⋂₀ T ⊆ (↑(g n) : Set X)

Tactic:
sInter_subset_of_mem (g n).2

Premises used: Set.sInter_subset_of_mem, Subtype.property
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
n : ℕ
⊢ ⋂₀ T ⊆ (↑(g n) : Set X)

Tactic:
exact sInter_subset_of_mem (g n).2

Premises used: Set.sInter_subset_of_mem, Subtype.property
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
inr :
  ∀ (g' : (n : ℕ) → Set X) (g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)) (clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n)
    (clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)), HasSeparatingCover s t
⊢ 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
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
apply : ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t
⊢ t = ⋂ (i : ℕ), closure[inst] (g' i)

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

Premises used: subset_closure, Set.subset_iInter, HasSubset.Subset.trans, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
rw : ⋂ (i : ℕ), closure[inst] (g' i) ⊆ ⋂₀ T
⊢ ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t

Tactic:
rw [T_int]
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
⊢ ⋂ (i : ℕ), closure[inst] (g' i) ⊆ ⋂₀ T

Tactic:
subset_sInter fun t tinT ↦ ?_

Premises used: Set.subset_sInter
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
refine : ∀ (t : Set X) (tinT : t ∈ T), ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t
⊢ ⋂ (i : ℕ), closure[inst] (g' i) ⊆ ⋂₀ T

Tactic:
refine subset_sInter fun t tinT ↦ ?_

Premises used: Set.subset_sInter
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t_1 : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t_1
t_cl : IsClosed[inst] t_1
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t_1 = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t_1 ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
t : Set X
tinT : t ∈ T
obtain : ∀ (n : ℕ) (gn : g n = Subtype.mk (p := fun (x : Set X) ↦ x ∈ T) t tinT), ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t
⊢ ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t

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

Premises used: Subtype.mk
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t_1 : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t_1
t_cl : IsClosed[inst] t_1
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t_1 = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t_1 ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = Subtype.mk (p := fun (x : Set X) ↦ x ∈ T) t tinT
⊢ ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t

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

Premises used: HasSubset.Subset.trans, Set.iInter_subset_of_subset
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t_1 : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t_1
t_cl : IsClosed[inst] t_1
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t_1 = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t_1 ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = Subtype.mk (p := fun (x : Set X) ↦ x ∈ T) t tinT
refine : (↑(g n) : Set X) ⊆ t
⊢ ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t

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

Premises used: HasSubset.Subset.trans, Set.iInter_subset_of_subset
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t_1 : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t_1
t_cl : IsClosed[inst] t_1
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t_1 = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t_1 ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
t : Set X
tinT : t ∈ T
n : ℕ
gn : g n = Subtype.mk (p := fun (x : Set X) ↦ x ∈ T) t tinT
rw rw₁ :
  (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ T) t tinT) : Set X) ⊆
    (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ T) t tinT) : Set X)
⊢ (↑(g n) : Set X) ⊆ t

Tactic:
rw [gn]
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
⊢ t = ⋂ (i : ℕ), closure[inst] (g' i)

Tactic:
have clg'_int : t = ⋂ i, closure (g' i) := by
    apply (subset_iInter fun n ↦ (clt_sub_g' n).trans subset_closure).antisymm
    rw [T_int]
    refine subset_sInter fun t tinT ↦ ?_
    obtain ⟨n, gn⟩ := g_surj ⟨t, tinT⟩
    refine iInter_subset_of_subset n <| (clg'_sub_g n).trans ?_
    rw [gn]
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
h :
  s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ (closure[inst] (g' n))ᶜ) n ∧
    ∀ (n : ℕ),
      IsOpen[inst] ((fun (n : ℕ) ↦ (closure[inst] (g' n))ᶜ) n) ∧
        Disjoint (closure[inst] ((fun (n : ℕ) ↦ (closure[inst] (g' n))ᶜ) n)) t
⊢ HasSeparatingCover s t

Tactic:
use fun n ↦ (closure (g' n))ᶜ

Premises used: Compl.compl, closure
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
h : s ⊆ ⋃ (n : ℕ), (closure[inst] (g' n))ᶜ
h₁ : ∀ (n : ℕ), IsOpen[inst] (closure[inst] (g' n))ᶜ ∧ Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t
⊢ s ⊆ ⋃ (n : ℕ), (fun (n : ℕ) ↦ (closure[inst] (g' n))ᶜ) n ∧
    ∀ (n : ℕ),
      IsOpen[inst] ((fun (n : ℕ) ↦ (closure[inst] (g' n))ᶜ) n) ∧
        Disjoint (closure[inst] ((fun (n : ℕ) ↦ (closure[inst] (g' n))ᶜ) n)) t

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
h : t ⊆ sᶜ
⊢ s ⊆ ⋃ (n : ℕ), (closure[inst] (g' n))ᶜ

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

Premises used: Set.compl_iInter, Set.subset_compl_comm
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
⊢ t ⊆ sᶜ

Tactic:
st_dis.subset_compl_left

Premises used: Disjoint.subset_compl_left
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
⊢ t ⊆ sᶜ

Tactic:
exact st_dis.subset_compl_left

Premises used: Disjoint.subset_compl_left
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
⊢ ∀ (n : ℕ), IsOpen[inst] (closure[inst] (g' n))ᶜ ∧ Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t

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

Premises used: Iff.mpr, And.intro, isClosed_closure, isOpen_compl_iff
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
h : ∀ (n : ℕ), Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t
⊢ ∀ (n : ℕ), IsOpen[inst] (closure[inst] (g' n))ᶜ ∧ Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t

Tactic:
refine fun n ↦ ⟨isOpen_compl_iff.mpr isClosed_closure, ?_⟩
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
n : ℕ
h : t ⊆ interior (closure[inst] (g' n))
⊢ Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t

Tactic:
simp only [closure_compl, disjoint_compl_left_iff_subset]

Premises used: Set.disjoint_compl_left_iff_subset, closure_compl
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
n : ℕ
h :
  ∀ (clt_sub_g' : ∀ (n : ℕ), closure[inst] t ⊆ g' n) (clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X))
    (clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)) (n : ℕ), t ⊆ interior (closure[inst] (g' n))
⊢ t ⊆ interior (closure[inst] (g' n))

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

Premises used: Iff.mpr, closure_eq_iff_isClosed
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), closure[inst] t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
n : ℕ
⊢ t ⊆ interior (closure[inst] (g' n))

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

Premises used: subset_closure, HasSubset.Subset.trans, IsOpen.subset_interior_closure
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
inst_1 : NormalSpace X
st_dis : Disjoint s t
t_cl : IsClosed[inst] t
T : Set (Set X)
T_open : ∀ t ∈ T, IsOpen[inst] t
T_count : T.Countable
T_int : t = ⋂₀ T
T_nonempty : T.Nonempty
g : ℕ → (↑T : Type u_1)
g_surj : Surjective g
g' : (n : ℕ) → Set X
g'_open : ∀ (n : ℕ), IsOpen[inst] (g' n)
clt_sub_g' : ∀ (n : ℕ), closure[inst] t ⊆ g' n
clg'_sub_g : ∀ (n : ℕ), closure[inst] (g' n) ⊆ (↑(g n) : Set X)
clg'_int : t = ⋂ (i : ℕ), closure[inst] (g' i)
n : ℕ
⊢ t ⊆ interior (closure[inst] (g' n))

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

Premises used: subset_closure, HasSubset.Subset.trans, IsOpen.subset_interior_closure