no goals
α : Type u
β : Type v
γ : Type ?u.50921
δ : Type ?u.50924
ε : Type ?u.50927
ζ : Type ?u.50930
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set (α × α)
x : α
hx : s ∈ 𝓝 (x, x)
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s
simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx