case intro
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ 0 < einfsep s
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
⊢ 0 < einfsep s
cases nonempty_fintype s
case pos
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ 0 < einfsep s

case neg
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬Set.Nontrivial s
⊢ 0 < einfsep s
case intro
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ 0 < einfsep s
by_cases hs : s.Nontrivial
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x✝ y✝ z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : Set.Nontrivial s
x : α
_hx : x ∈ s
y : α
_hy : y ∈ s
hxy : x ≠ y
hxy' : einfsep s = edist x y
⊢ 0 < einfsep s
case pos
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ 0 < einfsep s
rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
no goals
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x✝ y✝ z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : Set.Nontrivial s
x : α
_hx : x ∈ s
y : α
_hy : y ∈ s
hxy : x ≠ y
hxy' : einfsep s = edist x y
⊢ 0 < einfsep s
exact hxy'.symm ▸ edist_pos.2 hxy
case neg
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : Set.Subsingleton s
⊢ 0 < einfsep s
case neg
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : ¬Set.Nontrivial s
⊢ 0 < einfsep s
rw [not_nontrivial_iff] at hs
no goals
case neg
α : Type u_1
β : Type ?u.51801
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
hs : Set.Subsingleton s
⊢ 0 < einfsep s
exact hs.einfsep.symm ▸ WithTop.zero_lt_top