awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
a : s₁ ⊆ s₁ ∧ s₃ ⊆ s₃
⊢ (s₁, s₃) ∈ hausdorffEntourage (U ○ V)

Tactic:
grw [mem_hausdorffEntourage, preimage_comp, ← h₂₃, ← h₁₂, image_comp, ← h₂₁, ← h₃₂]

Premises used: SetRel.preimage_comp, mem_hausdorffEntourage, SetRel.image_comp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ s₁ ⊆ s₁ ∧ s₃ ⊆ s₃

Tactic:
⟨subset_rfl, subset_rfl⟩

Premises used: And.intro, subset_rfl
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s₁ s₃ s₂ : Set α
h₁₂ : s₁ ⊆ U.preimage s₂
h₂₁ : s₂ ⊆ U.image s₁
h₂₃ : s₂ ⊆ V.preimage s₃
h₃₂ : s₃ ⊆ V.image s₂
⊢ s₁ ⊆ s₁ ∧ s₃ ⊆ s₃

Tactic:
exact ⟨subset_rfl, subset_rfl⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst : U.IsTrans
grw : hausdorffEntourage U ○ hausdorffEntourage U ⊆ hausdorffEntourage U
grw₁ : hausdorffEntourage (U ○ U) ⊆ hausdorffEntourage U
grw₂ grw₃ : hausdorffEntourage U ⊆ hausdorffEntourage U
⊢ (hausdorffEntourage U).IsTrans

Tactic:
grw [isTrans_iff_comp_subset_self, ← hausdorffEntourage_comp, comp_subset_self]

Premises used: hausdorffEntourage_comp, SetRel.comp_subset_self, SetRel.isTrans_iff_comp_subset_self
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U : SetRel α α
x y : α
⊢ ({x}, {y}) ∈ hausdorffEntourage U ↔ (x, y) ∈ U

Tactic:
simp [hausdorffEntourage]

Premises used: hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U : SetRel α α
s₁ s₂ t₁ t₂ : Set α
h₁ : (s₁, t₁) ∈ hausdorffEntourage U
h₂ : (s₂, t₂) ∈ hausdorffEntourage U
⊢ (s₁ ∪ s₂, t₁ ∪ t₂) ∈ hausdorffEntourage U

Tactic:
grind [mem_hausdorffEntourage, preimage_union, image_union]

Premises used: SetRel.preimage_union, SetRel.image_union, mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
obtain :
  ∀ (t : Set α) (ht₁ : t.Finite) (ht₂ : s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ Prod.swap ⁻¹' U}),
    ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := hs _ (symm_le_uniformity hU)

Premises used: symm_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Set α
ht₁ : t.Finite
ht₂ : s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ t.Finite

Tactic:
ht₁
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Set α
ht₁ : t.Finite
ht₂ : s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
lift :
  ∀ (t : Finset α) (ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}),
    ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U

Tactic:
lift t to Finset α using ht₁

Premises used: Finset
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U

Tactic:
⟨{x ∈ t | ∃ y ∈ s, (x, y) ∈ U}, ?_⟩

Premises used: Membership.mem, Exists, Prod.mk, And, Exists.intro, Finset.filter
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
refine : ((↑({x ∈ t | ∃ y ∈ s, (x, y) ∈ U}) : Set α), s) ∈ hausdorffEntourage U
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U

Tactic:
refine ⟨{x ∈ t | ∃ y ∈ s, (x, y) ∈ U}, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
rw : ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U
⊢ ((↑({x ∈ t | ∃ y ∈ s, (x, y) ∈ U}) : Set α), s) ∈ hausdorffEntourage U

Tactic:
rw [Finset.coe_filter]

Premises used: Finset.coe_filter
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
⊢ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U

Tactic:
⟨fun _ h => h.2, fun x hx => ?_⟩

Premises used: Set.Mem, setOf, And.right, And.intro, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
refine :
  ∀ (x : α) (hx : x ∈ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2),
    x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1
⊢ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U

Tactic:
refine ⟨fun _ h => h.2, fun x hx => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
x : α
hx : x ∈ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2
obtain :
  ∀ (y : α) (hy : y ∈ (↑t : Set α)) (hxy : Membership.mem (γ := Set α) {x : α | (x, y) ∈ Prod.swap ⁻¹' U} x),
    x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1
⊢ x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1

Tactic:
obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht₂ hx)

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
x : α
hx : x ∈ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2
y : α
hy : y ∈ (↑t : Set α)
hxy : Membership.mem (γ := Set α) {x : α | (x, y) ∈ Prod.swap ⁻¹' U} x
⊢ x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1

Tactic:
⟨y, ⟨hy, x, hx, hxy⟩, hxy⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, SetRel.image
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
x : α
hx : x ∈ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2
y : α
hy : y ∈ (↑t : Set α)
hxy : Membership.mem (γ := Set α) {x : α | (x, y) ∈ Prod.swap ⁻¹' U} x
⊢ x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1

Tactic:
exact ⟨y, ⟨hy, x, hx, hxy⟩, hxy⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
t : Finset α
ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}
refine : ((↑({x ∈ t | ∃ y ∈ s, (x, y) ∈ U}) : Set α), s) ∈ hausdorffEntourage U
refine₁ : ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U
refine₂ :
  ∀ (x : α) (hx : x ∈ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2),
    x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1
refine₃ :
  ∀ (x : α) (hx : x ∈ ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).2) (y : α) (hy : y ∈ (↑t : Set α))
    (hxy : Membership.mem (γ := Set α) {x : α | (x, y) ∈ Prod.swap ⁻¹' U} x),
    x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U

Tactic:
classical
  refine ⟨{x ∈ t | ∃ y ∈ s, (x, y) ∈ U}, ?_⟩
  rw [Finset.coe_filter]
  refine ⟨fun _ h => h.2, fun x hx => ?_⟩
  obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht₂ hx)
  exact ⟨y, ⟨hy, x, hx, hxy⟩, hxy⟩

Premises used: Finset.coe_filter
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
U₁ : SetRel α α
U₂ : SetRel β β
s₁ t₁ : Set α
s₂ t₂ : Set β
h₁ : (s₁, t₁) ∈ hausdorffEntourage U₁
h₂ : (s₂, t₂) ∈ hausdorffEntourage U₂
⊢ s₁ ⊆ U₁.preimage t₁ ∧ t₁ ⊆ U₁.image s₁

Tactic:
simp only [mem_hausdorffEntourage] at *

Premises used: mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
U₁ : SetRel α α
U₂ : SetRel β β
s₁ t₁ : Set α
s₂ t₂ : Set β
h₁ : (s₁, t₁) ∈ hausdorffEntourage U₁
h₂ : (s₂, t₂) ∈ hausdorffEntourage U₂
h₃ : s₁ ⊆ U₁.preimage t₁ ∧ t₁ ⊆ U₁.image s₁
⊢ s₂ ⊆ U₂.preimage t₂ ∧ t₂ ⊆ U₂.image s₂

Tactic:
simp only [mem_hausdorffEntourage] at *

Premises used: mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
U₁ : SetRel α α
U₂ : SetRel β β
s₁ t₁ : Set α
s₂ t₂ : Set β
h₁ : s₁ ⊆ U₁.preimage t₁ ∧ t₁ ⊆ U₁.image s₁
h₂ : s₂ ⊆ U₂.preimage t₂ ∧ t₂ ⊆ U₂.image s₂
⊢ s₁ ×ˢ s₂ ⊆ (entourageProd U₁ U₂).preimage (t₁ ×ˢ t₂) ∧ t₁ ×ˢ t₂ ⊆ (entourageProd U₁ U₂).image (s₁ ×ˢ s₂)

Tactic:
grind [preimage_entourageProd_prod, image_entourageProd_prod]

Premises used: preimage_entourageProd_prod, image_entourageProd_prod
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
simp_rw : ∀ s ∈ 𝓤 α, (hausdorffEntourage s).IsRefl
⊢ 𝓟 SetRel.id ≤ (𝓤 α).lift' hausdorffEntourage

Tactic:
simp_rw [Filter.principal_le_lift', SetRel.id_subset_iff]

Premises used: Filter.principal_le_lift', SetRel.id_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ U.IsRefl

Tactic:
have := isRefl_of_mem_uniformity hU
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : SetRel α α
hU : U ∈ 𝓤 α
this : U.IsRefl
⊢ (hausdorffEntourage U).IsRefl

Tactic:
isRefl_hausdorffEntourage U

Premises used: isRefl_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : SetRel α α
hU : U ∈ 𝓤 α
this : U.IsRefl
⊢ (hausdorffEntourage U).IsRefl

Tactic:
exact isRefl_hausdorffEntourage U

Premises used: isRefl_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
rw :
  ∀ s ∈ 𝓤 α,
    Membership.mem (γ := Filter (Set α × Set α))
      (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) (hausdorffEntourage s)
⊢ (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) ≤
    (𝓤 α).lift' hausdorffEntourage

Tactic:
rw [Filter.le_lift']

Premises used: Filter.le_lift'
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α
obtain :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVU : SetRel.comp V V ⊆ U),
    Membership.mem (γ := Filter (Set α × Set α))
      (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) (hausdorffEntourage U)
⊢ Membership.mem (γ := Filter (Set α × Set α))
    (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) (hausdorffEntourage U)

Tactic:
obtain ⟨V, hV, hVU⟩ := comp_mem_uniformity_sets hU

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : SetRel.comp V V ⊆ U
⊢ Membership.mem (γ := Filter (Set α × Set α))
    (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) (hausdorffEntourage U)

Tactic:
Filter.mem_of_superset (Filter.mem_lift' (Filter.mem_lift' hV)) ?_

Premises used: Filter.mem_lift', Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : SetRel.comp V V ⊆ U
refine : (hausdorffEntourage V).comp (hausdorffEntourage V) ⊆ hausdorffEntourage U
⊢ Membership.mem (γ := Filter (Set α × Set α))
    (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) (hausdorffEntourage U)

Tactic:
refine Filter.mem_of_superset (Filter.mem_lift' (Filter.mem_lift' hV)) ?_

Premises used: Filter.mem_lift', Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : SetRel.comp V V ⊆ U
grw : hausdorffEntourage (SetRel.comp V V) ⊆ hausdorffEntourage U
grw₁ grw₂ : hausdorffEntourage U ⊆ hausdorffEntourage U
⊢ (hausdorffEntourage V).comp (hausdorffEntourage V) ⊆ hausdorffEntourage U

Tactic:
grw [← hausdorffEntourage_comp, hVU]

Premises used: hausdorffEntourage_comp
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
ι : Sort u_4
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
⊢ HasBasis (𝓤 (Set α)) p (hausdorffEntourage ∘ s)

Tactic:
h.lift' monotone_hausdorffEntourage

Premises used: monotone_hausdorffEntourage, iInf, uniformity, Filter.lift', Filter.lift, Filter.HasBasis.lift'
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
rw :
  ∀ (x : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} x → {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 x
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {s : Set α | (s ∩ U).Nonempty}

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
this : ∀ (x : α) (hx₁ : x ∈ s) (hx₂ : x ∈ U), {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s → {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s

Tactic:
⟨x, hx₁, hx₂⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : x ∈ U
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ U

Tactic:
rw [← hU.mem_nhds_iff, mem_nhds_iff] at hx₂

Premises used: IsOpen.mem_nhds_iff, UniformSpace.mem_nhds_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : ∃ V ∈ 𝓤 α, ball x V ⊆ U
obtain : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVU : ball x V ⊆ U), {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s
⊢ {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s

Tactic:
obtain ⟨V, hV, hVU⟩ := hx₂
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
rw :
  ∃ (V : Set (Set α × Set α)),
    Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) V ∧ ball s V ⊆ {s : Set α | (s ∩ U).Nonempty}
⊢ {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s

Tactic:
rw [mem_nhds_iff]

Premises used: UniformSpace.mem_nhds_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
⊢ ∃ (V : Set (Set α × Set α)),
    Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) V ∧ ball s V ⊆ {s : Set α | (s ∩ U).Nonempty}

Tactic:
⟨_, Filter.mem_lift' hV, ?_⟩

Premises used: Filter.mem_lift', And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
refine : ball s (hausdorffEntourage V) ⊆ {s : Set α | (s ∩ U).Nonempty}
⊢ ∃ (V : Set (Set α × Set α)),
    Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) V ∧ ball s V ⊆ {s : Set α | (s ∩ U).Nonempty}

Tactic:
refine ⟨_, Filter.mem_lift' hV, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
s' : Set α
hs' : (s, s').1 ⊆ SetRel.preimage V (s, s').2
obtain :
  ∀ (y : α) (hy : y ∈ (s, s').2) (hxy : (x, y) ∈ V), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s'
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s'

Tactic:
obtain ⟨y, hy, hxy⟩ := hs' hx₁
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
s' : Set α
hs' : (s, s').1 ⊆ SetRel.preimage V (s, s').2
y : α
hy : y ∈ (s, s').2
hxy : (x, y) ∈ V
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s'

Tactic:
⟨y, hy, hVU hxy⟩

Premises used: Set.Mem, setOf, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : ball x V ⊆ U
s' : Set α
hs' : (s, s').1 ⊆ SetRel.preimage V (s, s').2
y : α
hy : y ∈ (s, s').2
hxy : (x, y) ∈ V
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s'

Tactic:
exact ⟨y, hy, hVU hxy⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
F : Set α
hF : IsClosed[inst.toTopologicalSpace] F
simp_rw : IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {a : Set α | (a ∩ Fᶜ).Nonempty}
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 F)

Tactic:
simp_rw [Set.powerset, ← isOpen_compl_iff, Set.compl_setOf, ← Set.inter_compl_nonempty_iff]

Premises used: Set.powerset, Set.inter_compl_nonempty_iff, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
F : Set α
hF : IsClosed[inst.toTopologicalSpace] F
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {a : Set α | (a ∩ Fᶜ).Nonempty}

Tactic:
isOpen_inter_nonempty_of_isOpen hF.isOpen_compl

Premises used: IsClosed.isOpen_compl, UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
F : Set α
hF : IsClosed[inst.toTopologicalSpace] F
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {a : Set α | (a ∩ Fᶜ).Nonempty}

Tactic:
exact isOpen_inter_nonempty_of_isOpen hF.isOpen_compl

Premises used: IsClosed.isOpen_compl, UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
left : IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}
right : IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}
⊢ IsClopen (X := Set α) {∅}

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
left : IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 ∅)
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}

Tactic:
rw [← Set.powerset_empty]

Premises used: Set.powerset_empty
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 ∅)

Tactic:
isClosed_empty.powerset_hausdorff

Premises used: isClosed_empty, IsClosed.powerset_hausdorff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 ∅)

Tactic:
exact isClosed_empty.powerset_hausdorff

Premises used: isClosed_empty, IsClosed.powerset_hausdorff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
right : Membership.mem (γ := Filter (Set α)) (Filter.lift' (𝓤 (Set α)) (ball ∅)) {∅}
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}

Tactic:
simp_rw [isOpen_iff_mem_nhds, Set.mem_singleton_iff, forall_eq, nhds_eq_uniformity]

Premises used: forall_eq, Set.mem_singleton_iff, nhds_eq_uniformity, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
F : Set α
h :
  Subset (α := Set α) (∅, F).1 (SetRel.preimage Set.univ (∅, F).2) →
    ∀ (hF : (∅, F).2 ⊆ SetRel.image (α := α) Set.univ (∅, F).1), Membership.mem (γ := Set (Set α)) {∅} F
⊢ Membership.mem (γ := Set (Set α)) (ball ∅ (hausdorffEntourage Set.univ)) F → Membership.mem (γ := Set (Set α)) {∅} F

Tactic:
⟨_, hF⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h :
  ∀ (F : Set α),
    Subset (α := Set α) (∅, F).1 (SetRel.preimage Set.univ (∅, F).2) →
      ∀ (hF : (∅, F).2 ⊆ SetRel.image (α := α) Set.univ (∅, F).1), Membership.mem (γ := Set (Set α)) {∅} F
⊢ Membership.mem (γ := Filter (Set α)) (Filter.lift' (𝓤 (Set α)) (ball ∅)) {∅}

Tactic:
filter_upwards [Filter.mem_lift' <| Filter.mem_lift' Filter.univ_mem] with F ⟨_, hF⟩

Premises used: Filter.mem_lift', Filter.univ_mem
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
F : Set α
left : Subset (α := Set α) (∅, F).1 (SetRel.preimage Set.univ (∅, F).2)
hF : (∅, F).2 ⊆ SetRel.image (α := α) Set.univ (∅, F).1
⊢ Membership.mem (γ := Set (Set α)) {∅} F

Tactic:
simpa using hF
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
simp_rw : ((𝓤 α).lift' fun (x : Set (α × α)) ↦ {x_1 : α × α | (x_1.1, x_1.2) ∈ x}) = 𝓤 α
⊢ Filter.comap (fun (x : α × α) ↦ ({x.1}, {x.2})) ((𝓤 α).lift' hausdorffEntourage) = 𝓤 α

Tactic:
simp_rw [Filter.comap_lift'_eq, Function.comp_def, Set.preimage,
      singleton_mem_hausdorffEntourage]

Premises used: Filter.comap_lift'_eq, Function.comp_def, Set.preimage, singleton_mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ ((𝓤 α).lift' fun (x : Set (α × α)) ↦ {x_1 : α × α | (x_1.1, x_1.2) ∈ x}) = 𝓤 α

Tactic:
Filter.lift'_id

Premises used: Filter.lift'_id, Set.Mem, setOf
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ ((𝓤 α).lift' fun (x : Set (α × α)) ↦ {x_1 : α × α | (x_1.1, x_1.2) ∈ x}) = 𝓤 α

Tactic:
exact Filter.lift'_id

Premises used: Filter.lift'_id
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (β := Set α) fun (x : Set α × Set α) ↦ x.1 ∪ x.2

Tactic:
Filter.tendsto_lift'.mpr fun U hU => ?_

Premises used: Iff.mpr, Filter.tendsto_lift', UniformContinuous, iInf, uniformity, Filter.lift', Filter.lift
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
refine :
  ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α),
    ∀ᶠ (a : (Set α × Set α) × Set α × Set α) in 𝓤 (Set α × Set α),
      ((fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.1, (fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.2) ∈ hausdorffEntourage U
⊢ UniformContinuous (β := Set α) fun (x : Set α × Set α) ↦ x.1 ∪ x.2

Tactic:
refine Filter.tendsto_lift'.mpr fun U hU => ?_

Premises used: Iff.mpr, Filter.tendsto_lift'