-- Mathlib/Topology/MetricSpace/ProperSpace/Lemmas.lean
theorem exists_pos_lt_subset_ball (hr : 0 < r) (hs : IsClosed s) (h : s ⊆ ball x r) :
    ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Proof state:
case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
  this.exists_isMaxOn (β := α) (α := ℝ) hne (continuous_id.dist continuous_const).continuousOn

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Proof state:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : 0 < r
hs : IsClosed ∅
h : ∅ ⊆ ball x r
⊢ ∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'

Tactic:
exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
have : IsCompact s :=
  (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall)

Result:
case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
rcases exists_between hyr with ⟨r', hyr', hrr'⟩

Result:
case inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
r' : ℝ
hyr' : dist y x < r'
hrr' : r' < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
r' : ℝ
hyr' : dist y x < r'
hrr' : r' < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hne)

Result:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : 0 < r
hs : IsClosed ∅
h : ∅ ⊆ ball x r
⊢ ∃ r' ∈ Ioo 0 r, ∅ ⊆ ball x r'

case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Proof state:
case inr.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
have hyr : dist y x < r := h hys

Result:
case inr.intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'