awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
h₁ : ∀ (a : X) (hy : ∀ᶠ (x : X) in 𝓝 a, p x), ∀ᶠ (x : X) in 𝓝[s] a, p x
⊢ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x

Tactic:
filter_upwards [h] with _ hy
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
a_1 : X
hy : ∀ᶠ (x : X) in 𝓝 a_1, p x
⊢ ∀ᶠ (x : X) in 𝓝[s] a_1, p x

Tactic:
eventually_nhdsWithin_of_eventually_nhds hy

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
a_1 : X
hy : ∀ᶠ (x : X) in 𝓝 a_1, p x
⊢ ∀ᶠ (x : X) in 𝓝[s] a_1, p x

Tactic:
exact eventually_nhdsWithin_of_eventually_nhds hy

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
a_1 : X
h₁ : (∀ᶠ (x : X) in 𝓝[s] a_1, p x) → a_1 ∈ s → ∀ᶠ (x : X) in 𝓝 a_1, p x
⊢ (∀ᶠ (x : X) in 𝓝[s] a_1, p x) → a_1 ∈ s → ∀ᶠ (x : X) in 𝓝 a_1, p x

Tactic:
_
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
a_1 : X
h_1 : ∀ᶠ (x : X) in 𝓝[s] a_1, p x
h₁ : a_1 ∈ s → ∀ᶠ (x : X) in 𝓝 a_1, p x
⊢ a_1 ∈ s → ∀ᶠ (x : X) in 𝓝 a_1, p x

Tactic:
_
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
h₁ : ∀ (a : X), (∀ᶠ (x : X) in 𝓝[s] a, p x) → a ∈ s → ∀ᶠ (x : X) in 𝓝 a, p x
⊢ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x

Tactic:
filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
a_1 : X
h_1 : ∀ᶠ (x : X) in 𝓝[s] a_1, p x
h_2 : a_1 ∈ s
⊢ ∀ᶠ (x : X) in 𝓝 a_1, p x

Tactic:
simp_all [IsOpen.nhdsWithin_eq]

Premises used: IsOpen.nhdsWithin_eq
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
a : X
p : X → Prop
⊢ (∀ᶠ (y : X) in 𝓝[≠] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (x : X) in 𝓝[≠] a, p x

Tactic:
eventually_nhdsWithin_eventually_nhds_iff_of_isOpen isOpen_ne

Premises used: eventually_nhdsWithin_eventually_nhds_iff_of_isOpen, isOpen_ne
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x y : X
s : Set X
f : X → Y
inl : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x
inr : ∀ (h : x ≠ y), ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x

Tactic:
rcases eq_or_ne x y with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Tactic:
continuousWithinAt_insert_self

Premises used: continuousWithinAt_insert_self
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Tactic:
exact continuousWithinAt_insert_self

Premises used: continuousWithinAt_insert_self
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x y : X
s : Set X
f : X → Y
rw : ContinuousWithinAt f (insert y (s \ {y})) x ↔ ContinuousWithinAt f s x
rw₁ : X
rw₂ : ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
rw₃ rw₄ : ContinuousWithinAt f s x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x

Tactic:
rw [← continuousWithinAt_insert, insert_diff_singleton, continuousWithinAt_insert]

Premises used: continuousWithinAt_insert, Set.insert_diff_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
rw : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
rw [← continuousWithinAt_insert_self (s := s), ← continuousWithinAt_insert_self (s := t)]

Premises used: continuousWithinAt_insert_self
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x

Tactic:
continuousWithinAt_congr_set (eventuallyEq_insert h)

Premises used: eventuallyEq_insert, continuousWithinAt_congr_set
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x

Tactic:
exact continuousWithinAt_congr_set (eventuallyEq_insert h)

Premises used: eventuallyEq_insert, continuousWithinAt_congr_set
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
s : Set X
x : X
c : Y
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst] s
ht : ∀ y ∈ s, f y = c
rw : Membership.mem (γ := Set Y) (closure[inst_1] {c}) (f x)
⊢ f x = c

Tactic:
rw [← Set.mem_singleton_iff, ← closure_singleton]

Premises used: closure_singleton, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
s : Set X
x : X
c : Y
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst] s
ht : ∀ y ∈ s, f y = c
⊢ Membership.mem (γ := Set Y) (closure[inst_1] {c}) (f x)

Tactic:
h.mem_closure hx ht

Premises used: ContinuousWithinAt.mem_closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
s : Set X
x : X
c : Y
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst] s
ht : ∀ y ∈ s, f y = c
⊢ Membership.mem (γ := Set Y) (closure[inst_1] {c}) (f x)

Tactic:
exact h.mem_closure hx ht
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
s : Set X
c : Y
h : ∀ x ∈ closure[inst] s, ContinuousWithinAt f s x
ht : EqOn f (fun (x : X) ↦ c) s
x : X
hx : x ∈ closure[inst] s
⊢ f x = (fun (x : X) ↦ c) x

Tactic:
apply ContinuousWithinAt.eq_const_of_mem_closure (h x hx) hx ht

Premises used: ContinuousWithinAt.eq_const_of_mem_closure
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
rwa : Tendsto f (𝓝 x) (𝓝 (f x))
rwa₁ rwa₂ rwa₃ rwa₄ : Tendsto f (𝓝 x) (𝓝 y)
⊢ ContinuousAt f x

Tactic:
rwa [ContinuousAt, eq_of_tendsto_nhds h]

Premises used: ContinuousAt, eq_of_tendsto_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
l : Filter Y
inst_2 : l.NeBot
c d : X
simp_rw : map (fun (x : Y) ↦ c) l ≤ 𝓝 d ↔ c = d
simp_rw₁ : pure c ≤ 𝓝 d ↔ c = d
⊢ Tendsto (fun (x : Y) ↦ c) l (𝓝 d) ↔ c = d

Tactic:
simp_rw [Tendsto, Filter.map_const, pure_le_nhds_iff]

Premises used: Filter.map_const, Filter.Tendsto, pure_le_nhds_iff
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ {x} ⊆ s

Tactic:
simp only [singleton_subset_iff, mem_of_mem_nhds hs]

Premises used: Set.singleton_subset_iff, mem_of_mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ {x} ⊆ s

Tactic:
have A : {x} ⊆ s := by simp only [singleton_subset_iff, mem_of_mem_nhds hs]
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
⊢ IsClosed[inst] (s \ {x})

Tactic:
have B : IsClosed (s \ {x}) := (hsf.subset diff_subset).isClosed
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
⊢ (s \ {x})ᶜ ∈ 𝓝 x

Tactic:
have C : (s \ {x})ᶜ ∈ 𝓝 x := B.isOpen_compl.mem_nhds fun h => h.2 rfl
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ {x} ∈ 𝓝 x

Tactic:
simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C

Premises used: Filter.inter_mem, Set.diff_eq, Set.diff_diff_cancel_left
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ {x} ∈ 𝓝 x

Tactic:
have D : {x} ∈ 𝓝 x := by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
rwa : ∀ (D : Membership.mem (γ := Set X) (interior {x}) x), IsOpen[inst] {x}
rwa₁ : ∀ (D : Subset (α := Set X) {x} (interior {x})), IsOpen[inst] {x}
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (D : IsOpen[inst] {x}), IsOpen[inst] {x}
⊢ IsOpen[inst] {x}

Tactic:
rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D

Premises used: subset_interior_iff_isOpen, Set.singleton_subset_iff, mem_interior_iff_mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
⊢ s.Infinite

Tactic:
fun hsf => hx.1 ?_

Premises used: Filter.NeBot.ne', Not, Set.Infinite
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
refine : ∀ (hsf : s.Finite), 𝓝[≠] x = ⊥
⊢ s.Infinite

Tactic:
refine fun hsf => hx.1 ?_

Premises used: Filter.NeBot.ne'
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
rw : IsOpen[inst] {x}
⊢ 𝓝[≠] x = ⊥

Tactic:
rw [← isOpen_singleton_iff_punctured_nhds]

Premises used: isOpen_singleton_iff_punctured_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen[inst] {x}

Tactic:
isOpen_singleton_of_finite_mem_nhds x hs hsf

Premises used: isOpen_singleton_of_finite_mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen[inst] {x}

Tactic:
exact isOpen_singleton_of_finite_mem_nhds x hs hsf

Premises used: isOpen_singleton_of_finite_mem_nhds
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : Finite X
⊢ DiscreteTopology X

Tactic:
discreteTopology_iff_forall_isClosed.mpr (·.toFinite.isClosed)

Premises used: Iff.mpr, Set.toFinite, discreteTopology_iff_forall_isClosed, Set.Finite.isClosed
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
hs : s.Finite
⊢ IsDiscrete s

Tactic:
⟨@Finite.instDiscreteTopology _ _ _ hs.to_subtype⟩

Premises used: Finite.instDiscreteTopology, IsDiscrete.mk
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
rw : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ Y) f)
⊢ ContinuousOn f s

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have : Finite s := hs
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ Y) f)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric.{u_1 + 1} (α := X) Specializes
⊢ T1Space.{u_1} (SeparationQuotient X) ↔ R0Space X

Tactic:
rw [r0Space_iff, ((t1Space_TFAE (SeparationQuotient X)).out 0 9 :)]

Premises used: t1Space_TFAE, List.TFAE.out, r0Space_iff, SeparationQuotient, OfNat.ofNat
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
mp : (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) → Symmetric.{u_1 + 1} (α := X) Specializes
mpr : Symmetric.{u_1 + 1} (α := X) Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric.{u_1 + 1} (α := X) Specializes

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
mp :
  ∀ (xspecy : Specializes (X := SeparationQuotient X) (mk x) (mk y)),
    Specializes (X := SeparationQuotient X) (mk y) (mk x)
mp₁ mp₂ :
  ∀ (xspecy : Specializes (X := SeparationQuotient X) (mk y) (mk y)),
    Specializes (X := SeparationQuotient X) (mk y) (mk y)
⊢ y ⤳ x

Tactic:
rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *

Premises used: Topology.IsInducing.specializes_iff, SeparationQuotient.isInducing_mk
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
⊢ x ⤳ y

Tactic:
have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
xspecy : x ⤳ y
⊢ y ⤳ x

Tactic:
have yspecx : y ⤳ x := h xspecy
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
xspecy : x ⤳ y
yspecx : y ⤳ x
mpr : x ⤳ y ∧ y ⤳ x
⊢ Eq (α := SeparationQuotient X) (mk x) (mk y)

Tactic:
rw [mk_eq_mk, inseparable_iff_specializes_and]

Premises used: SeparationQuotient.mk_eq_mk, inseparable_iff_specializes_and
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ x ⤳ y ∧ y ⤳ x

Tactic:
⟨xspecy, yspecx⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ x ⤳ y ∧ y ⤳ x

Tactic:
exact ⟨xspecy, yspecx⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
a : X
⊢ IsClosed[inst] (A ∩ {a})

Tactic:
Subsingleton.inter_singleton.isClosed

Premises used: Set.Subsingleton.isClosed, Set.Subsingleton.inter_singleton
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
A : Set X
a : X
⊢ IsClosed[inst] ({a} ∩ A)

Tactic:
Subsingleton.singleton_inter.isClosed

Premises used: Set.Subsingleton.singleton_inter, Set.Subsingleton.isClosed
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
rw : ∀ (hs : DiscreteTopology.{u_1} (↑s : Type u_1)) {x : X} (hx : x ∈ s), {x} ∈ 𝓝[s] x
⊢ {x} ∈ 𝓝[s] x

Tactic:
rw [isDiscrete_iff_discreteTopology] at hs

Premises used: isDiscrete_iff_discreteTopology
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : DiscreteTopology.{u_1} (↑s : Type u_1)
x : X
hx : x ∈ s
⊢ {Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx} ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)

Tactic:
simp [nhds_discrete]

Premises used: nhds_discrete
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : DiscreteTopology.{u_1} (↑s : Type u_1)
x : X
hx : x ∈ s
⊢ {Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx} ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)

Tactic:
have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : DiscreteTopology.{u_1} (↑s : Type u_1)
x : X
hx : x ∈ s
this : {Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx} ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)
⊢ {x} ∈ 𝓝[s] x

Tactic:
simpa only [nhdsWithin_eq_map_subtype_coe hx, image_singleton] using
    @image_mem_map _ _ _ ((↑) : s → X) _ this

Premises used: Set.image_singleton, nhdsWithin_eq_map_subtype_coe, Filter.image_mem_map
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ 𝓝[s] x = pure x

Tactic:
(le_pure_iff.2 <| singleton_mem_nhdsWithin_of_mem_discrete hs hx).antisymm (pure_le_nhdsWithin hx)

Premises used: Iff.mpr, Filter.le_pure_iff, LE.le.antisymm, pure_le_nhdsWithin, singleton_mem_nhdsWithin_of_mem_discrete
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
rcases : ∀ (i : ι) (hi : p i) (hix : t i ∩ s ⊆ {x}), ∃ (i : ι), p i ∧ t i ∩ s = {x}
⊢ ∃ (i : ι), p i ∧ t i ∩ s = {x}

Tactic:
rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hs hx) with
    ⟨i, hi, hix⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp, nhdsWithin_hasBasis, singleton_mem_nhdsWithin_of_mem_discrete
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ (i : ι), p i ∧ t i ∩ s = {x}

Tactic:
⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, mem_of_mem_nhds, HasSubset.Subset.antisymm, And.intro, Exists.intro, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
i : ι
hi : p i
hix : t i ∩ s ⊆ {x}
⊢ ∃ (i : ι), p i ∧ t i ∩ s = {x}

Tactic:
exact ⟨i, hi, hix.antisymm <| singleton_subset_iff.2 ⟨mem_of_mem_nhds <| hb.mem_of_mem hi, hx⟩⟩
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, U ∩ s = {x}

Tactic:
simpa using (𝓝 x).basis_sets.exists_inter_eq_singleton_of_mem_discrete hs hx

Premises used: nhds, Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete, Filter.basis_sets
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
obtain : ∀ (U : Set X) (hU_nhds : U ∈ 𝓝 x) (hU_inter : U ∩ s = {x}), ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}

Tactic:
obtain ⟨U, hU_nhds, hU_inter⟩ := nhds_inter_eq_singleton_of_mem_discrete hs hx

Premises used: nhds_inter_eq_singleton_of_mem_discrete
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
obtain :
  ∀ (t : Set X) (ht_sub : t ⊆ U) (ht_open : IsOpen[inst] t) (ht_x : x ∈ t), ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}

Tactic:
obtain ⟨t, ht_sub, ht_open, ht_x⟩ := mem_nhds_iff.mp hU_nhds

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
t : Set X
ht_sub : t ⊆ U
ht_open : IsOpen[inst] t
ht_x : x ∈ t
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}

Tactic:
grind
-- Module: Mathlib.Topology.Separation.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
V : Set X
h : V ∈ 𝓝 x
h' : V ∩ s = {x}
rw : {x}ᶜ ∩ (V ∩ s) = ∅
rw₁ : Eq (α := Set X) ({x}ᶜ ∩ {x}) ∅
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
⊢ {x}ᶜ ∩ V ∩ s = ∅

Tactic:
rw [inter_assoc, h', compl_inter_self]

Premises used: Set.compl_inter_self, Set.inter_assoc
-- Module: Mathlib.Topology.Separation.Basic
Goal:
ι : Type u_3
β : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → TopologicalSpace (β i)
x : (i : ι) → β i
i : ι
inst_2 : ∀ (i : ι), T1Space.{u_4} (β i)
⊢ IsClosedEmbedding (update (β := β) x i)

Tactic:
.of_continuous_injective_isClosedMap (continuous_const.update i continuous_id)
    (update_injective x i) fun s hs ↦ ?_

Premises used: continuous_const, Continuous.update, continuous_id, Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap, Function.update_injective