-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem _root_.IsClosed.exists_infDist_eq_dist [ProperSpace α] (h : IsClosed s) (hne : s.Nonempty)
    (x : α) : ∃ y ∈ s, infDist x s = dist x y

Proof state:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
⊢ ∃ y ∈ s, infDist x t = dist x y

Tactic:
obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x

Result:
case intro.intro.intro.intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
y : α
hyd : infDist x t = dist x y
hys : y ∈ s
⊢ ∃ y ∈ s, infDist x t = dist x y

Proof state:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y ∈ s, infDist x s = dist x y

Tactic:
rw [← infDist_inter_closedBall_of_mem hz]

Result:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y ∈ s, infDist x (s ∩ closedBall x (dist z x)) = dist x y

Proof state:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
⊢ ∃ y ∈ s, infDist x t = dist x y

Tactic:
have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩

Result:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
⊢ ∃ y ∈ s, infDist x t = dist x y

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infDist x s = dist x y

Tactic:
rcases hne with ⟨z, hz⟩

Result:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y ∈ s, infDist x s = dist x y

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
htne : t.Nonempty
y : α
hyd : infDist x t = dist x y
hys : y ∈ s
⊢ ∃ y ∈ s, infDist x t = dist x y

Tactic:
exact ⟨y, hys, hyd⟩

Result:
no goals

Proof state:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
⊢ ∃ y ∈ s, infDist x t = dist x y

Tactic:
have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h

Result:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
htc : IsCompact t
⊢ ∃ y ∈ s, infDist x t = dist x y

Proof state:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
⊢ ∃ y ∈ s, infDist x (s ∩ closedBall x (dist z x)) = dist x y

Tactic:
set t := s ∩ closedBall x (dist z x)

Result:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
h : IsClosed s
x z : α
hz : z ∈ s
t : Set α := s ∩ closedBall x (dist z x)
⊢ ∃ y ∈ s, infDist x t = dist x y