awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (hypothesis)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES :
  ∀ (i : Fin n),
    ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)
hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))
hEdis : Pairwise (Disjoint on E)
g : (x : X) → Fin n
hg : ∀ (x : X), (fun (i : Fin n) ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun (i : Fin n) ↦ x ∈ E i) y → y = g x
⊢ ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
have h_ex : ∀ (i : Fin n), ∃ (x : X), x ∈ E i
Tactic: have h_ex (i) : ∃ x, x ∈ E i := by
    simpa [← SetLike.coe_set_eq, ← nonempty_iff_ne_empty] using hEne i
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES :
  ∀ (i : Fin n),
    ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)
hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))
hEdis : Pairwise (Disjoint on E)
g : (x : X) → Fin n
hg : ∀ (x : X), (fun (i : Fin n) ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun (i : Fin n) ↦ x ∈ E i) y → y = g x
h_ex : ∀ (i : Fin n), ∃ (x : X), x ∈ E i
⊢ ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
have choose : ∀ (r : (i : Fin n) → X) (hr : ∀ (i : Fin n), r i ∈ E i),
  ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
Tactic: choose r hr using h_ex
Cleared hypotheses: h_ex
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES :
  ∀ (i : Fin n),
    ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)
hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))
hEdis : Pairwise (Disjoint on E)
g : (x : X) → Fin n
hg : ∀ (x : X), (fun (i : Fin n) ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun (i : Fin n) ↦ x ∈ E i) y → y = g x
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ E i
⊢ ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
have refine : ∀ (j : Fin n), IsOpen[inst] (g ⁻¹' {j})
Tactic: refine ⟨n, g, f ∘ r, continuous_discrete_rng.mpr fun j ↦ ?_, fun x ↦ (hES _) _ (hg _) _ (hr _)⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES :
  ∀ (i : Fin n),
    ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)
hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))
hEdis : Pairwise (Disjoint on E)
g : (x : X) → Fin n
hg : ∀ (x : X), (fun (i : Fin n) ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun (i : Fin n) ↦ x ∈ E i) y → y = g x
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ E i
j : Fin n
⊢ IsOpen[inst] (g ⁻¹' {j})
have h : g ⁻¹' {j} = (↑(E j) : Set X)
Tactic: convert! (E j).isOpen
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V),
    ∀ (x : X),
      Membership.mem (α := V × V) S
        (((f : (a : X) → V) x, ∏ n : Fin n, (↑(U n) : Set X).mulIndicator (fun (x : X) ↦ v n) x) : V × V)
have obtain : ∀ (n : ℕ) (g : X → Fin n) (h : Fin n → V) (hg : Continuous[inst, _] g)
  (hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)),
  ∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V),
    ∀ (x : X),
      Membership.mem (α := V × V) S
        (((f : (a : X) → V) x, ∏ n : Fin n, (↑(U n) : Set X).mulIndicator (fun (x : X) ↦ v n) x) : V × V)
Tactic: obtain ⟨n, g, h, hg, hgh⟩ := exists_finite_approximation_of_mem_nhds_diagonal f hS
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
⊢ ∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V),
    ∀ (x : X),
      Membership.mem (α := V × V) S
        (((f : (a : X) → V) x, ∏ n : Fin n, (↑(U n) : Set X).mulIndicator (fun (x : X) ↦ v n) x) : V × V)
have refine : ∀ (x : X),
  Membership.mem (α := V × V) S
    (((f : (a : X) → V) x,
        ∏ n_1 : Fin n,
          (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := sorry : Clopens X }) n_1) : Set X).mulIndicator
            (fun (x : X) ↦ h n_1) x) :
      V × V)
Tactic: refine ⟨n, fun i ↦ ⟨_, (isClopen_discrete {i}).preimage hg⟩, h, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
x : X
⊢ Membership.mem (α := V × V) S
    (((f : (a : X) → V) x,
        ∏ n_1 : Fin n,
          (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := ⋯ : Clopens X }) n_1) : Set X).mulIndicator
            (fun (x : X) ↦ h n_1) x) :
      V × V)
have h₁ : ∏ n_1 : Fin n,
    (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := sorry : Clopens X }) n_1) : Set X).mulIndicator
      (fun (x : X) ↦ h n_1) x =
  h (g x)
Tactic: convert! hgh x
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T1Space X
hs : s.Countable
⊢ IsGδ sᶜ
have rw : IsGδ.{u_1} (X := X) (⋂ i ∈ s, {i}ᶜ)
Tactic: rw [← biUnion_of_singleton s, compl_iUnion₂]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
inst_2 : T1Space X
x : X
⊢ IsGδ (X := X) {x}
have rcases : ∀ (U : ℕ → Set X) (hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst] (U i)) (h_basis : (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ U i),
  IsGδ (X := X) {x}
Tactic: rcases (nhds_basis_opens x).exists_antitone_subbasis with ⟨U, hU, h_basis⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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δ (X := X) {x}
have rw : IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), U i)
Tactic: rw [← biInter_basis_nhds h_basis.toHasBasis]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
⊢ HasSeparatingCover s t
have obtain : ∀ (T : Set (Set X)) (T_open : ∀ t ∈ T, IsOpen[inst] t) (T_count : T.Countable) (T_int : t = ⋂₀ T),
  HasSeparatingCover s t
Tactic: obtain ⟨T, T_open, T_count, T_int⟩ := t_gd
Cleared hypotheses: t_gd
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
⊢ HasSeparatingCover s t
have 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
Tactic: rcases T.eq_empty_or_nonempty with rfl | T_nonempty
Cleared hypotheses: T, T_open, T_count, T_int
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
⊢ HasSeparatingCover s t
have inr : ∀ (T_nonempty : T.Nonempty), HasSeparatingCover s t
Tactic: rcases T.eq_empty_or_nonempty with rfl | T_nonempty
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (hypothesis)
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 = ⋂₀ ∅
⊢ HasSeparatingCover s t
have st_dis₁ : Disjoint s univ
Tactic: rw [T_int, sInter_empty] at st_dis
Cleared hypotheses: st_dis, t_cl, T_open, T_count, T_int
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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 s t
have inl : HasSeparatingCover ∅ t
Tactic: rw [(s.disjoint_univ).mp st_dis]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
⊢ HasSeparatingCover s t
have inr : ∀ (g : ℕ → (↑T : Type u_1)) (g_surj : Surjective g), HasSeparatingCover s t
Tactic: obtain ⟨g, g_surj⟩ := T_count.exists_surjective T_nonempty
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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 : ℕ
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ t ⊆ u ∧ closure[inst] u ⊆ (↑(g n) : Set X)
have apply : t ⊆ (↑(g n) : Set X)
Tactic: apply normal_exists_closure_subset t_cl (T_open (g n).1 (g n).2)
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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)
have rw : ⋂₀ T ⊆ (↑(g n) : Set X)
Tactic: rw [T_int]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
⊢ HasSeparatingCover s t
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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)
have apply : ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t
Tactic: apply (subset_iInter fun n ↦ (clt_sub_g' n).trans subset_closure).antisymm
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
have rw : ⋂ (i : ℕ), closure[inst] (g' i) ⊆ ⋂₀ T
Tactic: rw [T_int]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
have refine : ∀ (t : Set X) (tinT : t ∈ T), ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t
Tactic: refine subset_sInter fun t tinT ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
⊢ ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t
have obtain : ∀ (n : ℕ) (gn : g n = Subtype.mk (p := fun (x : Set X) ↦ x ∈ T) t tinT), ⋂ (i : ℕ), closure[inst] (g' i) ⊆ t
Tactic: obtain ⟨n, gn⟩ := g_surj ⟨t, tinT⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
have refine : (↑(g n) : Set X) ⊆ t
Tactic: refine iInter_subset_of_subset n <| (clg'_sub_g n).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
⊢ (↑(g n) : Set X) ⊆ t
have 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)
Tactic: rw [gn]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (hypothesis)
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)
⊢ HasSeparatingCover s t
have clg'_int : 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]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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)
⊢ HasSeparatingCover s t
have 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
Tactic: use fun n ↦ (closure (g' n))ᶜ
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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)
⊢ 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
have h : s ⊆ ⋃ (n : ℕ), (closure[inst] (g' n))ᶜ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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))ᶜ
⊢ 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
have h₁ : ∀ (n : ℕ), IsOpen[inst] (closure[inst] (g' n))ᶜ ∧ Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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)
⊢ s ⊆ ⋃ (n : ℕ), (closure[inst] (g' n))ᶜ
have h : t ⊆ sᶜ
Tactic: rw [← compl_iInter, subset_compl_comm, ← clg'_int]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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
have h : ∀ (n : ℕ), Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t
Tactic: refine fun n ↦ ⟨isOpen_compl_iff.mpr isClosed_closure, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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 : ℕ
⊢ Disjoint (closure[inst] (closure[inst] (g' n))ᶜ) t
have h : t ⊆ interior (closure[inst] (g' n))
Tactic: simp only [closure_compl, disjoint_compl_left_iff_subset]
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
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 : ℕ
⊢ t ⊆ interior (closure[inst] (g' n))
have 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))
Tactic: rw [← closure_eq_iff_isClosed.mpr t_cl] at clt_sub_g'
Cleared hypotheses: clt_sub_g', clg'_sub_g, clg'_int, n
-- Lean 4 proof step from Mathlib.Topology.Separation.GDelta (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PerfectlyNormalSpace X
x y : X
hxy : x ⤳ y
⊢ y ⤳ x
have rw : ∀ (s : Set X), IsClosed[inst] s → y ∈ s → x ∈ s
Tactic: rw [specializes_iff_forall_closed]