-- Mathlib/Topology/UniformSpace/Basic.lean
theorem nhdset_of_mem_uniformity {d : Set (α × α)} (s : Set (α × α)) (hd : d ∈ 𝓤 α) :
    ∃ t : Set (α × α), IsOpen t ∧ s ⊆ t ∧
      t ⊆ { p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d }

Proof state:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
let cl_d := { p : α × α | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d }

Result:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Proof state:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
x✝ : α × α
a b : α
hp : (a, b) ∈ s
⊢ ∃ a_1 b_1, ∃ (i : (a_1, b_1) ∈ s), (a, b) ∈ t (a_1, b_1) i

Tactic:
exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
x✝ : α × α
a b : α
hp : (a, b) ∈ s
⊢ (a, b) ∈ ⋃ p, ⋃ (h : p ∈ s), t p h

Tactic:
simp only [mem_iUnion, Prod.exists]

Result:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
x✝ : α × α
a b : α
hp : (a, b) ∈ s
⊢ ∃ a_1 b_1, ∃ (i : (a_1, b_1) ∈ s), (a, b) ∈ t (a_1, b_1) i

Proof state:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ 𝓝 (x, y)

Tactic:
rw [nhds_eq_uniformity_prod, mem_lift'_sets]

Result:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, {y | (y, x) ∈ t} ×ˢ {y_1 | (y, y_1) ∈ t} ⊆ cl_d

case hh
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s => {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}

Proof state:
case hh
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ Monotone fun s => {y | (y, x) ∈ s} ×ˢ {y_1 | (y, y_1) ∈ s}

Tactic:
exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
exact ⟨(⋃ p : α × α, ⋃ h : p ∈ s, t p h : Set (α × α)),
  isOpen_iUnion fun p : α × α => isOpen_iUnion fun hp => (ht p hp).right.left,
  fun ⟨a, b⟩ hp => by
    simp only [mem_iUnion, Prod.exists]; exact ⟨a, b, hp, (ht (a, b) hp).right.right⟩,
  iUnion_subset fun p => iUnion_subset fun hp => (ht p hp).left⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x✝ : α × α
x y : α
hp : (x, y) ∈ s
⊢ ∃ t ∈ 𝓤 α, {y | (y, x) ∈ t} ×ˢ {y_1 | (y, y_1) ∈ t} ⊆ cl_d

Tactic:
exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
this : ∀ p ∈ s, ∃ t ⊆ cl_d, IsOpen t ∧ p ∈ t
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

Tactic:
choose t ht using this

Result:
α : Type ua
inst✝ : UniformSpace α
d s : Set (α × α)
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen (t p a) ∧ p ∈ t p a
⊢ ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}