-- Mathlib/Topology/ShrinkingLemma.lean
theorem exists_subset_iUnion_closure_subset_t2space (hs : IsCompact 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)
      ∧ (∀ i, IsCompact (closure (v i)))

Proof state:
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w => IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w => IsCompact (closure w))),
    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) ∧ ∀ (i : ι), IsCompact (closure (v 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✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w => IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w => IsCompact (closure w))),
    IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w => IsCompact (closure w)
hv : IsMax v
⊢ ∃ v,
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))

Proof state:
case intro.refine_1.intro.intro
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s fun w => IsCompact (closure w))
this :
  ∀ (c : Set (PartialRefinement u s fun w => IsCompact (closure w))),
    IsChain (fun x1 x2 => x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s fun w => IsCompact (closure w)
hv : IsMax v
i : ι
hi : i ∉ v.carrier
v' : PartialRefinement u s fun w => IsCompact (closure w)
hlt : v < v'
right✝ : IsCompact (closure (v'.toFun i))
⊢ 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✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact 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) ∧ ∀ (i : ι), IsCompact (closure (v i))

Tactic:
haveI : Nonempty (PartialRefinement u s (fun w => IsCompact (closure w))) :=
  ⟨⟨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✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this : Nonempty (PartialRefinement u s fun w => IsCompact (closure w))
⊢ ∃ v,
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))

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

Tactic:
intro i

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

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

Tactic:
intro i

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

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

Tactic:
rcases exists_gt_t2space v hs i hi with ⟨v', hlt, _⟩

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