-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_closure : infEdist x (closure s) = infEdist x s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Tactic:
have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
z : α
zs : z ∈ s
dyz : edist y z < ↑ε / 2
⊢ infEdist x (closure s) + ↑ε / 2 + ↑ε / 2 = infEdist x (closure s) + ↑ε

Tactic:
rw [add_assoc, ENNReal.add_halves]

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Tactic:
obtain ⟨z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2⟩ := EMetric.mem_closure_iff.1 ycs (ε / 2) ε0

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
z : α
zs : z ∈ s
dyz : edist y z < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
⊢ 0 < ↑ε / 2

Tactic:
simpa [pos_iff_ne_zero] using εpos

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
z : α
zs : z ∈ s
dyz : edist y z < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Tactic:
calc
  infEdist x s ≤ edist x z := infEdist_le_edist_of_mem zs
  _ ≤ edist x y + edist y z := edist_triangle _ _ _
  _ ≤ infEdist x (closure s) + ε / 2 + ε / 2 := add_le_add (le_of_lt hy) (le_of_lt dyz)
  _ = infEdist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEdist x s ≤ infEdist x (closure s)

Tactic:
refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Tactic:
obtain ⟨y : α, ycs : y ∈ closure s, hy : edist x y < infEdist x (closure s) + ↑ε / 2⟩ :=
  infEdist_lt_iff.mp this

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
y : α
ycs : y ∈ closure s
hy : edist x y < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Tactic:
have : infEdist x (closure s) < infEdist x (closure s) + ε / 2 :=
  ENNReal.lt_add_right h.ne ε0.ne'

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x (closure s) < ⊤
ε0 : 0 < ↑ε / 2
this : infEdist x (closure s) < infEdist x (closure s) + ↑ε / 2
⊢ infEdist x s ≤ infEdist x (closure s) + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEdist x (closure s) = infEdist x s

Tactic:
refine le_antisymm (infEdist_anti subset_closure) ?_

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEdist x s ≤ infEdist x (closure s)