-- Mathlib/Topology/MetricSpace/Closeds.lean
theorem isClosed_subsets_of_isClosed (hs : IsClosed s) :
    IsClosed { t : Closeds α | (t : Set α) ⊆ s }

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
y : α
hy : y ∈ u
Dxy : edist x y < ε
⊢ ∃ y ∈ s, edist x y < ε

Tactic:
exact ⟨y, hu hy, Dxy⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
⊢ IsClosed {t | ↑t ⊆ s}

Tactic:
refine isClosed_of_closure_subset fun
  (t : Closeds α) (ht : t ∈ closure {t : Closeds α | (t : Set α) ⊆ s}) (x : α) (hx : x ∈ t) => ?_

Result:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
⊢ x ∈ s

Proof state:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
this : x ∈ closure s
⊢ x ∈ s

Tactic:
rwa [hs.closure_eq] at this

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
⊢ ∃ y ∈ s, edist x y < ε

Tactic:
obtain ⟨y : α, hy : y ∈ u, Dxy : edist x y < ε⟩ := exists_edist_lt_of_hausdorffEdist_lt hx Dtu

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
y : α
hy : y ∈ u
Dxy : edist x y < ε
⊢ ∃ y ∈ s, edist x y < ε

Proof state:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y ∈ s, edist x y < ε

Tactic:
obtain ⟨u : Closeds α, hu : u ∈ {t : Closeds α | (t : Set α) ⊆ s}, Dtu : edist t u < ε⟩ :=
  mem_closure_iff.1 ht ε εpos

Result:
case intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
⊢ ∃ y ∈ s, edist x y < ε

Proof state:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
⊢ x ∈ s

Tactic:
have : x ∈ closure s := by
  refine mem_closure_iff.2 fun ε εpos => ?_
  obtain ⟨u : Closeds α, hu : u ∈ {t : Closeds α | (t : Set α) ⊆ s}, Dtu : edist t u < ε⟩ :=
    mem_closure_iff.1 ht ε εpos
  obtain ⟨y : α, hy : y ∈ u, Dxy : edist x y < ε⟩ := exists_edist_lt_of_hausdorffEdist_lt hx Dtu
  exact ⟨y, hu hy, Dxy⟩

Result:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
this : x ∈ closure s
⊢ x ∈ s

Proof state:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
⊢ x ∈ closure s

Tactic:
refine mem_closure_iff.2 fun ε εpos => ?_

Result:
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ t
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y ∈ s, edist x y < ε