-- Mathlib/Topology/ShrinkingLemma.lean
theorem exists_subset_iUnion_closure_subset (hs : IsClosed s) (uo : ∀ i, IsOpen (u i))
    (uf : ∀ x ∈ s, { i | x ∈ u i }.Finite) (us : s ⊆ ⋃ i, u i) :
    ∃ v : ι → Set X, s ⊆ iUnion v ∧ (∀ i, IsOpen (v i)) ∧ ∀ i, closure (v i) ⊆ u i

Proof state:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
rcases zorn_le_nonempty this with ⟨v, hv⟩

Result:
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Proof state:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
hi : i ∉ v.carrier
v' : PartialRefinement u s ⊤
hlt : v < v'
⊢ False

Tactic:
exact hv.not_lt hlt

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
haveI : Nonempty (PartialRefinement u s ⊤) :=
  ⟨⟨u, ∅, uo, us, False.elim, False.elim, fun _ => rfl⟩⟩

Result:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this : Nonempty (PartialRefinement u s ⊤)
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Proof state:
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
suffices ∀ i, i ∈ v.carrier from
  ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i)⟩

Result:
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier

Proof state:
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier

Tactic:
refine fun i ↦ by_contra fun hi ↦ ?_

Result:
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
hi : i ∉ v.carrier
⊢ False

Proof state:
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
hi : i ∉ v.carrier
⊢ False

Tactic:
rcases v.exists_gt hs i hi with ⟨v', hlt⟩

Result:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
hi : i ∉ v.carrier
v' : PartialRefinement u s ⊤
hlt : v < v'
⊢ False