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

Proof state:
case inr
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ (closure E) = ⋃ x ∈ closure 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 α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure E)
⊢ x ∈ ⋃ x ∈ closure E, closedBall x δ

Proof state:
case inr.intro.intro
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure E)
y : α
yE : y ∈ closure E
hy : infDist x (closure E) = dist x y
⊢ x ∈ ⋃ x ∈ closure E, closedBall x δ

Tactic:
replace hy : dist x y ≤ δ :=
  (ENNReal.ofReal_le_ofReal_iff hδ).mp
    (((congr_arg ENNReal.ofReal hy.symm).le.trans ENNReal.ofReal_toReal_le).trans hx)

Result:
case inr.intro.intro
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure E)
y : α
yE : y ∈ closure E
hy : dist x y ≤ δ
⊢ x ∈ ⋃ x ∈ closure E, closedBall x δ

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

Tactic:
obtain ⟨y, yE, hy⟩ : ∃ y ∈ closure E, infDist x (closure E) = dist x y :=
  isClosed_closure.exists_infDist_eq_dist (closure_nonempty_iff.mpr hne) x

Result:
case inr.intro.intro
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure E)
y : α
yE : y ∈ closure E
hy : infDist x (closure E) = dist x y
⊢ x ∈ ⋃ x ∈ closure E, closedBall x δ

Proof state:
case inr.intro.intro
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure E)
y : α
yE : y ∈ closure E
hy : dist x y ≤ δ
⊢ x ∈ ⋃ x ∈ closure E, closedBall x δ

Tactic:
exact mem_biUnion yE hy

Result:
no goals

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

Tactic:
rw [← cthickening_closure]

Result:
case inr
δ : ℝ
α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ (closure E) = ⋃ x ∈ closure E, closedBall x δ

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

Tactic:
simp only [cthickening_empty, biUnion_empty, closure_empty]

Result:
no goals

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

Tactic:
rcases eq_empty_or_nonempty E with (rfl | hne)

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

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