case h
α : Type u
β : Type v
X : Type ?u.28557
ι : Type ?u.28560
inst✝ : PseudoMetricSpace α
x✝¹ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s : Set α
ε : ℝ
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x {p | dist p.fst p.snd < ε} ↔ x✝ ∈ ball x ε
α : Type u
β : Type v
X : Type ?u.28557
ι : Type ?u.28560
inst✝ : PseudoMetricSpace α
x✝ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s : Set α
ε : ℝ
x : α
⊢ UniformSpace.ball x {p | dist p.fst p.snd < ε} = ball x ε
ext
no goals
case h
α : Type u
β : Type v
X : Type ?u.28557
ι : Type ?u.28560
inst✝ : PseudoMetricSpace α
x✝¹ y z : α
δ ε✝ ε₁ ε₂ : ℝ
s : Set α
ε : ℝ
x x✝ : α
⊢ x✝ ∈ UniformSpace.ball x {p | dist p.fst p.snd < ε} ↔ x✝ ∈ ball x ε
simp [dist_comm, UniformSpace.ball]