case intro.intro
ι : Sort ?u.135640
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
ι : Sort ?u.135640
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht
no goals
case intro.intro
ι : Sort ?u.135640
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
refine' ⟨δ / 2, half_pos hδ, h.mono _ _⟩ <;>
  exact cthickening_subset_thickening' hδ (half_lt_self hδ) _