case pos
α : Type u_1
β : Type ?u.57659
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : x = y
⊢ infsep {x, y} = ENNReal.toReal (edist x y)

case neg
α : Type u_1
β : Type ?u.57659
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : ¬x = y
⊢ infsep {x, y} = ENNReal.toReal (edist x y)
α : Type u_1
β : Type ?u.57659
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infsep {x, y} = ENNReal.toReal (edist x y)
by_cases hxy : x = y
case pos
α : Type u_1
β : Type ?u.57659
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : x = y
⊢ infsep {y, y} = ENNReal.toReal (edist y y)
case pos
α : Type u_1
β : Type ?u.57659
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : x = y
⊢ infsep {x, y} = ENNReal.toReal (edist x y)
rw [hxy]
no goals
case pos
α : Type u_1
β : Type ?u.57659
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : x = y
⊢ infsep {y, y} = ENNReal.toReal (edist y y)
simp only [infsep_singleton, pair_eq_singleton, edist_self, ENNReal.zero_toReal]
no goals
case neg
α : Type u_1
β : Type ?u.57659
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : ¬x = y
⊢ infsep {x, y} = ENNReal.toReal (edist x y)
rw [infsep, einfsep_pair hxy]