no goals
α : Type u
β : Type v
γ : Type ?u.36228
δ : Type ?u.36231
ε : Type ?u.36234
ζ : Type ?u.36237
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
a : α
b : β
s : Set (α × β)
⊢ (∃ i, ((a ∈ i.fst ∧ IsOpen i.fst) ∧ b ∈ i.snd ∧ IsOpen i.snd) ∧ i.fst ×ˢ i.snd ⊆ s) ↔
    ∃ u v, IsOpen u ∧ a ∈ u ∧ IsOpen v ∧ b ∈ v ∧ u ×ˢ v ⊆ s
simp only [Prod.exists, and_comm, and_assoc, and_left_comm]