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

Goal state before:
pp: β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

Tactic:
constructor

Goal state after:
case mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i

case mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i) →
    ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, IsTopologicalBasis (range b)

Tactic:
by
  obtain ⟨t, ht⟩ := TopologicalSpace.exists_countable_basis α
  by_cases! hn : t.Nonempty
  · obtain ⟨b, rfl⟩ := ht.1.exists_eq_range hn
    exact ⟨b, ht.2.2⟩
  · exact ⟨fun n => ∅, by simp_all⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]
  exact SecondCountableTopology.mk' <|
    countable_iUnion fun i => @countable_countableBasis _ (t i) (ht i)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u = ⋃ y ∈ T, a ↑y

Tactic:
hT

Goal state after:
case refine_2
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u = ⋃ i, a ↑i
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la lb.smallSets
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la lb.smallSets

Tactic:
rw [tendsto_smallSets_iff] at ht ⊢

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s → IsSigmaCompact (f '' s)

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact (f '' s) → IsSigmaCompact s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] x ⊓ comap f l

Tactic:
nhdsWithin

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝 x ⊓ 𝓟 s ⊓ comap f l
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = f <$> s <*> t

Tactic:
ext

Goal state after:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ f <$> s <*> t
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
s : Set α
t : Set ↑s
⊢ ⋃ x ∈ t, {↑x} = Subtype.val '' t

Tactic:
ext

Goal state after:
α : Type u
s : Set α
t : Set ↑s
x✝ : α
⊢ x✝ ∈ ⋃ x ∈ t, {↑x} ↔ x✝ ∈ Subtype.val '' t
Module: Mathlib.Data.Set.Functor

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
⊢ f '' Subtype.val '' γ = β.domRestrict f '' γ

Tactic:
ext

Goal state after:
α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
x✝ : δ
⊢ x✝ ∈ f '' Subtype.val '' γ ↔ x✝ ∈ β.domRestrict f '' γ
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ici a) = Ici (f a)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ici a)) ↔ x✝ ∈ ↑(Ici (f a))
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ioi a) = Ioi (f a)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ioi a)) ↔ x✝ ∈ ↑(Ioi (f a))
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ↑(upperClosure s) = ⋃ a ∈ s, Ici a

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(upperClosure s) ↔ x✝ ∈ ⋃ a ∈ s, Ici a
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f.symm).symm (upperClosure s)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
x✝ : β
⊢ x✝ ∈ ↑(upperClosure (⇑f '' s)) ↔ x✝ ∈ ↑((UpperSet.map f.symm).symm (upperClosure s))
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ⨅ a ∈ s, Ici a = upperClosure s

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨅ a ∈ s, Ici a) ↔ x✝ ∈ ↑(upperClosure s)
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ upperClosure {a} = UpperSet.Ici a

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Preorder α
a x✝ : α
⊢ x✝ ∈ ↑(upperClosure {a}) ↔ x✝ ∈ ↑(UpperSet.Ici a)
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s.erase a

Tactic:
simp [sdiff, erase]

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
⊢ (map f).symm = map f.symm

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x✝¹ : UpperSet β
x✝ : α
⊢ x✝ ∈ ↑((map f).symm x✝¹) ↔ x✝ ∈ ↑((map f.symm) x✝¹)
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ map (OrderIso.refl α) = OrderIso.refl (UpperSet α)

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : Preorder α
x✝¹ : UpperSet α
x✝ : α
⊢ x✝ ∈ ↑((map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑((OrderIso.refl (UpperSet α)) x✝¹)
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
⊢ (map g) ((map f) s) = (map (f.trans g)) s

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑((map g) ((map f) s)) ↔ x✝ ∈ ↑((map (f.trans g)) s)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).ker = {y | y ⤳ x}

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x x✝ : X
⊢ x✝ ∈ (𝓝 x).ker ↔ x✝ ∈ {y | y ⤳ x}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f✝ : X → Y
inst✝ : IndiscreteTopology X
f : Filter X
hf : f.NeBot
⊢ f ≤ 𝓟 univ → ∃ x ∈ univ, ClusterPt x f

Tactic:
simp [clusterPt_of_indiscreteTopology, nonempty_of_neBot f]

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s → ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ (∀ (i : ι), IsCompact (eval i '' s)) → IsCompact s
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ irreducibleComponents X ↔ s ∈ {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s}

Tactic:
constructor

Goal state after:
case mp
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ irreducibleComponents X → s ∈ {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s}

case mpr
X : Type u_3
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ {s | Maximal (fun x ↦ IsClosed[inst✝] x ∧ IsIrreducible x) s} → s ∈ irreducibleComponents X
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t) ↔ ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t) → ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s) → ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) → ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki) → ∃ K, IsCompact K ∧ s ⊆ K
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
⊢ closure[inst✝¹] {x} = (𝓝 x).ker

Tactic:
ext

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x x✝ : X
⊢ x✝ ∈ closure[inst✝¹] {x} ↔ x✝ ∈ (𝓝 x).ker
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}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋃₀ c)ᶜ = ⋂ U, (↑U)ᶜ

Tactic:
ext

Goal state after:
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
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
x✝ : X
⊢ x✝ ∈ (⋃₀ c)ᶜ ↔ x✝ ∈ ⋂ U, (↑U)ᶜ
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ 𝓝[s \ {y}] x = 𝓝[s] x

Tactic:
by
  rw [sdiff_eq, inter_comm, nhdsWithin_inter_of_mem]
  exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Goal state after:
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 → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
← disjoint_iff

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.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:
constructor

Goal state after:
case mp
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)

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ Disjoint (𝓝[≠] x) (𝓟 S) → (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T2Space X ↔ T0Space X

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T2Space X → T0Space X

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ T0Space X → T2Space X
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
⊢ T2Space (X ⊕ Y)

Tactic:
constructor

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
⊢ Pairwise fun x y ↦
    ∃ u v, IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
⊢ T2Space ((i : ι) × X i)

Tactic:
constructor

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
⊢ Pairwise fun x y ↦
    ∃ u v, IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case inr
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
i : ι
x : X i
j : ι
y : X j
ne : ⟨i, x⟩ ≠ ⟨j, y⟩
h : i ≠ j
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨j, y⟩ ∈ v ∧ Disjoint u v

Tactic:
let _ := (⊥ : TopologicalSpace ι); have : DiscreteTopology ι := ⟨rfl⟩
    exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h
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
⊢ IsOpen[inst✝¹] (t \ (s \ {x})) ∧ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s

Tactic:
constructor

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
⊢ IsOpen[inst✝¹] (t \ (s \ {x}))

case h.right
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
⊢ x ∈ t \ (s \ {x}) ∧ t \ (s \ {x}) ∩ {x}ᶜ ⊆ U \ s
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:
constructor

Goal state after:
case mp
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

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite) → ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact s ↔ IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
constructor

Goal state after:
case mp
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ IsCompact s → IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_4
X : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), T2Space (X i)
s : Set ((i : ι) → X i)
⊢ (IsClosed[topologicalSpace] s ∧ ∀ (i : ι), IsCompact (eval i '' s)) → IsCompact s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t) ∧ (True ∨ x ∈ s ↔ True ∨ x ∈ t)

Tactic:
true_or,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t) ∧ True
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ f x ≠ g x ↔ ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ f x ≠ g x → ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x

case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ (∀ᶠ (x : X) in 𝓝 x, f x ≠ g x) → f x ≠ g x
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g

case mpr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ IsPreirreducible S → ∀ x ∈ S, S ⊆ closure[inst✝¹] {x}

case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
⊢ (∀ x ∈ S, S ⊆ closure[inst✝¹] {x}) → IsPreirreducible S
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x

Tactic:
· intro h
    filter_upwards [h] with _ hy
    exact eventually_nhdsWithin_of_eventually_nhds hy

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ ∀ᶠ (x : X) in 𝓝[s] p, x ⤳ p

Tactic:
by
  obtain ⟨t, h₁t, h₂t⟩ := disjoint_cofinite_right.mp hs
  set S := {y ∈ t ∩ s | ¬(y ⤳ p)}
  have hS_nhds (y) (hy : y ∈ S) : (closure ({y} : Set X))ᶜ ∈ 𝓝 p :=
    isClosed_closure.isOpen_compl.mem_nhds <| by
      simpa [specializes_iff_mem_closure] using hy.2
  filter_upwards [h₁t, nhdsWithin_le_nhds ((biInter_mem <| h₂t.subset (by grind)).mpr hS_nhds),
    self_mem_nhdsWithin] with x hxt hxS
  contrapose
  refine fun hxp hxf ↦ mem_iInter₂.mp hxS x ⟨⟨hxt, hxf⟩, hxp⟩ ?_
  grind [subset_closure]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓟 {x | x ⤳ p} ⊓ 𝓟 s ≤ 𝓝[s] p

Tactic:
nhdsWithin

Goal state after:
case a
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓟 {x | x ⤳ p} ⊓ 𝓟 s ≤ 𝓝 p ⊓ 𝓟 s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ closure[inst✝¹] K = ⋃ x ∈ K, {y | Inseparable x y}

Tactic:
ext

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
x✝ : X
⊢ x✝ ∈ closure[inst✝¹] K ↔ x✝ ∈ ⋃ x ∈ K, {y | Inseparable x y}
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot ↔ ¬IsBot a

Tactic:
constructor

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot → ¬IsBot a

case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot