case inl
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
⊢ ∃ r', r' < r ∧ s ⊆ ball x r'

case inr
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : 0 < r
⊢ ∃ r', r' < r ∧ s ⊆ ball x r'
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r', r' < r ∧ s ⊆ ball x r'
cases' le_or_lt r 0 with hr hr
case inl
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
⊢ ∃ r', r' < r ∧ s ⊆ ball x r'
case inl
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
⊢ ∃ r', r' < r ∧ s ⊆ ball x r'
rw [ball_eq_empty.2 hr, subset_empty_iff] at h
case inl
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : r ≤ 0
hs : IsClosed ∅
⊢ ∃ r', r' < r ∧ ∅ ⊆ ball x r'
case inl
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
⊢ ∃ r', r' < r ∧ s ⊆ ball x r'
subst s
no goals
case inl
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : r ≤ 0
hs : IsClosed ∅
⊢ ∃ r', r' < r ∧ ∅ ⊆ ball x r'
exact (exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩
no goals
case inr
α : Type u
β : Type v
X : Type ?u.438072
ι : Type ?u.438075
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : 0 < r
⊢ ∃ r', r' < r ∧ s ⊆ ball x r'
exact (exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩