simp_rw [inf_principal_eq_bot, inf_eq_bot_iff, mem_uniform_nhds_set_iff] at h ⊢
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : 𝓝ᵘ s ⊓ 𝓟 t = ⊥
⊢ 𝓝ᵘ s ⊓ 𝓝ᵘ t = ⊥
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s✝ t✝ : Set α
x u v : Set (α × α)
inst✝ : UniformSpace α
s t : Set α
h : ∃ u ∈ 𝓤 α, thickening u s ⊆ tᶜ
⊢ ∃ U, (∃ u ∈ 𝓤 α, thickening u s ⊆ U) ∧ ∃ V, (∃ u ∈ 𝓤 α, thickening u t ⊆ V) ∧ U ∩ V = ∅