-- Mathlib/Topology/MetricSpace/Closeds.lean
theorem NonemptyCompacts.isClosed_in_closeds [CompleteSpace α] :
    IsClosed (range <| @NonemptyCompacts.toCloseds α _ _)

Proof state:
case refine_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist t s < ⊤
⊢ (↑s).Nonempty

Tactic:
exact nonempty_of_hausdorffEdist_ne_top ht.1 (ne_of_lt Dst)

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist s t < ⊤
⊢ (↑s).Nonempty

Tactic:
rw [edist_comm] at Dst

Result:
case refine_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist t s < ⊤
⊢ (↑s).Nonempty

Proof state:
case h
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds ↔ s ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}

Tactic:
refine ⟨?_, fun h => ⟨⟨⟨s, h.2⟩, h.1⟩, Closeds.ext rfl⟩⟩

Result:
case h
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds → s ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}

Proof state:
case h
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds → s ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}

Tactic:
rintro ⟨s, hs, rfl⟩

Result:
case h.intro.refl
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
s : NonemptyCompacts α
⊢ s.toCloseds ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}

Proof state:
case refine_2
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
⊢ IsCompact ↑s

Tactic:
refine isCompact_iff_totallyBounded_isComplete.2 ⟨?_, s.closed.isComplete⟩

Result:
case refine_2
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
⊢ TotallyBounded ↑s

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : u.Finite
ut : ↑t ⊆ ⋃ y ∈ u, ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
⊢ x ∈ ⋃ y ∈ u, ball y ε

Tactic:
have : edist x y < ε :=
  calc
    edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
    _ < ε / 2 + ε / 2 := ENNReal.add_lt_add Dxz Dzy
    _ = ε := ENNReal.add_halves _

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this✝ : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : u.Finite
ut : ↑t ⊆ ⋃ y ∈ u, ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
this : edist x y < ε
⊢ x ∈ ⋃ y ∈ u, ball y ε

Proof state:
case refine_1
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
⊢ (↑s).Nonempty

Tactic:
rcases mem_closure_iff.1 hs ⊤ ENNReal.coe_lt_top with ⟨t, ht, Dst⟩

Result:
case refine_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist s t < ⊤
⊢ (↑s).Nonempty

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this✝ : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : u.Finite
ut : ↑t ⊆ ⋃ y ∈ u, ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
this : edist x y < ε
⊢ x ∈ ⋃ y ∈ u, ball y ε

Tactic:
exact mem_biUnion hy this

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : u.Finite
ut : ↑t ⊆ ⋃ y ∈ u, ball y (ε / 2)
x : α
hx : x ∈ ↑s
⊢ x ∈ ⋃ y ∈ u, ball y ε

Tactic:
rcases exists_edist_lt_of_hausdorffEdist_lt hx Dst with ⟨z, hz, Dxz⟩

Result:
case refine_2.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | (↑s).Nonempty ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : u.Finite
ut : ↑t ⊆ ⋃ y ∈ u, ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
⊢ x ∈ ⋃ y ∈ u, ball y ε

Proof state:
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
⊢ IsClosed (range NonemptyCompacts.toCloseds)

Tactic:
have :
  range NonemptyCompacts.toCloseds =
    { s : Closeds α | (s : Set α).Nonempty ∧ IsCompact (s : Set α) } := by
  ext s
  refine ⟨?_, fun h => ⟨⟨⟨s, h.2⟩, h.1⟩, Closeds.ext rfl⟩⟩
  rintro ⟨s, hs, rfl⟩
  exact ⟨s.nonempty, s.isCompact⟩

Result:
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
⊢ IsClosed (range NonemptyCompacts.toCloseds)

Proof state:
case refine_2
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
⊢ TotallyBounded ↑s

Tactic:
refine totallyBounded_iff.2 fun ε (εpos : 0 < ε) => ?_

Result:
case refine_2
α : Type u
inst✝¹ : EMetricSpace α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t, t.Finite ∧ ↑s ⊆ ⋃ y ∈ t, ball y ε