refine ⟨_, ⟨v, hv, subset_rfl⟩, _, ⟨v, hv, subset_rfl⟩, ?h⟩
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u✝ v✝ : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
u : Set (α × α)
hu : u ∈ 𝓤 α
hsu : thickening u s ⊆ tᶜ
v : Set (α × α)
hv : v ∈ 𝓤 α
hvs : ∀ {a b : α}, (a, b) ∈ v → (b, a) ∈ v
hvu : v ○ v ⊆ u
⊢ thickening v s ∩ thickening v t = ∅