α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x y : α
x✝ :
  (x, y) ∈
    (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹'
      ((fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) '' id U)
x' y' : α
hx' : (x', y') ∈ id U
h : x' ≈ x ∧ y' ≈ y
⊢ (x, y) ∈ id U
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x y : α
x✝ :
  (x, y) ∈
    (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹'
      ((fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) '' id U)
x' y' : α
hx' : (x', y') ∈ id U
h :
  (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (x', y') =
    (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) (x, y)
⊢ (x, y) ∈ id U
simp only [Prod.ext_iff, Quotient.eq] at h
no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x y : α
x✝ :
  (x, y) ∈
    (fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) ⁻¹'
      ((fun p => (Quotient.mk (separationSetoid α) p.fst, Quotient.mk (separationSetoid α) p.snd)) '' id U)
x' y' : α
hx' : (x', y') ∈ id U
h : x' ≈ x ∧ y' ≈ y
⊢ (x, y) ∈ id U
exact (((separationRel_iff_inseparable.1 h.1).prod
  (separationRel_iff_inseparable.1 h.2)).mem_open_iff hU.2).1 hx'