case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ (ε : { ε // 0 < ε }), 𝓟 {p | dist p.fst p.snd < ↑ε}
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ (ε : { ε // 0 < ε }), 𝓟 {p | dist p.fst p.snd < ↑ε}
ext s
case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.fst p.snd < ↑i}

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 < ↑ε}
case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ s ∈ ⨅ (ε : { ε // 0 < ε }), 𝓟 {p | dist p.fst p.snd < ↑ε}
rw [mem_iInf_of_directed]
no goals
case a
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ s ∈ 𝓤 (Completion α) ↔ ∃ i, s ∈ 𝓟 {p | dist p.fst p.snd < ↑i}
simp [Completion.mem_uniformity_dist, subset_def]
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)
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 < ↑ε}
rintro ⟨r, hr⟩ ⟨p, hp⟩
case a.h.mk.mk
α : 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) })
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)
use ⟨min r p, lt_min hr hp⟩
no goals
case a.h.mk.mk
α : 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) })
simp (config := { contextual := true }) [lt_min_iff]