-- Mathlib/Topology/MetricSpace/Completion.lean
theorem mem_uniformity_dist (s : Set (Completion α × Completion α)) :
    s ∈ 𝓤 (Completion α) ↔ ∃ ε > 0, ∀ {a b}, dist a b < ε → (a, b) ∈ s

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.mk
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
a b : Completion α
hp : (a, b) ∈ t1
⊢ (a, b) ∈ s

Tactic:
have : dist a b < ε := A a b hp

Result:
case mpr.intro.intro.intro.intro.intro.intro.mk
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
a b : Completion α
hp : (a, b) ∈ t1
this : dist a b < ε
⊢ (a, b) ∈ s

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ ∀ (a b : α), ε ≤ dist ↑a ↑b ∨ (↑a, ↑b) ∈ t

Tactic:
intro x y

Result:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
⊢ ε ≤ dist ↑x ↑y ∨ (↑x, ↑y) ∈ t

Proof state:
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
⊢ s ∈ 𝓤 (Completion α)

Tactic:
refine mem_of_superset ht1 ?_

Result:
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht : t1 ×ˢ t2 ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' {x | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
⊢ t1 ⊆ s

Proof state:
case neg
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
⊢ ε ≤ dist x y ∨ (↑x, ↑y) ∈ t

Tactic:
have Z := hε (not_le.1 h)

Result:
case neg
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
A : {x | (↑x.1, ↑x.2) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ {x | (↑x.1, ↑x.2) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
Z : (x, y) ∈ {x | (↑x.1, ↑x.2) ∈ t}
⊢ ε ≤ dist x y ∨ (↑x, ↑y) ∈ t