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

Proof state:
case refine_2.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
⊢ ∃ t, t.Finite ∧ ↑s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
rcases totallyBounded_iff.1 (isCompact_iff_totallyBounded_isComplete.1 ht.2).1 (ε / 2)
    (ENNReal.half_pos εpos.ne') with
  ⟨u, fu, ut⟩

Result:
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)
⊢ ∃ t, t.Finite ∧ ↑s ⊆ ⋃ y ∈ t, ball y ε

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

Tactic:
refine isClosed_of_closure_subset fun s hs => ⟨?_, ?_⟩

Result:
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

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

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

Tactic:
ext s

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

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

Tactic:
rw [this]

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

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)
⊢ ∃ t, t.Finite ∧ ↑s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
refine ⟨u, ⟨fu, fun x hx => ?_⟩⟩

Result:
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 ε

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}
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t, t.Finite ∧ ↑s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
rcases mem_closure_iff.1 hs (ε / 2) (ENNReal.half_pos εpos.ne') with ⟨t, ht, Dst⟩

Result:
case refine_2.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
⊢ ∃ t, t.Finite ∧ ↑s ⊆ ⋃ y ∈ t, ball y ε

Proof state:
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 ε

Tactic:
rcases mem_iUnion₂.1 (ut hz) with ⟨y, hy, Dzy⟩

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)
⊢ x ∈ ⋃ y ∈ u, ball y ε

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

Tactic:
exact ⟨s.nonempty, s.isCompact⟩

Result:
no goals