-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem _root_.IsCompact.cthickening_eq_biUnion_closedBall {α : Type*} [PseudoMetricSpace α]
    {δ : ℝ} {E : Set α} (hE : IsCompact E) (hδ : 0 ≤ δ) :
    cthickening δ E = ⋃ x ∈ E, closedBall x δ

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
rcases eq_empty_or_nonempty E with (rfl | hne)

Result:
case inl
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
hδ : 0 ≤ δ
hE : IsCompact ∅
⊢ cthickening δ ∅ = ⋃ x ∈ ∅, closedBall x δ

case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Proof state:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
⊢ x ∈ ⋃ x ∈ E, closedBall x δ

Tactic:
obtain ⟨y, yE, hy⟩ : ∃ y ∈ E, infEdist x E = edist x y := hE.exists_infEdist_eq_edist hne _

Result:
case inr.intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
⊢ x ∈ ⋃ x ∈ E, closedBall x δ

Proof state:
case inl
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
hδ : 0 ≤ δ
hE : IsCompact ∅
⊢ cthickening δ ∅ = ⋃ x ∈ ∅, closedBall x δ

Tactic:
simp only [cthickening_empty, biUnion_empty]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
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 ≤ δ

Tactic:
rw [edist_dist] at D1

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
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 ≤ δ

Proof state:
case inr.intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ ⋃ x ∈ E, closedBall x δ

Tactic:
have D2 : dist x y ≤ δ := by
  rw [edist_dist] at D1
  exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1

Result:
case inr.intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
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 ∈ E, closedBall x δ

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
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 ≤ δ

Tactic:
exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
⊢ x ∈ ⋃ x ∈ E, closedBall x δ

Tactic:
have D1 : edist x y ≤ ENNReal.ofReal δ := (le_of_eq hy.symm).trans hx

Result:
case inr.intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEdist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ ⋃ x ∈ E, closedBall x δ

Proof state:
case inr.intro.intro
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
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 ∈ E, closedBall x δ

Tactic:
exact mem_biUnion yE D2

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
refine Subset.antisymm (fun x hx ↦ ?_)
  (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)

Result:
case inr
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
⊢ x ∈ ⋃ x ∈ E, closedBall x δ