-- 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:
α : 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 b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ dist a b < ε

Tactic:
have I := ht this

Result:
α : 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 b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
I : ((a, b), a, a) ∈ (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}
⊢ dist a b < ε

Proof state:
case mpr.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ s ∈ 𝓤 (Completion α)

Tactic:
let r : Set (ℝ × ℝ) := { p | dist p.1 p.2 < ε }

Result:
case mpr.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 < ε}
⊢ s ∈ 𝓤 (Completion α)

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✝ < ε
x y : α
⊢ ε ≤ dist x y ∨ (↑x, ↑y) ∈ t

Tactic:
by_cases h : ε ≤ dist x y

Result:
case pos
α : 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

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

Proof state:
case mpr.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 < ε}
⊢ s ∈ 𝓤 (Completion α)

Tactic:
have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos

Result:
case mpr.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 ∈ 𝓤 ℝ
⊢ s ∈ 𝓤 (Completion α)

Proof state:
α : 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 < ε
this : {x | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} = {p | ε ≤ dist p.1 p.2} ∪ t
⊢ IsClosed {p | ε ≤ dist p.1 p.2}

Tactic:
exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous

Result:
no goals

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✝ < ε
x y : α
⊢ ε ≤ dist ↑x ↑y ∨ (↑x, ↑y) ∈ t

Tactic:
rw [Completion.dist_eq]

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 mp.intro.intro.intro.intro.intro
α : 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}
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
refine ⟨ε, εpos, @fun x y hxy ↦ ?_⟩

Result:
case mp.intro.intro.intro.intro.intro
α : 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) ∈ s

Proof state:
case mp.intro.intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
t : Set (Completion α × Completion α)
ht : t ∈ 𝓤 (Completion α)
tclosed : IsClosed t
ts : t ⊆ s
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
have A : { x : α × α | (↑x.1, ↑x.2) ∈ t } ∈ uniformity α :=
  uniformContinuous_def.1 (uniformContinuous_coe α) t ht

Result:
case mp.intro.intro.intro
α : 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} ∈ 𝓤 α
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) → ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

case mpr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ (∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (Completion α)

Proof state:
case mp
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) → ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
intro hs

Result:
case mp
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s