case inl
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : 0 < r
hs : IsClosed ∅
h : ∅ ⊆ ball x r
⊢ ∃ r', r' ∈ Ioo 0 r ∧ ∅ ⊆ ball x r'

case inr
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
rcases eq_empty_or_nonempty s with (rfl | hne)
case inr
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
this : IsCompact s
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
case inr
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
have : IsCompact s :=
  isCompact_of_isClosed_subset (isCompact_closedBall x r) hs
    (h.trans ball_subset_closedBall)
case inr.intro.intro
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
case inr
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
this : IsCompact s
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
  this.exists_forall_ge hne (continuous_id.dist continuous_const).continuousOn
case inr.intro.intro
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
case inr.intro.intro
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
have hyr : dist y x < r := h hys
case inr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
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', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
case inr.intro.intro
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
hyr : dist y x < r
⊢ ∃ r', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
rcases exists_between hyr with ⟨r', hyr', hrr'⟩
no goals
case inr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : Set.Nonempty s
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', r' ∈ Ioo 0 r ∧ s ⊆ ball x r'
exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩
no goals
case inl
α : Type u
β : Type v
X : Type ?u.436396
ι : Type ?u.436399
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : 0 < r
hs : IsClosed ∅
h : ∅ ⊆ ball x r
⊢ ∃ r', r' ∈ Ioo 0 r ∧ ∅ ⊆ ball x r'
exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩