-- Mathlib/Topology/ShrinkingLemma.lean
theorem exists_gt [NormalSpace X] (v : PartialRefinement u s ⊤) (hs : IsClosed s)
    (i : ι) (hi : i ∉ v.carrier) :
    ∃ v' : PartialRefinement u s ⊤, v < v'

Proof state:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
⊢ s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i

Tactic:
simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]

Result:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
⊢ ∀ x ∈ s, (∀ (i_1 : ι), i_1 ≠ i → x ∈ (v.toFun i_1)ᶜ) → x ∈ v.toFun i

Proof state:
case intro.intro.intro.refine_7
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ¬({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯, closure_subset := ⋯,
            pred_of_mem := ⋯, apply_eq := ⋯ }.carrier ⊆
        v.carrier ∧
      ∀
        i_1 ∈
          { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
              closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.carrier,
        { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ⋯, subset_iUnion := ⋯,
                closure_subset := ⋯, pred_of_mem := ⋯, apply_eq := ⋯ }.toFun
            i_1 =
          v.toFun i_1)

Tactic:
exact fun hle => hi (hle.1 <| mem_insert _ _)

Result:
no goals

Proof state:
case intro.intro.intro.refine_3.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
j : ι
hj : j ∈ v.carrier
⊢ closure (v.toFun j) ⊆ u j

Tactic:
exact v.closure_subset hj

Result:
no goals

Proof state:
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ∃ v', v < v'

Tactic:
refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ∀ (i_1 : ι), IsOpen (update v.toFun i vi i_1)

case intro.intro.intro.refine_2
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ s ⊆ ⋃ i_1, update v.toFun i vi i_1

case intro.intro.intro.refine_3
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i v.carrier → closure (update v.toFun i vi i_1) ⊆ u i_1

case intro.intro.intro.refine_4
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i v.carrier → ⊤ (update v.toFun i vi i_1)

case intro.intro.intro.refine_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ∀ {i_1 : ι}, i_1 ∉ insert i v.carrier → update v.toFun i vi i_1 = u i_1

case intro.intro.intro.refine_6
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ v.carrier ⊆
      { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine_1,
          subset_iUnion := ?intro.intro.intro.refine_2, closure_subset := ?intro.intro.intro.refine_3,
          pred_of_mem := ?intro.intro.intro.refine_4, apply_eq := ?intro.intro.intro.refine_5 }.carrier ∧
    ∀ i_1 ∈ v.carrier,
      v.toFun i_1 =
        { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine_1,
              subset_iUnion := ?intro.intro.intro.refine_2, closure_subset := ?intro.intro.intro.refine_3,
              pred_of_mem := ?intro.intro.intro.refine_4, apply_eq := ?intro.intro.intro.refine_5 }.toFun
          i_1

case intro.intro.intro.refine_7
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier
I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i
C : IsClosed (s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun i
⊢ ¬({ toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine_1,
            subset_iUnion := ?intro.intro.intro.refine_2, closure_subset := ?intro.intro.intro.refine_3,
            pred_of_mem := ?intro.intro.intro.refine_4, apply_eq := ?intro.intro.intro.refine_5 }.carrier ⊆
        v.carrier ∧
      ∀
        i_1 ∈
          { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine_1,
              subset_iUnion := ?intro.intro.intro.refine_2, closure_subset := ?intro.intro.intro.refine_3,
              pred_of_mem := ?intro.intro.intro.refine_4, apply_eq := ?intro.intro.intro.refine_5 }.carrier,
        { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine_1,
                subset_iUnion := ?intro.intro.intro.refine_2, closure_subset := ?intro.intro.intro.refine_3,
                pred_of_mem := ?intro.intro.intro.refine_4, apply_eq := ?intro.intro.intro.refine_5 }.toFun
            i_1 =
          v.toFun i_1)