awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : 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
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ Prod.map f f (x, y) ∈ (diagonal Y)ᶜ

Tactic:
inj.ne hx hy hne

Premises used: Set.Mem, setOf, Set.diagonal, Set.InjOn.ne, Not
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : 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
x_1 : X × X
x y : X
h : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ Prod.map f f (x, y) ∈ (diagonal Y)ᶜ

Tactic:
exact inj.ne hx hy hne

Premises used: Set.InjOn.ne
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : 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
⊢ ∀ x ∈ s ×ˢ s, ∀ᶠ (y : X × X) in 𝓝 x, f y.1 = f y.2 → y.1 = y.2

Tactic:
have : ∀ x ∈ s ×ˢ s, ∀ᶠ y in 𝓝 x, f y.1 = f y.2 → y.1 = y.2 := fun (x, y) ⟨hx, hy⟩ ↦ by
    rcases eq_or_ne x y with rfl | hne
    · rcases loc x hx with ⟨u, hu, hf⟩
      exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf
    · suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
      refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
      exact inj.ne hx hy hne
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : 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 ∈ s ×ˢ s, ∀ᶠ (y : X × X) in 𝓝 x, f y.1 = f y.2 → y.1 = y.2
⊢ ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2

Tactic:
rw [← eventually_nhdsSet_iff_forall, sc.nhdsSet_prod_eq sc] at this

Premises used: IsCompact.nhdsSet_prod_eq, eventually_nhdsSet_iff_forall
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : 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:
eventually_prod_self_iff.1 this

Premises used: Filter.eventually_prod_self_iff, Iff.mp, Set.InjOn
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : 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:
exact eventually_prod_self_iff.1 this

Premises used: Filter.eventually_prod_self_iff, Iff.mp
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : 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
⊢ ∃ (t : Set X), IsOpen[inst] t ∧ s ⊆ t ∧ InjOn f t

Tactic:
let ⟨_t, hst, ht⟩ := inj.exists_mem_nhdsSet sc fc loc
  let ⟨u, huo, hsu, hut⟩ := mem_nhdsSet_iff_exists.1 hst
  ⟨u, huo, hsu, ht.mono hut⟩

Premises used: _private.0.Set.InjOn.exists_isOpen_superset.match_1, Exists, mem_nhdsSet_iff_exists, HasSubset.Subset, And, Set.InjOn.exists_mem_nhdsSet, _private.0.Set.InjOn.exists_isOpen_superset.match_2, And.intro, Exists.intro, Iff.mp, Set.InjOn.mono, IsOpen, Set.InjOn
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
f : Filter X
x : X
inst_2 : f.NeBot
h : f ≤ 𝓝 x
⊢ f.lim = x

Tactic:
tendsto_nhds_unique (le_nhds_lim ⟨x, h⟩) h

Premises used: le_nhds_lim, Exists.intro, tendsto_nhds_unique
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
f : Filter X
inst_2 : f.NeBot
h : ∃ (x : X), f ≤ 𝓝 x
x : X
⊢ f.lim = x ↔ f ≤ 𝓝 x

Tactic:
⟨fun c => c ▸ le_nhds_lim h, lim_eq⟩

Premises used: lim_eq, Eq.rec, le_nhds_lim, Iff.intro
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
x : X
F : Ultrafilter X
⊢ F.lim = x ↔ (↑F : Filter X) ≤ 𝓝 x

Tactic:
⟨fun h => h ▸ F.le_nhds_lim, lim_eq⟩

Premises used: lim_eq, Eq.rec, Ultrafilter.le_nhds_lim, Iff.intro
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
rw :
  (∀ x ∈ U, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → U ∈ l) ↔
    ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
⊢ IsOpen[inst] U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)

Tactic:
rw [isOpen_iff_ultrafilter]

Premises used: isOpen_iff_ultrafilter
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
⊢ (∀ x ∈ U, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → U ∈ l) ↔
    ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)

Tactic:
⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩

Premises used: Ultrafilter.le_nhds_lim, Iff.intro, Ultrafilter.lim
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
refine :
  (∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)) →
    ∀ x ∈ U, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → U ∈ l
⊢ (∀ x ∈ U, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → U ∈ l) ↔
    ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)

Tactic:
refine ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
x : X
hx : x ∈ U
f : Ultrafilter X
h : (↑f : Filter X) ≤ 𝓝 x
⊢ f.lim ∈ U

Tactic:
rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx

Premises used: Iff.mpr, Ultrafilter.lim_eq_iff_le_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
x : X
hx : x ∈ U
f : Ultrafilter X
h : (↑f : Filter X) ≤ 𝓝 x
hx₁ : f.lim ∈ U
⊢ (↑f : Filter X) ≤ 𝓝 x

Tactic:
rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx

Premises used: Iff.mpr, Ultrafilter.lim_eq_iff_le_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
x : X
f : Ultrafilter X
hx : f.lim ∈ U
h : (↑f : Filter X) ≤ 𝓝 x
⊢ U ∈ f

Tactic:
cond _ hx
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ (↑F : Filter X)
x : X
f : Ultrafilter X
hx : f.lim ∈ U
h : (↑f : Filter X) ≤ 𝓝 x
⊢ U ∈ f

Tactic:
exact cond _ hx
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
f : Filter Y
inst_2 : f.NeBot
g : Y → X
h : Tendsto g f (𝓝 x)
⊢ f.limUnder g = x

Tactic:
lim_eq h

Premises used: lim_eq, Filter.limUnder
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
f : Filter Y
inst_2 : f.NeBot
g : Y → X
h : ∃ (x : X), Tendsto g f (𝓝 x)
x : X
⊢ f.limUnder g = x ↔ Tendsto g f (𝓝 x)

Tactic:
⟨fun c => c ▸ tendsto_nhds_limUnder h, Filter.Tendsto.limUnder_eq⟩

Premises used: Eq.rec, tendsto_nhds_limUnder, Iff.intro, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
f : Y → X
h : Continuous[inst_2, inst] f
y : Y
⊢ (𝓝 y).limUnder f = f y

Tactic:
(h.tendsto y).limUnder_eq

Premises used: Continuous.tendsto, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
⊢ (𝓝 x).lim = x

Tactic:
lim_eq le_rfl

Premises used: le_rfl, lim_eq
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
⊢ (𝓝 x).limUnder id = x

Tactic:
lim_nhds x

Premises used: Set.Mem, Filter.map, setOf, Set.preimage, Filter.limUnder, lim_nhds
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
s : Set X
h : x ∈ closure[inst] s
⊢ (𝓝[s] x).lim = x

Tactic:
haveI : NeBot (𝓝[s] x) := mem_closure_iff_clusterPt.1 h
  lim_eq inf_le_left

Premises used: lim_eq, inf_le_left
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
x : X
s : Set X
h : x ∈ closure[inst] s
⊢ (𝓝[s] x).limUnder id = x

Tactic:
lim_nhdsWithin h

Premises used: Set.Mem, Filter.map, nhdsWithin, setOf, lim_nhdsWithin, Set.preimage, Filter.limUnder
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
⊢ T2Space X

Tactic:
⟨fun x y h => ⟨{x}, {y}, isOpen_discrete _, isOpen_discrete _, rfl, rfl, disjoint_singleton.2 h⟩⟩

Premises used: Iff.mpr, Set.disjoint_singleton, And.intro, isOpen_discrete, Exists.intro, Singleton.singleton, T2Space.mk, rfl
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
x y : X
h : f x ≠ f y
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Tactic:
let ⟨u, v, uo, vo, xu, yv, uv⟩ := t2_separation h
  ⟨f ⁻¹' u, f ⁻¹' v, uo.preimage hf, vo.preimage hf, xu, yv, uv.preimage _⟩

Premises used: Disjoint, Membership.mem, Exists, _private.0.separated_by_continuous.match_1, And, Set.preimage, And.intro, Exists.intro, IsOpen, IsOpen.preimage, Disjoint.preimage, t2_separation
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
f : X → Y
hf : IsOpenEmbedding f
x y : X
h : x ≠ y
⊢ ∃ (u : Set Y) (v : Set Y), IsOpen[inst_1] u ∧ IsOpen[inst_1] v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v

Tactic:
let ⟨u, v, uo, vo, xu, yv, uv⟩ := t2_separation h
  ⟨f '' u, f '' v, hf.isOpenMap _ uo, hf.isOpenMap _ vo, mem_image_of_mem _ xu,
    mem_image_of_mem _ yv, disjoint_image_of_injective hf.injective uv⟩

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsOpenEmbedding.isOpenMap, Disjoint, Membership.mem, Exists, _private.0.t2_separation_nhds.match_1, And, Set.mem_image_of_mem, And.intro, Topology.IsEmbedding.injective, Exists.intro, Set.image, IsOpen, t2_separation, Set.disjoint_image_of_injective
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
p : X → Prop
inst_1 : T2Space X
⊢ T2Space.{u_1} (Subtype p)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
⊢ T2Space (X × Y)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
hinj : Injective f
hc : Continuous[inst, inst_1] f
⊢ T2Space X

Tactic:
⟨fun _ _ h => separated_by_continuous hc (hinj.ne h)⟩

Premises used: separated_by_continuous, Function.Injective.ne, T2Space.mk
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
f : X → Y
hf : IsEmbedding f
⊢ T2Space X

Tactic:
.of_injective_continuous hf.injective hf.continuous

Premises used: T2Space.of_injective_continuous, Topology.IsEmbedding.injective, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
h : X ≃ₜ Y
⊢ T2Space Y

Tactic:
h.symm.isEmbedding.t2Space

Premises used: Homeomorph.isEmbedding, Homeomorph.symm, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
⊢ T2Space (ULift.{u_3, u_1} X)

Tactic:
IsEmbedding.uliftDown.t2Space

Premises used: Topology.IsEmbedding.uliftDown, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
t2 :
  Pairwise fun (x y : X ⊕ Y) ↦
    ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
      IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
⊢ T2Space (X ⊕ Y)

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x y : X
h : Ne (α := X ⊕ Y) (Sum.inl x) (Sum.inl y)
⊢ ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

Tactic:
separated_by_isOpenEmbedding .inl <| ne_of_apply_ne _ h

Premises used: separated_by_isOpenEmbedding, ne_of_apply_ne, Topology.IsOpenEmbedding.inl
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x y : X
h : Ne (α := X ⊕ Y) (Sum.inl x) (Sum.inl y)
⊢ ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_isOpenEmbedding .inl <| ne_of_apply_ne _ h

Premises used: separated_by_isOpenEmbedding, ne_of_apply_ne, Topology.IsOpenEmbedding.inl
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x : X
y : Y
h : Sum.inl x ≠ Sum.inr y
⊢ Sum.isLeft.{u_1, u_2} (β := Y) (Sum.inl x) ≠ Sum.isLeft.{u_1, u_2} (α := X) (Sum.inr y)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x : X
y : Y
h : Sum.inl x ≠ Sum.inr y
⊢ ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inl x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous continuous_isLeft <| by simp

Premises used: separated_by_continuous, continuous_isLeft
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x : Y
y : X
h : Sum.inr x ≠ Sum.inl y
⊢ Sum.isLeft.{u_1, u_2} (α := X) (Sum.inr x) ≠ Sum.isLeft.{u_1, u_2} (β := Y) (Sum.inl y)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x : Y
y : X
h : Sum.inr x ≠ Sum.inl y
⊢ ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inl y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous continuous_isLeft <| by simp

Premises used: separated_by_continuous, continuous_isLeft
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x y : Y
h : Ne (α := X ⊕ Y) (Sum.inr x) (Sum.inr y)
⊢ ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

Tactic:
separated_by_isOpenEmbedding .inr <| ne_of_apply_ne _ h

Premises used: separated_by_isOpenEmbedding, Topology.IsOpenEmbedding.inr, ne_of_apply_ne
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
x y : Y
h : Ne (α := X ⊕ Y) (Sum.inr x) (Sum.inr y)
⊢ ∃ (u : Set (X ⊕ Y)) (v : Set (X ⊕ Y)),
    IsOpen[instTopologicalSpaceSum] u ∧ IsOpen[instTopologicalSpaceSum] v ∧ Sum.inr x ∈ u ∧ Sum.inr y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_isOpenEmbedding .inr <| ne_of_apply_ne _ h

Premises used: separated_by_isOpenEmbedding, Topology.IsOpenEmbedding.inr, ne_of_apply_ne
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X
Y : X → Type v
inst_1 : (a : X) → TopologicalSpace (Y a)
inst_2 : ∀ (a : X), T2Space.{v} (Y a)
⊢ T2Space ((a : X) → Y a)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
t2 :
  Pairwise fun (x y : (i : ι) × X i) ↦
    ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
      IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
⊢ T2Space ((i : ι) × X i)

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x : X i
j : ι
y : X j
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) j y
t2 :
  ∀ (y : X i) (ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) i y),
    ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
      IsOpen[instTopologicalSpaceSigma] u ∧
        IsOpen[instTopologicalSpaceSigma] v ∧
          mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) i y ∈ v ∧ Disjoint u v
t2₁ :
  ∀ (h : i ≠ j),
    ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
      IsOpen[instTopologicalSpaceSigma] u ∧
        IsOpen[instTopologicalSpaceSigma] v ∧
          mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v

Tactic:
rcases eq_or_ne i j with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x y : X i
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) i y
⊢ x ≠ y

Tactic:
replace ne : x ≠ y := ne_of_apply_ne _ ne
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x y : X i
ne : x ≠ y
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) i y ∈ v ∧ Disjoint u v

Tactic:
separated_by_isOpenEmbedding .sigmaMk ne

Premises used: separated_by_isOpenEmbedding, Topology.IsOpenEmbedding.sigmaMk
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x y : X i
ne : x ≠ y
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) i y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_isOpenEmbedding .sigmaMk ne

Premises used: separated_by_isOpenEmbedding, Topology.IsOpenEmbedding.sigmaMk
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x : X i
j : ι
y : X j
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) j y
h : i ≠ j
x_1 : TopologicalSpace ι := ⊥
⊢ DiscreteTopology ι

Tactic:
have : DiscreteTopology ι := ⟨rfl⟩
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x : X i
j : ι
y : X j
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) j y
h : i ≠ j
x_1 : TopologicalSpace ι := ⊥
this : DiscreteTopology ι
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v

Tactic:
separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h

Premises used: Iff.mpr, separated_by_continuous, Set.Mem, isOpen_sigma_fst_preimage, continuous_def
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
ι : Type u_4
X : ι → Type u_3
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (a : ι), T2Space.{u_3} (X a)
i : ι
x : X i
j : ι
y : X j
ne : mk (β := fun (i : ι) ↦ X i) i x ≠ mk (β := fun (i : ι) ↦ X i) j y
h : i ≠ j
x_1 : TopologicalSpace ι := ⊥
this : DiscreteTopology ι
⊢ ∃ (u : Set ((i : ι) × X i)) (v : Set ((i : ι) × X i)),
    IsOpen[instTopologicalSpaceSigma] u ∧
      IsOpen[instTopologicalSpaceSigma] v ∧
        mk (β := fun (i : ι) ↦ X i) i x ∈ u ∧ mk (β := fun (i : ι) ↦ X i) j y ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h

Premises used: Iff.mpr, separated_by_continuous, isOpen_sigma_fst_preimage, continuous_def
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Eq (α := T2Quotient X) (mk x) (mk y) ↔ ∀ (s : Setoid X), T2Space.{u_1} (Quotient s) → (s : X → X → Prop) x y

Tactic:
Setoid.quotient_mk_sInf_eq

Premises used: Set.Mem, setOf, Setoid.quotient_mk_sInf_eq, T2Quotient.mk, T2Quotient
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := X) (β := T2Quotient X) mk

Tactic:
Quotient.mk_surjective

Premises used: T2Quotient.mk, T2Quotient, Quotient.mk_surjective
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Continuous[inst, _] mk

Tactic:
continuous_quotient_mk'

Premises used: continuous_quotient_mk', T2Quotient.mk, T2Quotient, Quotient.mk'
-- Module: Mathlib.Topology.Separation.Hausdorff
Goal:
X : Type u_1
inst : TopologicalSpace X
motive : T2Quotient X → Prop
q : T2Quotient X
h : ∀ (x : X), motive (mk x)
⊢ motive q

Tactic:
Quotient.inductionOn q h

Premises used: Quotient.inductionOn