awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
a : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) → Disjoint (𝓝[≠] x) (𝓟 S)
a₁ : Disjoint (𝓝[≠] x) (𝓟 S) → (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
constructor
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
pos : ∀ (hx : x ∈ S), Disjoint (𝓝[≠] x) (𝓟 S)
neg : ∀ (hx : x ∉ S), Disjoint (𝓝[≠] x) (𝓟 S)
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
by_cases hx : x ∈ S
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
hx : x ∈ S
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
H.2 hx

Premises used: And.right
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
hx : x ∉ S
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
(H.1 hx).mono_left nhdsWithin_le_nhds

Premises used: Disjoint.mono_left, nhdsWithin_le_nhds, And.left
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
hx : x ∈ S
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
exacts [H.2 hx, (H.1 hx).mono_left nhdsWithin_le_nhds]

Premises used: And.right
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Tactic:
⟨fun hx ↦ ?_, fun _ ↦ H⟩

Premises used: And.intro
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
a : ∀ (hx : x ∉ S), Disjoint (𝓝 x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Tactic:
refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
hx : x ∉ S
⊢ Disjoint (𝓝 x) (𝓟 S)

Tactic:
simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H

Premises used: nhdsWithin, disjoint_iff, inf_assoc
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
simp :
  (∀ (i : X) (i_1 : i ∈ T), ∃ (u : Set X), IsOpen[inst] u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
    ∀ x ∈ T, ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))

Tactic:
simp only [codiscreteWithin, mem_iSup, mem_nhdsWithin, disjoint_principal_right, subset_def,
    mem_diff, mem_inter_iff, mem_compl_iff]

Premises used: Set.subset_def, Set.mem_inter_iff, Filter.mem_iSup, mem_nhdsWithin, Set.mem_diff, Filter.codiscreteWithin, Set.mem_compl_iff, Filter.disjoint_principal_right
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
a : ∀ (x : X) (u : Set X) (y : X), y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
⊢ (∀ (i : X) (i_1 : i ∈ T), ∃ (u : Set X), IsOpen[inst] u ∧ i ∈ u ∧ ∀ (x : X), x ∈ u ∧ x ∈ T ∧ x ∉ {i} → x ∈ S) ↔
    ∀ x ∈ T, ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ ∀ (x_1 : X), x_1 ∈ u ∧ x_1 ∉ {x} → ¬(x_1 ∈ T ∧ x_1 ∉ S)

Tactic:
congr! 7 with x - u y
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
x : X
u : Set X
y : X
a : (y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₁ : (y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₂ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₃ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₄ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₅ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₆ : ¬(y ∈ u ∧ y ∈ T ∧ y ∉ {x}) → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₇ : y ∈ S → y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)
a₈ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₉ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₀ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₁ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₂ : ¬(y ∈ u ∧ y ∉ {x}) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₃ : ¬(y ∈ T ∧ y ∉ S) → y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S
a₁₄ : y ∉ u → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₅ a₁₆ a₁₇ : ¬(y ∈ T ∧ y ∉ {x}) → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₈ : y ∈ S → y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → False
a₁₉ : y ∉ u → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₀ : ¬y ∉ {x} → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₁ : y ∉ T → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₂ a₂₃ a₂₄ : ¬y ∉ S → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
a₂₅ : y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → y ∉ T → False
a₂₆ : y ∈ u → y ∉ {x} → y ∈ T → y ∉ S → ¬y ∉ {x} → False
a₂₇ a₂₈ a₂₉ : y ∈ S → y ∈ u → y ∈ T → y ∉ {x} → y ∈ S
⊢ y ∈ u ∧ y ∈ T ∧ y ∉ {x} → y ∈ S ↔ y ∈ u ∧ y ∉ {x} → ¬(y ∈ T ∧ y ∉ S)

Tactic:
tauto
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
simp_rw : (∀ x ∈ T, Disjoint (𝓝[≠] x) (𝓟 (T \ S))) ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x
simp_rw₁ : (∀ x ∈ T, (T \ S)ᶜ ∈ 𝓝[≠] x) ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, S ∪ Tᶜ ∈ 𝓝[≠] x

Tactic:
simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff]

Premises used: mem_codiscreteWithin, Set.compl_diff, Filter.disjoint_principal_right
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, ¬AccPt x (𝓟 (T \ S))

Tactic:
simp only [mem_codiscreteWithin, disjoint_iff, AccPt, not_neBot]

Premises used: disjoint_iff, mem_codiscreteWithin, AccPt, Filter.not_neBot
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
⊢ U ∈ codiscreteWithin U

Tactic:
simp [mem_codiscreteWithin]

Premises used: mem_codiscreteWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
⊢ codiscreteWithin U₁ ≤ codiscreteWithin U

Tactic:
(biSup_mono hU).trans <| iSup₂_mono fun _ _ ↦ ?_

Premises used: iSup₂_mono, Set.Mem, biSup_mono, setOf, LE.le.trans
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
refine : ∀ x ∈ U, 𝓝[U₁ \ {x}] x ≤ 𝓝[U \ {x}] x
⊢ codiscreteWithin U₁ ≤ codiscreteWithin U

Tactic:
refine (biSup_mono hU).trans <| iSup₂_mono fun _ _ ↦ ?_

Premises used: iSup₂_mono, biSup_mono, LE.le.trans
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
x : X
h : x ∈ U
⊢ 𝓝[U₁ \ {x}] x ≤ 𝓝[U \ {x}] x

Tactic:
gcongr
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ s ∩ U = (sᶜ ∪ Uᶜ)ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
rw : ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥
⊢ IsDiscrete (s ∩ U)

Tactic:
rw [(by simp : ((s ∩ U) : Set X) = ((sᶜ ∪ Uᶜ)ᶜ : Set X)), isDiscrete_iff_nhdsNE]

Premises used: isDiscrete_iff_nhdsNE
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
simp_rw : ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, sᶜ ∪ Uᶜ ∈ 𝓝[≠] x
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥

Tactic:
simp_rw [← Filter.mem_iff_inf_principal_compl]

Premises used: Filter.mem_iff_inf_principal_compl
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, sᶜ ∪ Uᶜ ∈ 𝓝[≠] x

Tactic:
simp_all [← Set.compl_diff, mem_codiscreteWithin]

Premises used: mem_codiscreteWithin, Set.compl_diff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
simp : (∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
simp only [mem_codiscreteWithin, disjoint_principal_right]

Premises used: mem_codiscreteWithin, Filter.disjoint_principal_right
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
h : ∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x
z : X
hz : z ∈ U
⊢ (U \ s)ᶜ ∩ (U \ s) = ∅

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
refine : ∀ (h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) (z : X) (hz : z ∈ U), (U \ s)ᶜ ∈ 𝓝[≠] z
⊢ (∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
refine ⟨fun h z hz ↦ ⟨(U \ s)ᶜ, h z hz, by simp⟩, fun h z hz ↦ ?_⟩
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
rw : ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
⊢ (U \ s)ᶜ ∈ 𝓝[≠] z

Tactic:
rw [← exists_mem_subset_iff]

Premises used: Filter.exists_mem_subset_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
obtain : ∀ (t : Set X) (h₁t : t ∈ 𝓝[≠] z) (h₂t : t ∩ (U \ s) = ∅), ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
⊢ ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := h z hz
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
w : Set X
left : t ∈ 𝓝[≠] z
right : t ⊆ (U \ s)ᶜ
⊢ ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ

Tactic:
use t, h₁t, (disjoint_iff_inter_eq_empty.mpr h₂t).subset_compl_right

Premises used: Iff.mpr, Disjoint.subset_compl_right, Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
rw : ∀ x ∈ (U \ s)ᶜ, ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
⊢ IsClosed[inst] (U \ s)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_eventually]

Premises used: isOpen_iff_eventually, isOpen_compl_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
pos : ∀ (h₁x : x ∈ U), ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
neg : ∀ (h₁x : x ∉ U), ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
by_cases h₁x : x ∈ U
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
pos :
  ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))) (hU : IsClosed[inst] U) (x : X) (hx : x ∈ (U \ s)ᶜ) (h₁x : x ∈ U),
    ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
rw [mem_codiscreteWithin] at hs

Premises used: mem_codiscreteWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
h : ∀ (a : X), (Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s) → a ∈ (U \ s)ᶜ
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
filter_upwards [eventually_nhdsWithin_iff.1 (disjoint_principal_right.1 (hs x h₁x))]

Premises used: eventually_nhdsWithin_iff, Iff.mp, Filter.disjoint_principal_right
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s
pos : ∀ (h₂a : a = x), a ∈ (U \ s)ᶜ
neg : ∀ (h₂a : ¬a = x), a ∈ (U \ s)ᶜ
⊢ a ∈ (U \ s)ᶜ

Tactic:
by_cases h₂a : a = x
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s
h₂a : a = x
pos pos₁ :
  ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U ∩ sᶜ))) (hU : IsClosed[inst] U) (hx : ¬(True ∧ x ∉ s)) (h₁x : x ∈ U)
    (ha : x ∉ {x} → ¬False) (h₂a : a = x), ¬False
pos₂ pos₃ :
  ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U ∩ sᶜ))) (hU : IsClosed[inst] U) (hx : ¬(True ∧ x ∉ s)) (h₁x : x ∈ U)
    (ha : x ∉ {x} → ¬False) (h₂a : a = x), False → False
⊢ a ∈ (U \ s)ᶜ

Tactic:
tauto_set
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : Membership.mem (γ := Set X) {x}ᶜ a → a ∉ U \ s
h₂a : ¬a = x
⊢ a ∉ U \ s

Tactic:
specialize ha h₂a
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
h₂a : ¬a = x
ha : a ∉ U \ s
neg neg₁ :
  ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U ∩ sᶜ))) (hU : IsClosed[inst] U) (hx : ¬(True ∧ x ∉ s)) (h₁x : x ∈ U)
    (h₂a : ¬a = x) (ha : ¬(a ∈ U ∧ a ∉ s)), ¬False
neg₂ neg₃ :
  ∀ (hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U ∩ sᶜ))) (hU : IsClosed[inst] U) (hx : ¬(True ∧ x ∉ s)) (h₁x : x ∈ U)
    (h₂a : ¬a = x) (ha : ¬(a ∈ U ∧ a ∉ s)), False → False
⊢ a ∈ (U \ s)ᶜ

Tactic:
tauto_set
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
neg : ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
rw [eventually_iff_exists_mem]

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
right : ∀ y ∈ Uᶜ, y ∈ (U \ s)ᶜ
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ

Tactic:
use Uᶜ, hU.compl_mem_nhds h₁x

Premises used: IsClosed.compl_mem_nhds
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
y : X
hy : y ∈ Uᶜ
right right₁ : ∀ (hx : ¬(False ∧ x ∉ s)) (h₁x : x ∉ U) (hy : y ∉ U), ¬(False ∧ y ∉ s)
right₂ right₃ : ∀ (hx : ¬(False ∧ x ∉ s)) (h₁x : x ∉ U) (hy : y ∉ U), False ∧ y ∉ s → False
⊢ y ∈ (U \ s)ᶜ

Tactic:
tauto_set
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hU : U ∈ 𝓝[≠] x
hs : Finite.{u_3 + 1} (↑s : Type u_3)
rw :
  ∀ (hU : ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U) (hs : Finite.{u_3 + 1} (↑s : Type u_3)),
    ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
⊢ U \ s ∈ 𝓝[≠] x

Tactic:
rw [mem_nhdsWithin] at hU ⊢

Premises used: mem_nhdsWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hU : ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
hs : Finite.{u_3 + 1} (↑s : Type u_3)
obtain :
  ∀ (t : Set X) (ht : IsOpen[inst] t) (h₁ts : x ∈ t) (h₂ts : t ∩ {x}ᶜ ⊆ U),
    ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s

Tactic:
obtain ⟨t, ht, h₁ts, h₂ts⟩ := hU
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
h : IsOpen[inst] (t \ (s \ {x})) ∧ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
⊢ ∃ (u : Set X), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s

Tactic:
use t \ (s \ {x})

Premises used: SDiff.sdiff, Singleton.singleton
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
h : IsOpen[inst] (t \ (s \ {x}))
h₁ : x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
⊢ IsOpen[inst] (t \ (s \ {x})) ∧ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s

Tactic:
constructor
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
h : IsClosed[inst] (s \ {x} ∪ tᶜ)
⊢ IsOpen[inst] (t \ (s \ {x}))

Tactic:
rw [← isClosed_compl_iff, compl_diff]

Premises used: Set.compl_diff, isClosed_compl_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsClosed[inst] (s \ {x} ∪ tᶜ)

Tactic:
s.toFinite.diff.isClosed.union (isClosed_compl_iff.2 ht)

Premises used: Iff.mpr, IsClosed.union, Set.Finite.diff, Set.toFinite, Set.Finite.isClosed, isClosed_compl_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsClosed[inst] (s \ {x} ∪ tᶜ)

Tactic:
exact s.toFinite.diff.isClosed.union (isClosed_compl_iff.2 ht)

Premises used: Iff.mpr, IsClosed.union, Set.Finite.diff, Set.toFinite, Set.Finite.isClosed, isClosed_compl_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
U s : Set X
hs : Finite.{u_3 + 1} (↑s : Type u_3)
t : Set X
ht : IsOpen[inst] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
h h₁ h₂ h₃ :
  ∀ (h₂ts : ∀ (x_1 : X), x_1 ∈ t ∧ x_1 ∉ {x} → x_1 ∈ U),
    (True ∧ ¬(x ∈ s ∧ x ∉ {x})) ∧ ∀ (x_1 : X), (x_1 ∈ t ∧ ¬(x_1 ∈ s ∧ x_1 ∉ {x})) ∧ x_1 ∉ {x} → x_1 ∈ U ∧ x_1 ∉ s
⊢ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s

Tactic:
tauto_set
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
rw : (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
rw [codiscreteWithin_iff_locallyEmptyComplementWithin]

Premises used: codiscreteWithin_iff_locallyEmptyComplementWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
mp : (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) → ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
mpr : (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite) → ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
constructor
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
mp : ∀ (t : Set X) (h₁t : t ∈ 𝓝[≠] z) (h₂t : t ∩ (U \ s) = ∅), ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
right : (insert z t ∩ (U \ s)).Finite
⊢ ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
use insert z t, insert_mem_nhds_iff.mpr h₁t

Premises used: Iff.mpr, Insert.insert, insert_mem_nhds_iff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
pos : ∀ (hz : z ∈ U \ s), (insert z t ∩ (U \ s)).Finite
neg : ∀ (hz : z ∉ U \ s), (insert z t ∩ (U \ s)).Finite
⊢ (insert z t ∩ (U \ s)).Finite

Tactic:
by_cases hz : z ∈ U \ s
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∈ U \ s
pos : Set.Finite (α := X) (insert z ∅)
⊢ (insert z t ∩ (U \ s)).Finite

Tactic:
rw [inter_comm, inter_insert_of_mem hz, inter_comm, h₂t]

Premises used: Set.inter_insert_of_mem, Set.inter_comm
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∈ U \ s
⊢ Set.Finite (α := X) (insert z ∅)

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
neg : Set.Finite.{u_1} (α := X) ∅
⊢ (insert z t ∩ (U \ s)).Finite

Tactic:
rw [inter_comm, inter_insert_of_notMem hz, inter_comm, h₂t]

Premises used: Set.inter_insert_of_notMem, Set.inter_comm
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
hz : z ∉ U \ s
⊢ Set.Finite.{u_1} (α := X) ∅

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
mpr : ∀ (t : Set X) (h₁t : t ∈ 𝓝 z) (h₂t : (t ∩ (U \ s)).Finite), ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := h z h₁z
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝 z
h₂t : (t ∩ (U \ s)).Finite
right : t \ (t ∩ (U \ s)) ∩ (U \ s) = ∅
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
use t \ (t ∩ (U \ s)), nhdsNE_of_nhdsNE_sdiff_finite (mem_nhdsWithin_of_mem_nhds h₁t) h₂t

Premises used: nhdsNE_of_nhdsNE_sdiff_finite, mem_nhdsWithin_of_mem_nhds, Inter.inter, SDiff.sdiff
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
z : X
h₁z : z ∈ U
t : Set X
h₁t : t ∈ 𝓝 z
h₂t : (t ∩ (U \ s)).Finite
⊢ t \ (t ∩ (U \ s)) ∩ (U \ s) = ∅

Tactic:
simp
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x : X
rw : ∀ z ∈ s, ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅
⊢ {x}ᶜ ∈ codiscreteWithin s

Tactic:
rw [codiscreteWithin_iff_locallyEmptyComplementWithin]

Premises used: codiscreteWithin_iff_locallyEmptyComplementWithin
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x z : X
hz : z ∈ s
h : univ \ {x} ∈ 𝓝[≠] z ∧ univ \ {x} ∩ (s \ {x}ᶜ) = ∅
⊢ ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅

Tactic:
use univ \ {x}

Premises used: Set.univ
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ univ \ {x} ∩ (s \ {x}ᶜ) = ∅

Tactic:
aesop
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x z : X
hz : z ∈ s
⊢ univ \ {x} ∈ 𝓝[≠] z ∧ univ \ {x} ∩ (s \ {x}ᶜ) = ∅

Tactic:
exact ⟨nhdsNE_of_nhdsNE_sdiff_finite univ_mem Finite.of_subsingleton, by aesop⟩
-- Module: Mathlib.Topology.DiscreteSubset
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
h : t.Finite
empty : ∅ᶜ ∈ codiscreteWithin s
insert :
  ∀ {a : X} {s_1 : Set X},
    a ∉ s_1 → ∀ (hs : s_1.Finite), s_1ᶜ ∈ codiscreteWithin s → (Insert.insert a s_1)ᶜ ∈ codiscreteWithin s
⊢ tᶜ ∈ codiscreteWithin s

Tactic:
apply h.induction_on (motive := fun t _ ↦ tᶜ ∈ codiscreteWithin s)

Premises used: Set.Finite.induction_on