awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsClosed[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsClosed[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
⊢ False
have this : s \ U = s
Tactic: have : s \ U = s := hmin (s \ U) diff_subset ⟨y, hy, hyU⟩ (hs.sdiff hUo)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
⊢ ∃ x ∈ S, IsClosed[inst] {x}
have obtain : ∀ (V : Set X) (Vsub : V ⊆ S) (Vne : V.Nonempty) (Vcls : IsClosed[inst] V)
  (hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V), ∃ x ∈ S, IsClosed[inst] {x}
Tactic: obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
inst_2 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
V : Set X
Vsub : V ⊆ S
Vne : V.Nonempty
Vcls : IsClosed[inst] V
hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
⊢ ∃ x ∈ S, IsClosed[inst] {x}
have rcases : ∀ (x : X) (Vsub : {x} ⊆ S) (Vne : Set.Nonempty (α := X) {x}) (Vcls : IsClosed[inst] {x})
  (hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed[inst] V' → V' = {x}), ∃ x ∈ S, IsClosed[inst] {x}
Tactic: rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩
Cleared hypotheses: V, Vsub, Vne, Vcls, hV
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
⊢ s.Subsingleton
have refine : ∀ (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y), False
Tactic: refine fun x hx y hy => of_not_not fun hxy => ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
⊢ False
have rcases : ∀ (U : Set X) (hUo : IsOpen[inst] U) (hU : Xor (x ∈ U) (y ∈ U)), False
Tactic: rcases exists_isOpen_xor_mem hxy with ⟨U, hUo, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
⊢ False
have inr : ∀
  (this :
    ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s)
      (hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
      (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False)
  (h : ¬(x ∈ U ∧ y ∉ U)), False
Tactic: wlog h : x ∈ U ∧ y ∉ U
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hs : IsOpen[inst] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst] U
hU : Xor (x ∈ U) (y ∈ U)
inr :
  ∀
    (this :
      ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s)
        (hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y)
        (U : Set X) (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False)
    (h : ¬(x ∈ U ∧ y ∉ U)), False
⊢ False
have wlog : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s)
  (hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) (x : X) (hx : x ∈ s) (y : X) (hy : y ∈ s) (hxy : ¬x = y) (U : Set X)
  (hUo : IsOpen U) (hU : Xor (x ∈ U) (y ∈ U)) (h : x ∈ U ∧ y ∉ U), False
Tactic: wlog h : x ∈ U ∧ y ∉ U
Cleared hypotheses: inst_1, s, hs, hmin, x, hx, y, hy, hxy, U, hUo, hU
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsOpen[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
⊢ False
have hxU : x ∈ U
Tactic: obtain ⟨hxU, hyU⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsOpen[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
hxU : x ∈ U
⊢ False
have hyU : y ∉ U
Tactic: obtain ⟨hxU, hyU⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
X : Type u_1
inst_1 : TopologicalSpace X
inst_2 : T0Space X
s : Set X
hs : IsOpen[inst_1] s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen[inst_1] t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen[inst_1] U
hU : Xor (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
⊢ False
have this : s ∩ U = s
Tactic: have : s ∩ U = s := hmin (s ∩ U) inter_subset_left ⟨x, hx, hxU⟩ (hs.inter hUo)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Set X
hfin : s.Finite
hne : s.Nonempty
ho : IsOpen[inst] s
⊢ ∃ x ∈ s, IsOpen[inst] {x}
have lift : ∀ (s : Finset X) (hne : (↑s : Set X).Nonempty) (ho : IsOpen[inst] (↑s : Set X)), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
Tactic: lift s to Finset X using hfin
Cleared hypotheses: s, hfin, hne, ho
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
have a : ∀ (s : Finset X),
  (∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}) →
    ∀ (hne : (↑s : Set X).Nonempty) (ho : IsOpen[inst] (↑s : Set X)), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
Tactic: induction s using Finset.strongInductionOn
Cleared hypotheses: s, hne, ho
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
have a : ∀ (t : Finset X) (hts : t ⊂ s) (htne : t.Nonempty) (hto : IsOpen[inst] (↑t : Set X)),
  ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
Tactic: rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
a :
  ∀ (t : Finset X) (hts : t ⊂ s) (htne : t.Nonempty) (hto : IsOpen[inst] (↑t : Set X)),
    ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
have a₁ : ∀ (ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
Tactic: rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen[inst] (↑t : Set X)
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
have a : ∀ (x : X) (hxt : x ∈ (↑t : Set X)) (hxo : IsOpen[inst] {x}), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
Tactic: rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
have a : ∀ (x : X) (hx : (↑s : Set X) = {x}), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
Tactic: rsuffices ⟨x, hx⟩ : ∃ x, (s : Set X) = {x}
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
a : ∀ (x : X) (hx : (↑s : Set X) = {x}), ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
⊢ ∃ x ∈ (↑s : Set X), IsOpen[inst] {x}
have rsuffices : ∃ (x : X), (↑s : Set X) = {x}
Tactic: rsuffices ⟨x, hx⟩ : ∃ x, (s : Set X) = {x}
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
⊢ ∃ (x : X), (↑s : Set X) = {x}
have refine : ∀ t ⊆ (↑s : Set X), t.Nonempty → IsOpen[inst] t → t = (↑s : Set X)
Tactic: refine minimal_nonempty_open_eq_singleton ho hne ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
⊢ ∀ t ⊆ (↑s : Set X), t.Nonempty → IsOpen[inst] t → t = (↑s : Set X)
have refine : ∀ (t : Set X) (hts : t ⊆ (↑s : Set X)) (htne : t.Nonempty) (hto : IsOpen[inst] t) (hts' : ¬t = (↑s : Set X)),
  ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
Tactic: refine fun t hts htne hto => of_not_not fun hts' => ht ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, ∀ (hne : (↑t : Set X).Nonempty) (ho : IsOpen[inst] (↑t : Set X)), ∃ x ∈ (↑t : Set X), IsOpen[inst] {x}
hne : (↑s : Set X).Nonempty
ho : IsOpen[inst] (↑s : Set X)
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
t : Set X
hts : t ⊆ (↑s : Set X)
htne : t.Nonempty
hto : IsOpen[inst] t
hts' : ¬t = (↑s : Set X)
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
have lift : ∀ (t : Finset X) (hts : (↑t : Set X) ⊆ (↑s : Set X)) (htne : (↑t : Set X).Nonempty) (hto : IsOpen[inst] (↑t : Set X))
  (hts' : ¬(↑t : Set X) = (↑s : Set X)), ∃ t ⊂ s, t.Nonempty ∧ IsOpen[inst] (↑t : Set X)
Tactic: lift t to Finset X using s.finite_toSet.subset hts
Cleared hypotheses: t, hts, htne, hto, hts'
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
⊢ T0Space X
have refine : ∀ (x y : X) (hxy : Inseparable x y), x = y
Tactic: refine ⟨fun x y hxy => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
x y : X
hxy : Inseparable x y
⊢ x = y
have rcases : ∀ (s : Set X) (hxs : x ∈ s) (hys : y ∈ s) (hs : T0Space.{u_1} (↑s : Type u_1)), x = y
Tactic: rcases h x y hxy with ⟨s, hxs, hys, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
x y : X
hxy : Inseparable x y
s : Set X
hxs : x ∈ s
hys : y ∈ s
hs : T0Space.{u_1} (↑s : Type u_1)
⊢ x = y
have lift : ∀ (x : { x : X // x ∈ s }) (hxy : Inseparable (↑x : X) y), (↑x : X) = y
Tactic: lift x to s using hxs
Cleared hypotheses: x, hxy, hxs
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
y : X
s : Set X
hys : y ∈ s
hs : T0Space.{u_1} (↑s : Type u_1)
x : { x : X // x ∈ s }
hxy : Inseparable (↑x : X) y
⊢ (↑x : X) = y
have lift : ∀ (y : { x : X // x ∈ s }) (hxy : Inseparable (↑x : X) (↑y : X)), (↑x : X) = (↑y : X)
Tactic: lift y to s using hys
Cleared hypotheses: y, hys, hxy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ (s : Set X), x ∈ s ∧ y ∈ s ∧ T0Space.{u_1} (↑s : Type u_1)
s : Set X
hs : T0Space.{u_1} (↑s : Type u_1)
x y : { x : X // x ∈ s }
hxy : Inseparable (↑x : X) (↑y : X)
⊢ (↑x : X) = (↑y : X)
have hxy₁ : Inseparable x y
Tactic: rw [← subtype_inseparable_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
⊢ closure[inst] {x} = (𝓝 x).ker
have h : ∀ (x_1 : X), Membership.mem (γ := Set X) (closure[inst] {x}) x_1 ↔ x_1 ∈ (𝓝 x).ker
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
⊢ IsCompact (X := X) (closure[inst] {x})
have refine : ∀ {ι : Type u_1} (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen[inst] (U i))
  (hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)),
  ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)
Tactic: refine isCompact_of_finite_subcover fun U hUo hxU ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
⊢ ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)
have obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)
Tactic: obtain ⟨i, hi⟩ : ∃ i, x ∈ U i := mem_iUnion.1 <| hxU <| subset_closure rfl
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
i : ι
hi : x ∈ U i
⊢ ∃ (t : Finset ι), Subset (α := Set X) (closure[inst] {x}) (⋃ i ∈ t, U i)
have refine : ∀ (y : X) (hy : Membership.mem (γ := Set X) (closure[inst] {x}) y),
  Membership.mem (γ := Set X) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Finset ι) {i} i_1), U i_1) y
Tactic: refine ⟨{i}, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : R0Space X
x : X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hxU : Subset (α := Set X) (closure[inst] {x}) (⋃ (i : ι), U i)
i : ι
hi : x ∈ U i
y : X
hy : Membership.mem (γ := Set X) (closure[inst] {x}) y
⊢ Membership.mem (γ := Set X) (⋃ (i_1 : ι), ⋃ (_ : Membership.mem (γ := Finset ι) {i} i_1), U i_1) y
have hy₁ : y ⤳ x
Tactic: rw [← specializes_iff_mem_closure, specializes_comm] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ 𝓝[s \ {y}] x = 𝓝[s] x
have rw : {y}ᶜ ∈ 𝓝[s] x
Tactic: rw [diff_eq, inter_comm, nhdsWithin_inter_of_mem]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
have inl : 𝓝[≠] x ≤ 𝓝[≠] x
Tactic: rcases eq_or_ne x y with rfl | hy
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
inl : 𝓝[≠] x ≤ 𝓝[≠] x
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
have inr : ∀ (hy : x ≠ y), 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
Tactic: rcases eq_or_ne x y with rfl | hy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
have inr : 𝓝[≠] x ≤ 𝓝 x
Tactic: rw [Ne.nhdsWithin_compl_singleton hy]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
⊢ IsOpen[inst] {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
have refine : ∀ (a : X) (ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a),
  {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a
Tactic: refine isOpen_iff_mem_nhds.mpr fun a ha => ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
⊢ {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a
have h : ∀ (b : X) (hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x), ∀ᶠ (y : X) in 𝓝[≠] b, p y
Tactic: filter_upwards [eventually_nhds_nhdsWithin.mpr ha] with b hb
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
have h : ∀ (hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x), ∀ᶠ (y : X) in 𝓝[≠] a, p y
Tactic: rcases eq_or_ne a b with rfl | h
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : ∀ (hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x), ∀ᶠ (y : X) in 𝓝[≠] a, p y
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
have h₁ : ∀ (h : a ≠ b), ∀ᶠ (y : X) in 𝓝[≠] b, p y
Tactic: rcases eq_or_ne a b with rfl | h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
p : X → Prop
a : X
ha : Membership.mem (γ := Set X) {x : X | ∀ᶠ (y : X) in 𝓝[≠] x, p y} a
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
have hb₁ : ∀ᶠ (x : X) in 𝓝 b, p x
Tactic: rw [h.symm.nhdsWithin_compl_singleton] at hb
Cleared hypotheses: hb, h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst] s
have rw : IsClosed[inst] (⋃ x ∈ s, {x})
Tactic: rw [← biUnion_of_singleton s]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a
have rcases : ∀ (a : Set X) (ab : a ∈ b) (xa : x ∈ a) (ha : a ⊆ {y_1 : X | y_1 ≠ y}), ∃ a ∈ b, x ∈ a ∧ y ∉ a
Tactic: rcases hb.isOpen_iff.1 isOpen_ne x h with ⟨a, ab, xa, ha⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
Tactic: tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
Tactic: tfae_have 2 ↔ 3 := by
    simp only [isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
have refine : (∀ (b a : X), a ≠ b → {b}ᶜ ∈ 𝓝 a) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
Tactic: refine forall_comm.trans ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
Tactic: tfae_have 5 ↔ 3 := by
    refine forall_comm.trans ?_
    simp only [isOpen_iff_mem_nhds, mem_compl_iff, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst] {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed[inst] {x}) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen[inst] {x}ᶜ
⊢ [T1Space X, ∀ (x : X), IsClosed[inst] {x}, ∀ (x : X), IsOpen[inst] {x}ᶜ,
      Continuous[inst, _] (⇑CofiniteTopology.of : (a : X) → CofiniteTopology X), ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
have tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
Tactic: tfae_have 5 ↔ 6 := by
    simp only [← subset_compl_singleton_iff, exists_mem_subset_iff]