[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ dist x x = 0
[PROOFSTEP]
refine' induction_on x _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ IsClosed {a | dist a a = 0}
[PROOFSTEP]
refine' isClosed_eq _ continuous_const
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ Continuous fun a => dist a a
[PROOFSTEP]
exact Completion.continuous_dist continuous_id continuous_id
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ ∀ (a : α), dist (↑α a) (↑α a) = 0
[PROOFSTEP]
intro a
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist (↑α a) (↑α a) = 0
[PROOFSTEP]
rw [Completion.dist_eq, dist_self]
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ dist x y = dist y x
[PROOFSTEP]
refine' induction_on₂ x y _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed {x | dist x.fst x.snd = dist x.snd x.fst}
[PROOFSTEP]
exact
  isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
    (Completion.continuous_dist continuous_snd continuous_fst)
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ ∀ (a b : α), dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
[PROOFSTEP]
intro a b
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist (↑α a) (↑α b) = dist (↑α b) (↑α a)
[PROOFSTEP]
rw [Completion.dist_eq, Completion.dist_eq, dist_comm]
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
refine' induction_on₃ x y z _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ IsClosed {x | dist x.fst x.snd.snd ≤ dist x.fst x.snd.fst + dist x.snd.fst x.snd.snd}
[PROOFSTEP]
refine' isClosed_le _ (Continuous.add _ _)
[GOAL]
case refine'_1.refine'_1
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x => dist x.fst x.snd.snd
[PROOFSTEP]
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
[GOAL]
case refine'_1.refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x => dist x.fst x.snd.fst
[PROOFSTEP]
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
[GOAL]
case refine'_1.refine'_3
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous fun x => dist x.snd.fst x.snd.snd
[PROOFSTEP]
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
⊢ ∀ (a b c : α), dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
[PROOFSTEP]
intro a b c
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist (↑α a) (↑α c) ≤ dist (↑α a) (↑α b) + dist (↑α b) (↑α c)
[PROOFSTEP]
rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]
[GOAL]
case refine'_2
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c
[PROOFSTEP]
exact dist_triangle a b c
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) → ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
intro hs
[GOAL]
case mp
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩
[GOAL]
case mp.intro.intro.intro
α : Type u
β : Type v
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
[PROOFSTEP]
have A : {x : α × α | (↑x.1, ↑x.2) ∈ t} ∈ uniformity α := uniformContinuous_def.1 (uniformContinuous_coe α) t ht
[GOAL]
case mp.intro.intro.intro
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
refine' ⟨ε, εpos, @fun x y hxy ↦ _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ (x, y) ∈ s
[PROOFSTEP]
have : ε ≤ dist x y ∨ (x, y) ∈ t := by
  refine' induction_on₂ x y _ _
  · have :
      {x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} =
        {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t :=
      by ext; simp
    rw [this]
    apply IsClosed.union _ tclosed
    exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
  · intro x y
    rw [Completion.dist_eq]
    by_cases h : ε ≤ dist x y
    · exact Or.inl h
    · have Z := hε (not_le.1 h)
      simp only [Set.mem_setOf_eq] at Z 
      exact Or.inr Z
[GOAL]
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ ε ≤ dist x y ∨ (x, y) ∈ t
[PROOFSTEP]
refine' induction_on₂ x y _ _
[GOAL]
case refine'_1
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ IsClosed {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t}
[PROOFSTEP]
have :
  {x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t :=
  by ext; simp
[GOAL]
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
x✝ : Completion α × Completion α
⊢ x✝ ∈ {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} ↔ x✝ ∈ {p | ε ≤ dist p.fst p.snd} ∪ t
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
⊢ IsClosed {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t}
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_1
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
⊢ IsClosed ({p | ε ≤ dist p.fst p.snd} ∪ t)
[PROOFSTEP]
apply IsClosed.union _ tclosed
[GOAL]
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : {x | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t} = {p | ε ≤ dist p.fst p.snd} ∪ t
⊢ IsClosed {p | ε ≤ dist p.fst p.snd}
[PROOFSTEP]
exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
[GOAL]
case refine'_2
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
⊢ ∀ (a b : α), ε ≤ dist (↑α a) (↑α b) ∨ (↑α a, ↑α b) ∈ t
[PROOFSTEP]
intro x y
[GOAL]
case refine'_2
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
⊢ ε ≤ dist (↑α x) (↑α y) ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
rw [Completion.dist_eq]
[GOAL]
case refine'_2
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
by_cases h : ε ≤ dist x y
[GOAL]
case pos
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ε ≤ dist x y
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
exact Or.inl h
[GOAL]
case neg
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
have Z := hε (not_le.1 h)
[GOAL]
case neg
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
Z : (x, y) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
simp only [Set.mem_setOf_eq] at Z 
[GOAL]
case neg
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x✝ y✝ : Completion α
hxy : dist x✝ y✝ < ε
x y : α
h : ¬ε ≤ dist x y
Z : (↑α x, ↑α y) ∈ t
⊢ ε ≤ dist x y ∨ (↑α x, ↑α y) ∈ t
[PROOFSTEP]
exact Or.inr Z
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : ε ≤ dist x y ∨ (x, y) ∈ t
⊢ (x, y) ∈ s
[PROOFSTEP]
simp only [not_le.mpr hxy, false_or_iff, not_le] at this 
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
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.fst, ↑α x.snd) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : α}, dist a b < ε → (a, b) ∈ {x | (↑α x.fst, ↑α x.snd) ∈ t}
x y : Completion α
hxy : dist x y < ε
this : (x, y) ∈ t
⊢ (x, y) ∈ s
[PROOFSTEP]
exact ts this
[GOAL]
case mpr
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ (∃ ε, ε > 0 ∧ ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (Completion α)
[PROOFSTEP]
rintro ⟨ε, εpos, hε⟩
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
let r : Set (ℝ × ℝ) := {p | dist p.1 p.2 < ε}
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
T : {x | (dist x.fst.fst x.fst.snd, dist x.snd.fst x.snd.snd) ∈ r} ∈ 𝓤 (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
simp only [uniformity_prod_eq_prod, mem_prod_iff, exists_prop, Filter.mem_map, Set.mem_setOf_eq] at T 
[GOAL]
case mpr.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
T :
  ∃ t₁,
    t₁ ∈ 𝓤 (Completion α) ∧
      ∃ t₂,
        t₂ ∈ 𝓤 (Completion α) ∧
          t₁ ×ˢ t₂ ⊆
            (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
              {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
rcases T with ⟨t1, ht1, t2, ht2, ht⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ s ∈ 𝓤 (Completion α)
[PROOFSTEP]
refine' mem_of_superset ht1 _
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ t1 ⊆ s
[PROOFSTEP]
have A : ∀ a b : Completion α, (a, b) ∈ t1 → dist a b < ε :=
  by
  intro a b hab
  have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
  have I := ht this
  simp [Completion.dist_self, Real.dist_eq, Completion.dist_comm] at I 
  exact lt_of_le_of_lt (le_abs_self _) I
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
[PROOFSTEP]
intro a b hab
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
⊢ dist a b < ε
[PROOFSTEP]
have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ dist a b < ε
[PROOFSTEP]
have I := ht this
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
I :
  ((a, b), a, a) ∈
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
⊢ dist a b < ε
[PROOFSTEP]
simp [Completion.dist_self, Real.dist_eq, Completion.dist_comm] at I 
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
I : |dist a b| < ε
⊢ dist a b < ε
[PROOFSTEP]
exact lt_of_le_of_lt (le_abs_self _) I
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
⊢ t1 ⊆ s
[PROOFSTEP]
show t1 ⊆ s
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
⊢ t1 ⊆ s
[PROOFSTEP]
rintro ⟨a, b⟩ hp
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.mk
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
a b : Completion α
hp : (a, b) ∈ t1
⊢ (a, b) ∈ s
[PROOFSTEP]
have : dist a b < ε := A a b hp
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.mk
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p | dist p.fst p.snd < ε}
this✝ : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : t1 ∈ 𝓤 (Completion α)
t2 : Set (Completion α × Completion α)
ht2 : t2 ∈ 𝓤 (Completion α)
ht :
  t1 ×ˢ t2 ⊆
    (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹'
      {x | dist (dist x.fst.fst x.fst.snd) (dist x.snd.fst x.snd.snd) < ε}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
a b : Completion α
hp : (a, b) ∈ t1
this : dist a b < ε
⊢ (a, b) ∈ s
[PROOFSTEP]
exact hε this
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
⊢ x = y
[PROOFSTEP]
have : SeparatedSpace (Completion α) := by infer_instance
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
⊢ SeparatedSpace (Completion α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
⊢ x = y
[PROOFSTEP]
refine' separated_def.1 this x y fun s hs ↦ _
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
⊢ (x, y) ∈ s
[PROOFSTEP]
rcases(Completion.mem_uniformity_dist s).1 hs with ⟨ε, εpos, hε⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
[PROOFSTEP]
rw [← h] at εpos 
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
x y : Completion α
h : dist x y = 0
this : SeparatedSpace (Completion α)
s : Set (Completion α × Completion α)
hs : s ∈ 𝓤 (Completion α)
ε : ℝ
εpos : ε > dist x y
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ (x, y) ∈ s
[PROOFSTEP]
exact hε εpos
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ (ε : { ε // 0 < ε }), 𝓟 {p | dist p.fst p.snd < ↑ε}
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ (ε : { ε // 0 < ε }), 𝓟 {p | dist p.fst p.snd < ↑ε}
[PROOFSTEP]
rw [mem_iInf_of_directed]
[GOAL]
case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.fst p.snd < ↑i}
[PROOFSTEP]
simp [Completion.mem_uniformity_dist, subset_def]
[GOAL]
case a.h
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Directed (fun x x_1 => x ≥ x_1) fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}
[PROOFSTEP]
rintro ⟨r, hr⟩ ⟨p, hp⟩
[GOAL]
case a.h.mk.mk
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ ∃ z,
    (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := r, property := hr })
        ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) z) ∧
      (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := p, property := hp })
        ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) z)
[PROOFSTEP]
use⟨min r p, lt_min hr hp⟩
[GOAL]
case h
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := r, property := hr })
      ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := min r p, property := (_ : 0 < min r p) }) ∧
    (fun x x_1 => x ≥ x_1) ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := p, property := hp })
      ((fun ε => 𝓟 {p | dist p.fst p.snd < ↑ε}) { val := min r p, property := (_ : 0 < min r p) })
[PROOFSTEP]
simp (config := { contextual := true }) [lt_min_iff]
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ (ε : ℝ) (_ : ε > 0), 𝓟 {p | dist p.fst p.snd < ε}
[PROOFSTEP]
simpa [iInf_subtype] using @Completion.uniformity_dist' α _
[GOAL]
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
⊢ UniformSpace (Completion α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => dist (Completion.extension f x.fst) (Completion.extension f x.snd)
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous fun x => ↑K * dist x.fst x.snd
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α), dist (Completion.extension f (↑α a)) (Completion.extension f (↑α b)) ≤ ↑K * dist (↑α a) (↑α b)
[PROOFSTEP]
simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x => dist (Completion.extension f x.fst) (Completion.extension f x.snd)
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous fun x => dist x.fst x.snd
[PROOFSTEP]
continuity
[GOAL]
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : MetricSpace β
inst✝ : CompleteSpace β
f : α → β
h : Isometry f
x y : Completion α
x✝¹ x✝ : α
⊢ dist (Completion.extension f (↑α x✝¹)) (Completion.extension f (↑α x✝)) = dist (↑α x✝¹) (↑α x✝)
[PROOFSTEP]
simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]
