case inl
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
hδ : 0 ≤ δ
hE : IsCompact ∅
⊢ cthickening δ ∅ = ⋃ (x : α) (_ : x ∈ ∅), closedBall x δ

case inr
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ E), closedBall x δ
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ E), closedBall x δ
rcases eq_empty_or_nonempty E with (rfl | hne)
case inr
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
case inr
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ E), closedBall x δ
refine Subset.antisymm (fun x hx ↦ ?_)
  (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
case inr.intro.intro
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
case inr
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
obtain ⟨y, yE, hy⟩ : ∃ y ∈ E, infEdist x E = edist x y := hE.exists_infEdist_eq_edist hne _
case inr.intro.intro
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
case inr.intro.intro
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
have D1 : edist x y ≤ ENNReal.ofReal δ := (le_of_eq hy.symm).trans hx
case inr.intro.intro
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
D2 : dist x y ≤ δ
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
case inr.intro.intro
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
have D2 : dist x y ≤ δ := by
  rw [edist_dist] at D1
  exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1
no goals
case inr.intro.intro
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
D2 : dist x y ≤ δ
⊢ x ∈ ⋃ (x : α) (_ : x ∈ E), closedBall x δ
exact mem_biUnion yE D2
no goals
case inl
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
hδ : 0 ≤ δ
hE : IsCompact ∅
⊢ cthickening δ ∅ = ⋃ (x : α) (_ : x ∈ ∅), closedBall x δ
simp only [cthickening_empty, biUnion_empty]
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ
rw [edist_dist] at D1
no goals
ι : Sort ?u.147332
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ✝ ε : ℝ
s t : Set α✝
x✝ : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : Set.Nonempty E
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ
exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1