case pos
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ infsep s
hs : Set.Nontrivial s
⊢ d ≤ dist x y

case neg
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ infsep s
hs : ¬Set.Nontrivial s
⊢ d ≤ dist x y
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ infsep s
⊢ d ≤ dist x y
by_cases hs : s.Nontrivial
no goals
case pos
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ infsep s
hs : Set.Nontrivial s
⊢ d ≤ dist x y
exact hs.le_infsep_iff.1 hd x hx y hy hxy
case neg
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ infsep s
hs : Set.Subsingleton s
⊢ d ≤ dist x y
case neg
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ infsep s
hs : ¬Set.Nontrivial s
⊢ d ≤ dist x y
rw [not_nontrivial_iff] at hs
case neg
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ 0
hs : Set.Subsingleton s
⊢ d ≤ dist x y
case neg
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ infsep s
hs : Set.Subsingleton s
⊢ d ≤ dist x y
rw [hs.infsep_zero] at hd
no goals
case neg
α : Type u_1
β : Type ?u.59969
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
s t : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ 0
hs : Set.Subsingleton s
⊢ d ≤ dist x y
exact le_trans hd dist_nonneg