-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)
I : s ∩ ⋂ (j : ι), ⋂ (_ : j ≠ i), (v.toFun (u := u) (s := s) (p := ⊤) j)ᶜ ⊆ v.toFun (u := u) (s := s) (p := ⊤) i
C : IsClosed (s ∩ ⋂ (j : ι), ⋂ (_ : j ≠ i), (v.toFun (u := u) (s := s) (p := ⊤) j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι), ⋂ (_ : j ≠ i), (v.toFun (u := u) (s := s) (p := ⊤) j)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun (u := u) (s := s) (p := ⊤) i
refine_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_2 : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
refine_3 :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1) ⊆ u i_1
refine_4 :
  ∀ {i_1 : ι} (hi : i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤))),
    ⊤ (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_5 :
  ∀ {i_1 : ι},
    i_1 ∉ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1 = u i_1
refine_6 :
  (fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
      v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
          v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
    v
    (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
      (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
refine_7 :
  ¬(fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
        v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
            v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
      (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
        (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v
refine_2₁ : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
refine_3₁ :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1) ⊆ u i_1
refine_4₁ :
  ∀ {i_1 : ι} (hi : i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤))),
    ⊤ (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_5₁ :
  ∀ {i_1 : ι},
    i_1 ∉ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1 = u i_1
refine_6₁ :
  (fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
      v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
          v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
    v
    (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
      (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
refine_7₁ :
  ¬(fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
        v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
            v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
      (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
        (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v
refine_3₂ :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1) ⊆ u i_1
refine_4₂ :
  ∀ {i_1 : ι} (hi : i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤))),
    ⊤ (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_5₂ :
  ∀ {i_1 : ι},
    i_1 ∉ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1 = u i_1
refine_6₂ :
  (fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
      v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
          v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
    v
    (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
      (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
refine_7₂ :
  ¬(fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
        v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
            v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
      (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
        (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v
refine_4₃ :
  ∀ {i_1 : ι} (hi : i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤))),
    ⊤ (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_5₃ :
  ∀ {i_1 : ι},
    i_1 ∉ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1 = u i_1
refine_6₃ :
  (fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
      v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
          v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
    v
    (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
      (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
refine_7₃ :
  ¬(fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
        v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
            v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
      (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
        (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v
refine_5₄ :
  ∀ {i_1 : ι},
    i_1 ∉ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1 = u i_1
refine_6₄ :
  (fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
      v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
          v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
    v
    (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
      (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
refine_7₄ :
  ¬(fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
        v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
            v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
      (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
        (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v
refine_6₅ :
  (fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
      v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
          v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
    v
    (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
      (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
refine_7₅ refine_7₆ :
  ¬(fun (v₁ v₂ : PartialRefinement u s ⊤) ↦
        v₁.carrier (u := u) (s := s) (p := ⊤) ⊆ v₂.carrier (u := u) (s := s) (p := ⊤) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := ⊤),
            v₁.toFun (u := u) (s := s) (p := ⊤) i = v₂.toFun (u := u) (s := s) (p := ⊤) i)
      (mk (u := u) (s := s) (p := ⊤) (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi)
        (insert i (v.carrier (u := u) (s := s) (p := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'

Tactic:
classical
  refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ?_, ?_⟩
  · intro j
    rcases eq_or_ne j i with (rfl | hne) <;> simp [*, v.isOpen]
  · refine fun x hx => mem_iUnion.2 ?_
    by_cases! h : ∃ j ≠ i, x ∈ v j
    · rcases h with ⟨j, hji, hj⟩
      use j
      rwa [update_of_ne hji]
    · use i
      rw [update_self]
      exact hvi ⟨hx, mem_biInter h⟩
  · rintro j (rfl | hj)
    · rwa [update_self, ← v.apply_eq hi]
    · rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
      exact v.closure_subset hj
  · exact fun _ => trivial
  · intro j hj
    rw [mem_insert_iff, not_or] at hj
    rw [update_of_ne hj.1, v.apply_eq hj.2]
  · refine ⟨subset_insert _ _, fun j hj => ?_⟩
    exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm
  · exact fun hle => hi (hle.1 <| mem_insert _ _)

Premises used: Iff.mpr, trivial, Set.mem_iUnion, ShrinkingLemma.PartialRefinement.apply_eq, not_or, Set.mem_insert_iff, ShrinkingLemma.PartialRefinement.isOpen, Function.update_self, rfl