[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
d : ℝ≥0∞
⊢ d ≤ einfsep s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ edist x y
[PROOFSTEP]
simp_rw [einfsep, le_iInf_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep s = 0 ↔ ∀ (C : ℝ≥0∞), 0 < C → ∃ x x_1 y x_2 _hxy, edist x y < C
[PROOFSTEP]
simp_rw [einfsep, ← _root_.bot_eq_zero, iInf_eq_bot, iInf_lt_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ 0 < einfsep s ↔ ∃ C _hC, ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → C ≤ edist x y
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, einfsep_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ (¬∀ (C : ℝ≥0∞), 0 < C → ∃ x x_1 y x_2 _hxy, edist x y < C) ↔
    ∃ C _hC, ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → C ≤ edist x y
[PROOFSTEP]
simp only [not_forall, not_exists, not_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep s = ⊤ ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → edist x y = ⊤
[PROOFSTEP]
simp_rw [einfsep, iInf_eq_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep s < ⊤ ↔ ∃ x x_1 y x_2 _hxy, edist x y < ⊤
[PROOFSTEP]
simp_rw [einfsep, iInf_lt_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep s ≠ ⊤ ↔ ∃ x x_1 y x_2 _hxy, edist x y ≠ ⊤
[PROOFSTEP]
simp_rw [← lt_top_iff_ne_top, einfsep_lt_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
d : ℝ≥0∞
⊢ einfsep s < d ↔ ∃ x x_1 y x_2 _h, edist x y < d
[PROOFSTEP]
simp_rw [einfsep, iInf_lt_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hs : einfsep s < ⊤
⊢ Set.Nontrivial s
[PROOFSTEP]
rcases einfsep_lt_top.1 hs with ⟨_, hx, _, hy, hxy, _⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hs : einfsep s < ⊤
w✝¹ : α
hx : w✝¹ ∈ s
w✝ : α
hy : w✝ ∈ s
hxy : w✝¹ ≠ w✝
h✝ : edist w✝¹ w✝ < ⊤
⊢ Set.Nontrivial s
[PROOFSTEP]
exact ⟨_, hx, _, hy, hxy⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = ⊤
[PROOFSTEP]
rw [einfsep_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Subsingleton s
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → edist x y = ⊤
[PROOFSTEP]
exact fun _ hx _ hy hxy => (hxy <| hs hx hy).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s✝ t : Set α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ einfsep (f '' s) ↔ ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → f x ≠ f y → d ≤ edist (f x) (f y)
[PROOFSTEP]
simp_rw [le_einfsep_iff, ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s✝ t : Set α
ι : Type u_3
o : Option ι
s : ι → Set α
⊢ einfsep (⋃ (i : ι) (_ : i ∈ o), s i) = ⨅ (i : ι) (_ : i ∈ o), einfsep (s i)
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s✝ t : Set α
ι : Type u_3
s : ι → Set α
⊢ einfsep (⋃ (i : ι) (_ : i ∈ none), s i) = ⨅ (i : ι) (_ : i ∈ none), einfsep (s i)
[PROOFSTEP]
simp
[GOAL]
case some
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s✝ t : Set α
ι : Type u_3
s : ι → Set α
val✝ : ι
⊢ einfsep (⋃ (i : ι) (_ : i ∈ Option.some val✝), s i) = ⨅ (i : ι) (_ : i ∈ Option.some val✝), einfsep (s i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep (insert x s) ≤ ⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y
[PROOFSTEP]
simp_rw [le_iInf_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ ∀ (i : α), i ∈ s → x ≠ i → einfsep (insert x s) ≤ edist x i
[PROOFSTEP]
refine' fun _ hy hxy => einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ hy) hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ edist x y ⊓ edist y x ≤ einfsep {x, y}
[PROOFSTEP]
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 = y →
      ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1
[PROOFSTEP]
rintro a (rfl | rfl) b (rfl | rfl) hab
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : EDist α
y : α
s t : Set α
b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b
[PROOFSTEP]
try simp only [le_refl, true_or, or_true]
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : EDist α
y : α
s t : Set α
b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b
[PROOFSTEP]
simp only [le_refl, true_or, or_true]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : EDist α
s t : Set α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b
[PROOFSTEP]
try simp only [le_refl, true_or, or_true]
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : EDist α
s t : Set α
a b : α
hab : a ≠ b
⊢ edist a b ≤ edist a b ∨ edist b a ≤ edist a b
[PROOFSTEP]
simp only [le_refl, true_or, or_true]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : EDist α
s t : Set α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b
[PROOFSTEP]
try simp only [le_refl, true_or, or_true]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : EDist α
s t : Set α
a b : α
hab : a ≠ b
⊢ edist b a ≤ edist a b ∨ edist a b ≤ edist a b
[PROOFSTEP]
simp only [le_refl, true_or, or_true]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : EDist α
x : α
s t : Set α
b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
[PROOFSTEP]
try simp only [le_refl, true_or, or_true]
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : EDist α
x : α
s t : Set α
b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
[PROOFSTEP]
simp only [le_refl, true_or, or_true]
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : EDist α
y : α
s t : Set α
b : α
hab : b ≠ b
⊢ edist b y ≤ edist b b ∨ edist y b ≤ edist b b
[PROOFSTEP]
contradiction
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : EDist α
x : α
s t : Set α
b : α
hab : b ≠ b
⊢ edist x b ≤ edist b b ∨ edist b x ≤ edist b b
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {x, y} ≤ edist y x
[PROOFSTEP]
rw [pair_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {y, x} ≤ edist y x
[PROOFSTEP]
exact einfsep_pair_le_left hxy.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
⊢ einfsep s = ⨅ (d : ↑(offDiag s)), uncurry edist ↑d
[PROOFSTEP]
refine' eq_of_forall_le_iff fun _ => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
x✝ : ℝ≥0∞
⊢ x✝ ≤ einfsep s ↔ x✝ ≤ ⨅ (d : ↑(offDiag s)), uncurry edist ↑d
[PROOFSTEP]
simp_rw [le_einfsep_iff, le_iInf_iff, imp_forall_iff, SetCoe.forall, mem_offDiag, Prod.forall, uncurry_apply_pair,
  and_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : EDist α
x y : α
s t : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ einfsep s = Finset.inf (toFinset (offDiag s)) (uncurry edist)
[PROOFSTEP]
refine' eq_of_forall_le_iff fun _ => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : EDist α
x y : α
s t : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
x✝ : ℝ≥0∞
⊢ x✝ ≤ einfsep s ↔ x✝ ≤ Finset.inf (toFinset (offDiag s)) (uncurry edist)
[PROOFSTEP]
simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, mem_toFinset, mem_offDiag, Prod.forall, uncurry_apply_pair,
  and_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Finite s
⊢ Set.einfsep s = Finset.inf (Finite.toFinset (_ : Set.Finite (offDiag s))) (uncurry edist)
[PROOFSTEP]
refine' eq_of_forall_le_iff fun _ => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Finite s
x✝ : ℝ≥0∞
⊢ x✝ ≤ Set.einfsep s ↔ x✝ ≤ Finset.inf (Finite.toFinset (_ : Set.Finite (offDiag s))) (uncurry edist)
[PROOFSTEP]
simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, Finite.mem_toFinset, mem_offDiag, Prod.forall,
  uncurry_apply_pair, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
⊢ einfsep ↑s = Finset.inf (Finset.offDiag s) (uncurry edist)
[PROOFSTEP]
simp_rw [einfsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
⊢ ∃ x x_1 y x_2 _hxy, einfsep s = edist x y
[PROOFSTEP]
classical
cases nonempty_fintype s
simp_rw [einfsep_of_fintype]
rcases@Finset.exists_mem_eq_inf _ _ _ _ s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩
simp_rw [mem_toFinset] at hxy
refine' ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
⊢ ∃ x x_1 y x_2 _hxy, einfsep s = edist x y
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x x_1 y x_2 _hxy, einfsep s = edist x y
[PROOFSTEP]
simp_rw [einfsep_of_fintype]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x h y h h, Finset.inf (toFinset (offDiag s)) (uncurry edist) = edist x y
[PROOFSTEP]
rcases@Finset.exists_mem_eq_inf _ _ _ _ s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ Finset.Nonempty (toFinset (offDiag s))
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ toFinset (offDiag s)
hed : Finset.inf (toFinset (offDiag s)) (uncurry edist) = uncurry edist w
⊢ ∃ x h y h h, Finset.inf (toFinset (offDiag s)) (uncurry edist) = edist x y
[PROOFSTEP]
simp_rw [mem_toFinset] at hxy
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : EDist α
x y : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hed : Finset.inf (toFinset (offDiag s)) (uncurry edist) = uncurry edist w
hxy : w ∈ offDiag s
⊢ ∃ x h y h h, Finset.inf (toFinset (offDiag s)) (uncurry edist) = edist x y
[PROOFSTEP]
refine' ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {x, y} = edist x y
[PROOFSTEP]
nth_rw 1 [← min_self (edist x y)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ einfsep {x, y} = min (edist x y) (edist x y)
[PROOFSTEP]
convert einfsep_pair_eq_inf hxy using 2
[GOAL]
case h.e'_3.h.e'_2
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
⊢ edist x y = edist y x
[PROOFSTEP]
rw [edist_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
⊢ einfsep (insert x s) = (⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y) ⊓ einfsep s
[PROOFSTEP]
refine' le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
⊢ (⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y) ⊓ einfsep s ≤ einfsep (insert x s)
[PROOFSTEP]
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 ∈ s →
      ∀ (y : α),
        y = x ∨ y ∈ s → x_1 ≠ y → ⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ einfsep s ≤ edist x_1 y
[PROOFSTEP]
rintro y (rfl | hy) z (rfl | hz) hyz
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
y z✝ : α
s t : Set α
z : α
hyz : z ≠ z
⊢ ⨅ (y : α) (_ : y ∈ s) (_ : z ≠ y), edist z y ≤ edist z z ∨ einfsep s ≤ edist z z
[PROOFSTEP]
exact False.elim (hyz rfl)
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
y✝ z✝ : α
s t : Set α
y z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ (y_1 : α) (_ : y_1 ∈ s) (_ : y ≠ y_1), edist y y_1 ≤ edist y z ∨ einfsep s ≤ edist y z
[PROOFSTEP]
exact Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
y✝ z✝ : α
s t : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ (y : α) (_ : y ∈ s) (_ : z ≠ y), edist z y ≤ edist y z ∨ einfsep s ≤ edist y z
[PROOFSTEP]
rw [edist_comm]
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
y✝ z✝ : α
s t : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ (y : α) (_ : y ∈ s) (_ : z ≠ y), edist z y ≤ edist z y ∨ einfsep s ≤ edist z y
[PROOFSTEP]
exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y✝ z✝ : α
s t : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y ≤ edist y z ∨ einfsep s ≤ edist y z
[PROOFSTEP]
exact Or.inr (einfsep_le_edist_of_mem hy hz hyz)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ einfsep {x, y, z} = edist x y ⊓ edist x z ⊓ edist y z
[PROOFSTEP]
simp_rw [einfsep_insert, iInf_insert, iInf_singleton, einfsep_singleton, inf_top_eq, ciInf_pos hxy, ciInf_pos hyz,
  ciInf_pos hxz]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
x y z : α
s✝ t : Set α
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
⊢ c ≤ einfsep (pi univ s)
[PROOFSTEP]
refine' le_einfsep fun x hx y hy hxy => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : x ∈ pi univ s
y : (i : β) → π i
hy : y ∈ pi univ s
hxy : x ≠ y
⊢ c ≤ edist x y
[PROOFSTEP]
rw [mem_univ_pi] at hx hy
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y
[PROOFSTEP]
rcases Function.ne_iff.mp hxy with ⟨i, hi⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
x✝ y✝ z : α
s✝ t : Set α
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (π b)
s : (b : β) → Set (π b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ einfsep (s b)
x : (i : β) → π i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → π i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
i : β
hi : x i ≠ y i
⊢ c ≤ edist x y
[PROOFSTEP]
exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ Set.Subsingleton s
[PROOFSTEP]
rw [einfsep_top] at hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → edist x y = ⊤
⊢ Set.Subsingleton s
[PROOFSTEP]
exact fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : Set.Nontrivial s
⊢ einfsep s ≠ ⊤
[PROOFSTEP]
contrapose! hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ ¬Set.Nontrivial s
[PROOFSTEP]
rw [not_nontrivial_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : einfsep s = ⊤
⊢ Set.Subsingleton s
[PROOFSTEP]
exact subsingleton_of_einfsep_eq_top hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : Set.Nontrivial s
⊢ einfsep s < ⊤
[PROOFSTEP]
rw [lt_top_iff_ne_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
hs : Set.Nontrivial s
⊢ einfsep s ≠ ⊤
[PROOFSTEP]
exact hs.einfsep_ne_top
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
⊢ 0 < einfsep s
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ 0 < einfsep s
[PROOFSTEP]
by_cases hs : s.Nontrivial
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
[GOAL]
case pos.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact hxy'.symm ▸ edist_pos.2 hxy
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [not_nontrivial_iff] at hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact hs.einfsep.symm ▸ WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
⊢ ∃ C _hC, ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → C ≤ edist x y
[PROOFSTEP]
rw [← einfsep_pos]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : EMetricSpace α
x y z : α
s t : Set α
C : ℝ≥0∞
sC : Set ℝ≥0∞
inst✝ : Finite ↑s
⊢ 0 < einfsep s
[PROOFSTEP]
exact einfsep_pos_of_finite
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
⊢ infsep s = 0 ↔ einfsep s = 0 ∨ einfsep s = ⊤
[PROOFSTEP]
rw [infsep, ENNReal.toReal_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
⊢ 0 < infsep s ↔ 0 < einfsep s ∧ einfsep s < ⊤
[PROOFSTEP]
simp_rw [infsep, ENNReal.toReal_pos_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ infsep s = 0
[PROOFSTEP]
rw [infsep_zero.mpr]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = 0 ∨ Set.einfsep s = ⊤
[PROOFSTEP]
right
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = ⊤
[PROOFSTEP]
exact hs.einfsep
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hs : 0 < infsep s
⊢ Set.Nontrivial s
[PROOFSTEP]
contrapose hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hs : ¬Set.Nontrivial s
⊢ ¬0 < infsep s
[PROOFSTEP]
rw [not_nontrivial_iff] at hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ ¬0 < infsep s
[PROOFSTEP]
exact hs.infsep_zero ▸ lt_irrefl _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hxy : x ≠ y
⊢ infsep {x, y} ≤ ENNReal.toReal (edist x y ⊓ edist y x)
[PROOFSTEP]
simp_rw [infsep, einfsep_pair_eq_inf hxy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : EDist α
x y : α
s : Set α
hxy : x ≠ y
⊢ ENNReal.toReal (edist x y ⊓ edist y x) ≤ ENNReal.toReal (edist x y ⊓ edist y x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infsep {x, y} = ENNReal.toReal (edist x y)
[PROOFSTEP]
by_cases hxy : x = y
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : x = y
⊢ infsep {x, y} = ENNReal.toReal (edist x y)
[PROOFSTEP]
rw [hxy]
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : x = y
⊢ infsep {y, y} = ENNReal.toReal (edist y y)
[PROOFSTEP]
simp only [infsep_singleton, pair_eq_singleton, edist_self, ENNReal.zero_toReal]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
hxy : ¬x = y
⊢ infsep {x, y} = ENNReal.toReal (edist x y)
[PROOFSTEP]
rw [infsep, einfsep_pair hxy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ d ≤ infsep s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ dist x y
[PROOFSTEP]
simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
  ENNReal.ofReal_le_ofReal_iff dist_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ infsep s < d ↔ ∃ x x_1 y x_2 _hxy, dist x y < d
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ ¬infsep s < d ↔ ¬∃ x x_1 y x_2 _hxy, dist x y < d
[PROOFSTEP]
push_neg
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ d ≤ infsep s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ dist x y
[PROOFSTEP]
exact hs.le_infsep_iff
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
by_cases hs : s.Nontrivial
[GOAL]
case pos
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact hs.le_infsep_iff.1 hd x hx y hy hxy
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [not_nontrivial_iff] at hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [hs.infsep_zero] at hd
[GOAL]
case neg
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact le_trans hd dist_nonneg
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
⊢ infsep {x, y} = dist x y
[PROOFSTEP]
rw [infsep_pair_eq_toReal, edist_dist]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
⊢ ENNReal.toReal (ENNReal.ofReal (dist x y)) = dist x y
[PROOFSTEP]
exact ENNReal.toReal_ofReal dist_nonneg
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ infsep {x, y, z} = dist x y ⊓ dist x z ⊓ dist y z
[PROOFSTEP]
simp only [infsep, einfsep_triple hxy hyz hxz, ENNReal.toReal_inf, edist_ne_top x y, edist_ne_top x z, edist_ne_top y z,
  dist_edist, Ne.def, inf_eq_top_iff, and_self_iff, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
⊢ infsep s = if Set.Nontrivial s then ⨅ (d : ↑(offDiag s)), uncurry dist ↑d else 0
[PROOFSTEP]
split_ifs with hs
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
[PROOFSTEP]
have hb : BddBelow (uncurry dist '' s.offDiag) :=
  by
  refine' ⟨0, fun d h => _⟩
  simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
  rcases h with ⟨_, _, _, rfl⟩
  exact dist_nonneg
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
⊢ BddBelow (uncurry dist '' offDiag s)
[PROOFSTEP]
refine' ⟨0, fun d h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
d : ℝ
h : d ∈ uncurry dist '' offDiag s
⊢ 0 ≤ d
[PROOFSTEP]
simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
d : ℝ
h : ∃ a b, (a, b) ∈ offDiag s ∧ dist a b = d
⊢ 0 ≤ d
[PROOFSTEP]
rcases h with ⟨_, _, _, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
w✝¹ w✝ : α
left✝ : (w✝¹, w✝) ∈ offDiag s
⊢ 0 ≤ dist w✝¹ w✝
[PROOFSTEP]
exact dist_nonneg
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
hb : BddBelow (uncurry dist '' offDiag s)
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
[PROOFSTEP]
refine' eq_of_forall_le_iff fun _ => _
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : Set.Nontrivial s
hb : BddBelow (uncurry dist '' offDiag s)
x✝ : ℝ
⊢ x✝ ≤ infsep s ↔ x✝ ≤ ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
[PROOFSTEP]
simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff, mem_offDiag, Prod.forall,
  uncurry_apply_pair, and_imp]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hs : ¬Set.Nontrivial s
⊢ infsep s = 0
[PROOFSTEP]
exact (not_nontrivial_iff.mp hs).infsep_zero
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hs : Set.Nontrivial s
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
[PROOFSTEP]
classical rw [Set.infsep_eq_iInf, if_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hs : Set.Nontrivial s
⊢ infsep s = ⨅ (d : ↑(offDiag s)), uncurry dist ↑d
[PROOFSTEP]
rw [Set.infsep_eq_iInf, if_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ Finset.Nonempty (toFinset (offDiag s))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ infsep s =
    if hs : Set.Nontrivial s then
      Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
    else 0
[PROOFSTEP]
split_ifs with hs
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ infsep s = Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
[PROOFSTEP]
refine' eq_of_forall_le_iff fun _ => _
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
x✝ : ℝ
⊢ x✝ ≤ infsep s ↔ x✝ ≤ Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
[PROOFSTEP]
simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag, Prod.forall,
  uncurry_apply_pair, and_imp]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : ¬Set.Nontrivial s
⊢ infsep s = 0
[PROOFSTEP]
rw [not_nontrivial_iff] at hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝² : Decidable (Set.Nontrivial s)
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Subsingleton s
⊢ infsep s = 0
[PROOFSTEP]
exact hs.infsep_zero
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ Finset.Nonempty (toFinset (offDiag s))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ infsep s = Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
[PROOFSTEP]
classical rw [Set.infsep_of_fintype, dif_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
hs : Set.Nontrivial s
⊢ infsep s = Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist)
[PROOFSTEP]
rw [Set.infsep_of_fintype, dif_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hsf : Set.Finite s
hs : Set.Nontrivial s
⊢ Finset.Nonempty (Finite.toFinset (_ : Set.Finite (offDiag s)))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hsf : Set.Finite s
⊢ Set.infsep s =
    if hs : Set.Nontrivial s then
      Finset.inf' (Finite.toFinset (_ : Set.Finite (offDiag s)))
        (_ : Finset.Nonempty (Finite.toFinset (_ : Set.Finite (offDiag s)))) (uncurry dist)
    else 0
[PROOFSTEP]
split_ifs with hs
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hsf : Set.Finite s
hs : Set.Nontrivial s
⊢ Set.infsep s =
    Finset.inf' (Finite.toFinset (_ : Set.Finite (offDiag s)))
      (_ : Finset.Nonempty (Finite.toFinset (_ : Set.Finite (offDiag s)))) (uncurry dist)
[PROOFSTEP]
refine' eq_of_forall_le_iff fun _ => _
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hsf : Set.Finite s
hs : Set.Nontrivial s
x✝ : ℝ
⊢ x✝ ≤ Set.infsep s ↔
    x✝ ≤
      Finset.inf' (Finite.toFinset (_ : Set.Finite (offDiag s)))
        (_ : Finset.Nonempty (Finite.toFinset (_ : Set.Finite (offDiag s)))) (uncurry dist)
[PROOFSTEP]
simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset, mem_offDiag, Prod.forall,
  uncurry_apply_pair, and_imp]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hsf : Set.Finite s
hs : ¬Set.Nontrivial s
⊢ Set.infsep s = 0
[PROOFSTEP]
rw [not_nontrivial_iff] at hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable (Set.Nontrivial s)
hsf : Set.Finite s
hs : Set.Subsingleton s
⊢ Set.infsep s = 0
[PROOFSTEP]
exact hs.infsep_zero
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hsf : Set.Finite s
hs : Set.Nontrivial s
⊢ Finset.Nonempty (Finite.toFinset (_ : Set.Finite (offDiag s)))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hsf : Set.Finite s
hs : Set.Nontrivial s
⊢ Set.infsep s =
    Finset.inf' (Finite.toFinset (_ : Set.Finite (offDiag s)))
      (_ : Finset.Nonempty (Finite.toFinset (_ : Set.Finite (offDiag s)))) (uncurry dist)
[PROOFSTEP]
classical simp_rw [hsf.infsep, dif_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hsf : Set.Finite s
hs : Set.Nontrivial s
⊢ Set.infsep s =
    Finset.inf' (Finite.toFinset (_ : Set.Finite (offDiag s)))
      (_ : Finset.Nonempty (Finite.toFinset (_ : Set.Finite (offDiag s)))) (uncurry dist)
[PROOFSTEP]
simp_rw [hsf.infsep, dif_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
⊢ infsep ↑s = if hs : Finset.Nonempty (Finset.offDiag s) then Finset.inf' (Finset.offDiag s) hs (uncurry dist) else 0
[PROOFSTEP]
have H : (s : Set α).Nontrivial ↔ s.offDiag.Nonempty := by
  rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
[PROOFSTEP]
rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = if hs : Finset.Nonempty (Finset.offDiag s) then Finset.inf' (Finset.offDiag s) hs (uncurry dist) else 0
[PROOFSTEP]
split_ifs with hs
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
hs : Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = Finset.inf' (Finset.offDiag s) hs (uncurry dist)
[PROOFSTEP]
simp_rw [(H.mpr hs).infsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
H : Set.Nontrivial ↑s ↔ Finset.Nonempty (Finset.offDiag s)
hs : ¬Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = 0
[PROOFSTEP]
exact (not_nontrivial_iff.mp (H.mp.mt hs)).infsep_zero
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
hs : Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = Finset.inf' (Finset.offDiag s) hs (uncurry dist)
[PROOFSTEP]
rw [Finset.coe_infsep, dif_pos hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
hs : Finset.offDiag s = ∅
⊢ infsep ↑s = 0
[PROOFSTEP]
rw [← Finset.not_nonempty_iff_eq_empty] at hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
hs : ¬Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = 0
[PROOFSTEP]
rw [Finset.coe_infsep, dif_neg hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
⊢ ∃ x x_1 y x_2 _hxy, infsep s = dist x y
[PROOFSTEP]
classical
cases nonempty_fintype s
simp_rw [hs.infsep_of_fintype]
rcases@Finset.exists_mem_eq_inf' _ _ _ s.offDiag.toFinset (by simpa) (uncurry dist) with ⟨w, hxy, hed⟩
simp_rw [mem_toFinset] at hxy
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
⊢ ∃ x x_1 y x_2 _hxy, infsep s = dist x y
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x x_1 y x_2 _hxy, infsep s = dist x y
[PROOFSTEP]
simp_rw [hs.infsep_of_fintype]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
[PROOFSTEP]
rcases@Finset.exists_mem_eq_inf' _ _ _ s.offDiag.toFinset (by simpa) (uncurry dist) with ⟨w, hxy, hed⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
⊢ Finset.Nonempty (toFinset (offDiag s))
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ toFinset (offDiag s)
hed : Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = uncurry dist w
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
[PROOFSTEP]
simp_rw [mem_toFinset] at hxy
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Finite ↑s
hs : Set.Nontrivial s
val✝ : Fintype ↑s
w : α × α
hed : Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = uncurry dist w
hxy : w ∈ offDiag s
⊢ ∃ x h y h h, Finset.inf' (toFinset (offDiag s)) (_ : Finset.Nonempty (toFinset (offDiag s))) (uncurry dist) = dist x y
[PROOFSTEP]
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ infsep s = 0 ↔ Set.Subsingleton s
[PROOFSTEP]
rw [infsep_zero, einfsep_eq_top_iff, or_iff_right_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ einfsep s = 0 → Set.Subsingleton s
[PROOFSTEP]
exact fun H => (einfsep_pos_of_finite.ne' H).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < infsep s ↔ Set.Nontrivial s
[PROOFSTEP]
rw [infsep_pos, einfsep_lt_top_iff, and_iff_right_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ Set.Nontrivial s → 0 < einfsep s
[PROOFSTEP]
exact fun _ => einfsep_pos_of_finite