case intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst
case intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ Disjoint (thickening (↑r / 2) s) (thickening (↑r / 2) t)
case intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ ∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
refine' ⟨r / 2, half_pos (NNReal.coe_pos.2 hr), _⟩
case intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ thickening (↑r / 2) s ⊓ thickening (↑r / 2) t ≤ ⊥
case intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ Disjoint (thickening (↑r / 2) s) (thickening (↑r / 2) t)
rw [disjoint_iff_inf_le]
case intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : z ∈ thickening (↑r / 2) s
hzt : z ∈ thickening (↑r / 2) t
⊢ z ∈ ⊥
case intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
⊢ thickening (↑r / 2) s ⊓ thickening (↑r / 2) t ≤ ⊥
rintro z ⟨hzs, hzt⟩
case intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : ∃ z_1, z_1 ∈ s ∧ edist z z_1 < ENNReal.ofReal (↑r / 2)
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ENNReal.ofReal (↑r / 2)
⊢ z ∈ ⊥
case intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : z ∈ thickening (↑r / 2) s
hzt : z ∈ thickening (↑r / 2) t
⊢ z ∈ ⊥
rw [mem_thickening_iff_exists_edist_lt] at hzs hzt
case intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : ∃ z_1, z_1 ∈ s ∧ edist z z_1 < ↑(r / 2)
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ↑(r / 2)
⊢ z ∈ ⊥
case intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : ∃ z_1, z_1 ∈ s ∧ edist z z_1 < ENNReal.ofReal (↑r / 2)
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ENNReal.ofReal (↑r / 2)
⊢ z ∈ ⊥
rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt
case intro.intro.intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ↑(r / 2)
x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
⊢ z ∈ ⊥
case intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzs : ∃ z_1, z_1 ∈ s ∧ edist z z_1 < ↑(r / 2)
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ↑(r / 2)
⊢ z ∈ ⊥
obtain ⟨x, hx, hzx⟩ := hzs
case intro.intro.intro.intro.intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ z ∈ ⊥
case intro.intro.intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z : α
hzt : ∃ z_1, z_1 ∈ t ∧ edist z z_1 < ↑(r / 2)
x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
⊢ z ∈ ⊥
obtain ⟨y, hy, hzy⟩ := hzt
case intro.intro.intro.intro.intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ edist x y ≤ ↑r
case intro.intro.intro.intro.intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ z ∈ ⊥
refine' (h x hx y hy).not_le _
no goals
case intro.intro.intro.intro.intro.intro.intro
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ edist x y ≤ ↑r
calc
  edist x y ≤ edist z x + edist z y := edist_triangle_left _ _ _
  _ ≤ ↑(r / 2) + ↑(r / 2) := (add_le_add hzx.le hzy.le)
  _ = r := by rw [← ENNReal.coe_add, add_halves]
no goals
ι : Sort ?u.131908
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x✝ : α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed t
r : ℝ≥0
hr : 0 < r
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ↑r < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < ↑(r / 2)
y : α
hy : y ∈ t
hzy : edist z y < ↑(r / 2)
⊢ ↑(r / 2) + ↑(r / 2) = ↑r
rw [← ENNReal.coe_add, add_halves]