α : Type u_1
β : Type ?u.44124
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
⊢ (⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y) ⊓ einfsep s ≤ einfsep (insert x s)
α : Type u_1
β : Type ?u.44124
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
⊢ einfsep (insert x s) = (⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y) ⊓ einfsep s
refine' le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) _
α : Type u_1
β : Type ?u.44124
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
α : Type u_1
β : Type ?u.44124
inst✝ : PseudoEMetricSpace α
x y z : α
s t : Set α
⊢ (⨅ (y : α) (_ : y ∈ s) (_ : x ≠ y), edist x y) ⊓ einfsep s ≤ einfsep (insert x s)
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff]
case inl.inl
α : Type u_1
β : Type ?u.44124
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

case inl.inr
α : Type u_1
β : Type ?u.44124
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

case inr.inl
α : Type u_1
β : Type ?u.44124
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

case inr.inr
α : Type u_1
β : Type ?u.44124
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
α : Type u_1
β : Type ?u.44124
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
rintro y (rfl | hy) z (rfl | hz) hyz
no goals
case inl.inl
α : Type u_1
β : Type ?u.44124
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
exact False.elim (hyz rfl)
no goals
case inl.inr
α : Type u_1
β : Type ?u.44124
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
exact Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))
case inr.inl
α : Type u_1
β : Type ?u.44124
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
case inr.inl
α : Type u_1
β : Type ?u.44124
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
rw [edist_comm]
no goals
case inr.inl
α : Type u_1
β : Type ?u.44124
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
exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))
no goals
case inr.inr
α : Type u_1
β : Type ?u.44124
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
exact Or.inr (einfsep_le_edist_of_mem hy hz hyz)