-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_insert : einfsep (insert x s) =
    (⨅ (y ∈ s) (_ : x ≠ y), edist x y) ⊓ s.einfsep

Proof state:
case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
rw [edist_comm]

Result:
case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y

Proof state:
case inl.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y_1 ∈ s, ⨅ (_ : y ≠ y_1), edist y y_1 ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
exact Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z y ∨ s.einfsep ≤ edist z y

Tactic:
exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (insert x s).einfsep = (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊓ s.einfsep

Tactic:
refine le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) ?_

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊓ s.einfsep ≤ (insert x s).einfsep

Proof state:
case inr.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
exact Or.inr (einfsep_le_edist_of_mem hy hz hyz)

Result:
no goals

Proof state:
case inl.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
z : α
hyz : z ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z z ∨ s.einfsep ≤ edist z z

Tactic:
exact False.elim (hyz rfl)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊓ s.einfsep ≤ (insert x s).einfsep

Tactic:
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 ∈ s →
      ∀ (y : α), y = x ∨ y ∈ s → x_1 ≠ y → ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ s.einfsep ≤ edist x_1 y

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 ∈ s →
      ∀ (y : α), y = x ∨ y ∈ s → x_1 ≠ y → ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ s.einfsep ≤ edist x_1 y

Tactic:
rintro y (rfl | hy) z (rfl | hz) hyz

Result:
case inl.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
z : α
hyz : z ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist z z ∨ s.einfsep ≤ edist z z

case inl.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y_1 ∈ s, ⨅ (_ : y ≠ y_1), edist y y_1 ≤ edist y z ∨ s.einfsep ≤ edist y z

case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z

case inr.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z