mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cofinite

Tactic:
]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
]

Goal state after:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝 b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed[inst✝] z₁
x✝ : IsClosed[inst✝] z₂
⊢ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst✝¹] (⋃ x ∈ s, {x})

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Finite
⊢ IsClosed[inst✝¹] (⋃ x ∈ s, {x})
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := ⋯
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ Sᶜ ∈ opens ∧ ∀ s ∈ c, s ⊆ Sᶜ

Tactic:
refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩

Goal state after:
case h
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ Sᶜᶜ.Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
a : Set X
ab : a ∈ b
xa : x ∈ a
ha : a ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a

Tactic:
exact ⟨a, ab, xa, fun h => ha h rfl⟩

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ S.Nonempty

Tactic:
]

Goal state after:
case h
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ S.Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U s : Set X
h : sᶜ ∈ codiscreteWithin U
⊢ ∀ x ∈ (sᶜ ∪ Uᶜ)ᶜ, 𝓝[≠] x ⊓ 𝓟 (sᶜ ∪ Uᶜ)ᶜ = ⊥
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst✝¹] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst✝¹] V'
this : V'ᶜ = U
⊢ V' = V'

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
⊢ (∀ (U : Set X), IsOpen[inst✝] U → (univ ∩ U).Nonempty → univ ⊆ closure[inst✝] (univ ∩ U)) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst✝] U → U.Nonempty → Dense U

Tactic:
]

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
⊢ (∀ (U : Set X), IsOpen[inst✝] U → (univ ∩ U).Nonempty → univ ⊆ closure[inst✝] (univ ∩ U)) ↔
    ∀ ⦃U : Set X⦄, IsOpen[inst✝] U → U.Nonempty → Dense U
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ S
hZW : Z ⊆ W
⊢ Z ∈ S

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ S
hZW : Z ⊆ W
⊢ Z ∈ S
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ S
hZW : Z ⊆ W
⊢ W ∈ S

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
Z : Set X
hZ : Z ∈ irreducibleComponents X
S : Set (Set X)
hS : S.Finite
hSα : S ⊆ irreducibleComponents X
hZS : Z ⊆ ⋃₀ S
W : Set X
hWS : W ∈ S
hZW : Z ⊆ W
⊢ W ∈ S
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: 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 ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ

Tactic:
]

Goal state after:
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 ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ ⋃₀ (irreducibleComponents X \ {⋃₀ {Z}} ∪ {Z}) = univ

Tactic:
Set.sUnion_singleton,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ ⋃₀ (irreducibleComponents X \ {Z} ∪ {Z}) = univ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ univ = univ

pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ {Z} ⊆ irreducibleComponents X

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ {Z} ⊆ irreducibleComponents X
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
⊢ ∀ x ∈ (U \ s)ᶜ, ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
⊢ ∀ x ∈ (U \ s)ᶜ, ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ Z ∈ irreducibleComponents X

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ Z ∈ irreducibleComponents X
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap π
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q | π q.1 = π q.2}

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap π
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y) ↔ IsClosed[instTopologicalSpaceProd] {q | π q.1 = π q.2}
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₁
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z

Tactic:
]

Goal state after:
case h₁
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)

Tactic:
]

Goal state after:
case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂.hU
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsClosed[inst✝] (⋃ i ∈ irreducibleComponents X \ {Z}, i)

Tactic:
]

Goal state after:
case h₂.hU
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsClosed[inst✝] (⋃ i ∈ irreducibleComponents X \ {Z}, i)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case pos
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
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ

Tactic:
]

Goal state after:
case pos
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
⊢ ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂.h
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})

Tactic:
]

Goal state after:
case h₂.h
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ ¬Z ⊆ ⋃₀ (irreducibleComponents X \ {Z})
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst✝] (V ∩ {x | IsPreirreducible (f ⁻¹' {x})})
⊢ IsPreirreducible (f ⁻¹' V)

Tactic:
rintro U₁ U₂ hU₁ hU₂ ⟨x, hxV, hxU₁⟩ ⟨y, hyV, hyU₂⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
V : Set Y
hV : IsPreirreducible V
f : X → Y
hf' : IsOpenMap f
hf'' : V ⊆ closure[inst✝] (V ∩ {x | IsPreirreducible (f ⁻¹' {x})})
U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
x : X
hxV : x ∈ f ⁻¹' V
hxU₁ : x ∈ U₁
y : X
hyV : y ∈ f ⁻¹' V
hyU₂ : y ∈ U₂
⊢ (f ⁻¹' V ∩ (U₁ ∩ U₂)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case inr
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}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' sᶜ)ᶜ

Tactic:
]

Goal state after:
case inr
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}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
H : T1Space X
s : Set (CofiniteTopology X)
hs : sᶜ.Finite
⊢ IsOpen[inst✝] (⇑CofiniteTopology.of ⁻¹' sᶜ)ᶜ
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Tactic:
]

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F

Tactic:
]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (?m.12 ⁻¹' univ)

pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Type ?u.22

pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Y → ?m.11

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (?m.12 ⁻¹' univ)

X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Type ?u.22

X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Y → ?m.11
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible univ

Tactic:
rw [← Set.preimage_univ]
    exact .preimage PreirreducibleSpace.isPreirreducible_univ hf

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
f : Ultrafilter X
hx : f.lim ∈ U
h : ↑f ≤ 𝓝 x
⊢ U ∈ f

Tactic:
]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
x : X
f : Ultrafilter X
hx : f.lim ∈ U
h : ↑f ≤ 𝓝 x
⊢ U ∈ f
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
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
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ

Tactic:
]

Goal state after:
case neg
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
⊢ ∃ v ∈ 𝓝 x, ∀ y ∈ v, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ⊆ u
⊢ t ⊆ closure[inst✝¹] (t ∩ range f)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : t ∈ irreducibleComponents X
f : Y → X
hf₁ : Continuous[inst✝, inst✝¹] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : X), IsPreirreducible (f ⁻¹' {x})
h : (t ∩ range f).Nonempty
u : Set Y
hu : IsIrreducible u
htu : f ⁻¹' t ⊆ u
⊢ t ⊆ closure[inst✝¹] (t ∩ range f)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
this : f ⁻¹' Z ⊆ V
⊢ f '' f ⁻¹' Z ⊆ f '' V

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
this : f ⁻¹' Z ⊆ V
⊢ f '' f ⁻¹' Z ⊆ f '' V
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hU : ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
hs : Finite ↑s
⊢ ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s

Tactic:
]

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hU : ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
hs : Finite ↑s
⊢ ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
⊢ Pairwise fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
⊢ Pairwise fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h.left
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsClosed[inst✝¹] (s \ {x} ∪ tᶜ)

Tactic:
]

Goal state after:
case h.left
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hs : Finite ↑s
t : Set X
ht : IsOpen[inst✝¹] t
h₁ts : x ∈ t
h₂ts : t ∩ {x}ᶜ ⊆ U
⊢ IsClosed[inst✝¹] (s \ {x} ∪ tᶜ)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: 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}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of
h : Continuous[inst✝, _] ⇑CofiniteTopology.of
x : X
⊢ IsClosed[inst✝] (⇑CofiniteTopology.of ⁻¹' ⇑CofiniteTopology.of '' {x})

Tactic:
]

Goal state after:
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}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous[inst✝, _] ⇑CofiniteTopology.of
h : Continuous[inst✝, _] ⇑CofiniteTopology.of
x : X
⊢ IsClosed[inst✝] (⇑CofiniteTopology.of ⁻¹' ⇑CofiniteTopology.of '' {x})
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (f '' univ)
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
i✝ : T2Quotient X
x : X
j✝ : T2Quotient X
y : X
h : ¬mk x = mk y
s : Setoid X
hs : T2Space (Quotient s)
hsxy : ⟦x⟧ ≠ ⟦y⟧
⊢ s ∈ {s | T2Space (Quotient s)}

Tactic:
exact hs

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : IrreducibleSpace X
⊢ IsPreirreducible (f '' univ)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
hf : Surjective f
inst✝ : IrreducibleSpace X
⊢ IsPreirreducible (f '' univ)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite