awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
z : α
hz : z ∈ t
⊢ z ∈ V.image (U.image s ∩ V.preimage t)
have a : ∀ (x : α) (hx : x ∈ s) (y : α) (hxy : (x, y) ∈ U) (hyz : (y, z) ∈ V), z ∈ V.image (U.image s ∩ V.preimage t)
Tactic: obtain ⟨x, hx, y, hxy, hyz⟩ := hts hz
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
U V : SetRel α α
s₁ s₃ : Set α
⊢ (s₁, s₃) ∈ hausdorffEntourage U ○ hausdorffEntourage V → (s₁, s₃) ∈ hausdorffEntourage (U ○ V)
have a : ∀ (s₂ : Set α) (h₁₂ : (s₁, s₂).1 ⊆ U.preimage (s₁, s₂).2) (h₂₁ : (s₁, s₂).2 ⊆ U.image (s₁, s₂).1)
  (h₂₃ : (s₂, s₃).1 ⊆ V.preimage (s₂, s₃).2) (h₃₂ : (s₂, s₃).2 ⊆ V.image (s₂, s₃).1),
  (s₁, s₃) ∈ hausdorffEntourage (U ○ V)
Tactic: ⟨s₂, ⟨h₁₂, h₂₁⟩, ⟨h₂₃, h₃₂⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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₃) ∈ hausdorffEntourage (U ○ V)
have a : s₁ ⊆ s₁ ∧ s₃ ⊆ s₃
Tactic: grw [mem_hausdorffEntourage, preimage_comp, ← h₂₃, ← h₁₂, image_comp, ← h₂₁, ← h₃₂]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst : U.IsTrans
⊢ (hausdorffEntourage U).IsTrans
have grw : hausdorffEntourage U ○ hausdorffEntourage U ⊆ hausdorffEntourage U
Tactic: grw [isTrans_iff_comp_subset_self, ← hausdorffEntourage_comp, comp_subset_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst : U.IsTrans
grw : hausdorffEntourage U ○ hausdorffEntourage U ⊆ hausdorffEntourage U
⊢ (hausdorffEntourage U).IsTrans
have grw₁ : hausdorffEntourage (U ○ U) ⊆ hausdorffEntourage U
Tactic: grw [isTrans_iff_comp_subset_self, ← hausdorffEntourage_comp, comp_subset_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ (hausdorffEntourage U).IsTrans
have grw₂ : hausdorffEntourage U ⊆ hausdorffEntourage U
Tactic: grw [isTrans_iff_comp_subset_self, ← hausdorffEntourage_comp, comp_subset_self]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
have obtain : ∀ (t : Set α) (ht₁ : t.Finite) (ht₂ : s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ Prod.swap ⁻¹' U}),
  ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
Tactic: obtain ⟨t, ht₁, ht₂⟩ := hs _ (symm_le_uniformity hU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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 : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
have lift : ∀ (t : Finset α) (ht₂ : s ⊆ ⋃ y ∈ (↑t : Set α), {x : α | (x, y) ∈ Prod.swap ⁻¹' U}),
  ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
Tactic: lift t to Finset α using ht₁
Cleared hypotheses: t, ht₁, ht₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
have refine : ((↑({x ∈ t | ∃ y ∈ s, (x, y) ∈ U}) : Set α), s) ∈ hausdorffEntourage U
Tactic: refine ⟨{x ∈ t | ∃ y ∈ s, (x, y) ∈ U}, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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 ∈ t | ∃ y ∈ s, (x, y) ∈ U}) : Set α), s) ∈ hausdorffEntourage U
have rw : ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s) ∈ hausdorffEntourage U
Tactic: rw [Finset.coe_filter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
have 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
Tactic: refine ⟨fun _ h => h.2, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ x ∈ U.image ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, s).1
have 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
Tactic: obtain ⟨y, hy, hxy⟩ := Set.mem_iUnion₂.mp (ht₂ hx)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
have refine : ((↑({x ∈ t | ∃ y ∈ s, (x, y) ∈ U}) : 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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
have refine₁ : ({x : α | x ∈ t ∧ ∃ y ∈ s, (x, y) ∈ U}, 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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ ∃ (t : Finset α), ((↑t : Set α), s) ∈ hausdorffEntourage U
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
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₁ ×ˢ s₂, t₁ ×ˢ t₂) ∈ hausdorffEntourage (entourageProd U₁ U₂)
have h₃ : s₁ ⊆ U₁.preimage t₁ ∧ t₁ ⊆ U₁.image s₁
Tactic: simp only [mem_hausdorffEntourage] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
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₁ ×ˢ s₂, t₁ ×ˢ t₂) ∈ hausdorffEntourage (entourageProd U₁ U₂)
have h₄ : s₂ ⊆ U₂.preimage t₂ ∧ t₂ ⊆ U₂.image s₂
Tactic: simp only [mem_hausdorffEntourage] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
⊢ 𝓟 SetRel.id ≤ (𝓤 α).lift' hausdorffEntourage
have simp_rw : ∀ s ∈ 𝓤 α, (hausdorffEntourage s).IsRefl
Tactic: simp_rw [Filter.principal_le_lift', SetRel.id_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ (hausdorffEntourage U).IsRefl
have this : U.IsRefl
Tactic: have := isRefl_of_mem_uniformity hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
⊢ (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) ≤
    (𝓤 α).lift' hausdorffEntourage
have rw : ∀ s ∈ 𝓤 α,
  Membership.mem (γ := Filter (Set α × Set α))
    (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) (hausdorffEntourage s)
Tactic: rw [Filter.le_lift']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ Membership.mem (γ := Filter (Set α × Set α))
    (((𝓤 α).lift' hausdorffEntourage).lift' fun (s : Set (Set α × Set α)) ↦ SetRel.comp s s) (hausdorffEntourage U)
have 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)
Tactic: obtain ⟨V, hV, hVU⟩ := comp_mem_uniformity_sets hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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)
have refine : (hausdorffEntourage V).comp (hausdorffEntourage V) ⊆ hausdorffEntourage U
Tactic: refine Filter.mem_of_superset (Filter.mem_lift' (Filter.mem_lift' hV)) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ (hausdorffEntourage V).comp (hausdorffEntourage V) ⊆ hausdorffEntourage U
have grw : hausdorffEntourage (SetRel.comp V V) ⊆ hausdorffEntourage U
Tactic: grw [← hausdorffEntourage_comp, hVU]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ (hausdorffEntourage V).comp (hausdorffEntourage V) ⊆ hausdorffEntourage U
have grw₁ : hausdorffEntourage U ⊆ hausdorffEntourage U
Tactic: grw [← hausdorffEntourage_comp, hVU]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {s : Set α | (s ∩ U).Nonempty}
have rw : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} x → {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s → {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s
have this : ∀ (x : α) (hx₁ : x ∈ s) (hx₂ : x ∈ U), {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s
Tactic: ⟨x, hx₁, hx₂⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set α
hU : IsOpen[inst.toTopologicalSpace] U
s : Set α
x : α
hx₁ : x ∈ s
hx₂ : x ∈ U
⊢ {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s
have hx₃ : ∃ V ∈ 𝓤 α, ball x V ⊆ U
Tactic: rw [← hU.mem_nhds_iff, mem_nhds_iff] at hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s
have obtain : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVU : ball x V ⊆ U), {s : Set α | (s ∩ U).Nonempty} ∈ 𝓝 s
Tactic: obtain ⟨V, hV, hVU⟩ := hx₂
Cleared hypotheses: hx₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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 α | (s ∩ U).Nonempty} ∈ 𝓝 s
have rw : ∃ (V : Set (Set α × Set α)),
  Membership.mem (γ := Filter (Set α × Set α)) (𝓤 (Set α)) V ∧ ball s V ⊆ {s : Set α | (s ∩ U).Nonempty}
Tactic: rw [mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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}
have refine : ball s (hausdorffEntourage V) ⊆ {s : Set α | (s ∩ U).Nonempty}
Tactic: refine ⟨_, Filter.mem_lift' hV, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
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
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s'
have obtain : ∀ (y : α) (hy : y ∈ (s, s').2) (hxy : (x, y) ∈ V), Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} s'
Tactic: obtain ⟨y, hy, hxy⟩ := hs' hx₁
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
F : Set α
hF : IsClosed[inst.toTopologicalSpace] F
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 F)
have simp_rw : IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {a : Set α | (a ∩ Fᶜ).Nonempty}
Tactic: simp_rw [Set.powerset, ← isOpen_compl_iff, Set.compl_setOf, ← Set.inter_compl_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClopen (X := Set α) {∅}
have left : IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
left : IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}
⊢ IsClopen (X := Set α) {∅}
have right : IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}
have left : IsClosed[(UniformSpace.hausdorff α).toTopologicalSpace] (𝒫 ∅)
Tactic: rw [← Set.powerset_empty]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsOpen[(UniformSpace.hausdorff α).toTopologicalSpace] {∅}
have right : Membership.mem (γ := Filter (Set α)) (Filter.lift' (𝓤 (Set α)) (ball ∅)) {∅}
Tactic: simp_rw [isOpen_iff_mem_nhds, Set.mem_singleton_iff, forall_eq, nhds_eq_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
F : Set α
⊢ Membership.mem (γ := Set (Set α)) (ball ∅ (hausdorffEntourage Set.univ)) F → Membership.mem (γ := Set (Set α)) {∅} F
have 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
Tactic: ⟨_, hF⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Membership.mem (γ := Filter (Set α)) (Filter.lift' (𝓤 (Set α)) (ball ∅)) {∅}
have 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
Tactic: filter_upwards [Filter.mem_lift' <| Filter.mem_lift' Filter.univ_mem] with F ⟨_, hF⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Filter.comap (fun (x : α × α) ↦ ({x.1}, {x.2})) ((𝓤 α).lift' hausdorffEntourage) = 𝓤 α
have simp_rw : ((𝓤 α).lift' fun (x : Set (α × α)) ↦ {x_1 : α × α | (x_1.1, x_1.2) ∈ x}) = 𝓤 α
Tactic: simp_rw [Filter.comap_lift'_eq, Function.comp_def, Set.preimage,
      singleton_mem_hausdorffEntourage]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ UniformContinuous (β := Set α) fun (x : Set α × Set α) ↦ x.1 ∪ x.2
have 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
Tactic: refine Filter.tendsto_lift'.mpr fun U hU => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
a : (Set α × Set α) × Set α × Set α
⊢ a ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U) →
    (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U
have h : ∀ (h₁ : (a.1.1, a.2.1) ∈ hausdorffEntourage U) (h₂ : (a.1.2, a.2.2) ∈ hausdorffEntourage U),
  (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U
Tactic: ⟨h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
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
have h : ∀ (a : (Set α × Set α) × Set α × Set α),
  Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
    {x : (Set α × Set α) × Set α × Set α |
      x ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U) →
        Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
          {x : (Set α × Set α) × Set α × Set α |
            (fun (a : (Set α × Set α) × Set α × Set α) ↦
                ((fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.1, (fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.2) ∈
                  hausdorffEntourage U)
              x}
          x}
    a
Tactic: filter_upwards [entourageProd_mem_uniformity (Filter.mem_lift' hU) (Filter.mem_lift' hU)]
    with _ ⟨h₁, h₂⟩ using union_mem_hausdorffEntourage U h₁ h₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
h :
  ∀ (a : (Set α × Set α) × Set α × Set α),
    Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
      {x : (Set α × Set α) × Set α × Set α |
        x ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U) →
          Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
            {x : (Set α × Set α) × Set α × Set α |
              (fun (a : (Set α × Set α) × Set α × Set α) ↦
                  ((fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.1, (fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.2) ∈
                    hausdorffEntourage U)
                x}
            x}
      a
⊢ ∀ᶠ (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
have h₁ : ∀ a ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U), (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U
Tactic: filter_upwards [entourageProd_mem_uniformity (Filter.mem_lift' hU) (Filter.mem_lift' hU)]
    with _ ⟨h₁, h₂⟩ using union_mem_hausdorffEntourage U h₁ h₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α
h :
  ∀ (a : (Set α × Set α) × Set α × Set α),
    Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
      {x : (Set α × Set α) × Set α × Set α |
        x ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U) →
          Membership.mem (γ := Set ((Set α × Set α) × Set α × Set α))
            {x : (Set α × Set α) × Set α × Set α |
              (fun (a : (Set α × Set α) × Set α × Set α) ↦
                  ((fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.1, (fun (x : Set α × Set α) ↦ x.1 ∪ x.2) a.2) ∈
                    hausdorffEntourage U)
                x}
            x}
      a
h₁ :
  ∀ a ∈ entourageProd (hausdorffEntourage U) (hausdorffEntourage U),
    (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage 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
have h₂ : ∀ (a : (Set α × Set α) × Set α × Set α) (h₁ : (a.1.1, a.2.1) ∈ hausdorffEntourage U)
  (h₂ : (a.1.2, a.2.2) ∈ hausdorffEntourage U), (a.1.1 ∪ a.1.2, a.2.1 ∪ a.2.2) ∈ hausdorffEntourage U
Tactic: filter_upwards [entourageProd_mem_uniformity (Filter.mem_lift' hU) (Filter.mem_lift' hU)]
    with _ ⟨h₁, h₂⟩ using union_mem_hausdorffEntourage U h₁ h₂