awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
h : ¬j = i
hji : j = i
⊢ IsCompact
    (closure
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        j))

Tactic:
exact False.elim (h hji)

Premises used: False.elim
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
h : ¬j = i
hjmemv : j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
neg : IsCompact (closure (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j))
⊢ IsCompact
    (closure
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        j))

Tactic:
rw [update_of_ne h]

Premises used: Function.update_of_ne
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
h : ¬j = i
hjmemv : j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
⊢ IsCompact (closure (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j))

Tactic:
v.pred_of_mem hjmemv

Premises used: ShrinkingLemma.PartialRefinement.pred_of_mem
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
h : ¬j = i
hjmemv : j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
⊢ IsCompact (closure (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j))

Tactic:
exact v.pred_of_mem hjmemv

Premises used: ShrinkingLemma.PartialRefinement.pred_of_mem
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : j ∉ insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))
⊢ ¬j = i ∧ j ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))

Tactic:
rw [mem_insert_iff, not_or] at hj

Premises used: not_or, Set.mem_insert_iff
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : ¬j = i ∧ j ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
refine_5 : v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j = u j
refine_5₁ refine_5₂ : u j = u j
⊢ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi j =
    u j

Tactic:
rw [update_of_ne hj.1, v.apply_eq hj.2]

Premises used: ShrinkingLemma.PartialRefinement.apply_eq, And.right, And.left, Function.update_of_ne
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
⊢ (fun (v₁ v₂ : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦
      v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ⊆
          v₂.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)),
          v₁.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i =
            v₂.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)
    v
    (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
        vi)
      (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)

Tactic:
⟨subset_insert _ _, fun j hj => ?_⟩

Premises used: And.intro, Set.subset_insert
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
refine_6 :
  ∀ (j : ι) (hj : j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))),
    v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j =
      PartialRefinement.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
        (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
          (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))
            i vi)
          (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)
        j
⊢ (fun (v₁ v₂ : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦
      v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ⊆
          v₂.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ∧
        ∀ i ∈ v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)),
          v₁.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i =
            v₂.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)
    v
    (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
        vi)
      (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)

Tactic:
refine ⟨subset_insert _ _, fun j hj => ?_⟩
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
⊢ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j =
    PartialRefinement.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
      (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
        (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi)
        (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)
      j

Tactic:
(update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm

Premises used: Function.update, dite, ne_of_mem_of_not_mem, Eq.symm, Function.update_of_ne
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
j : ι
hj : j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
⊢ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j =
    PartialRefinement.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
      (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
        (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi)
        (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)
      j

Tactic:
exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm

Premises used: ne_of_mem_of_not_mem, Eq.symm, Function.update_of_ne
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
⊢ ¬(fun (v₁ v₂ : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦
        v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ⊆
            v₂.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)),
            v₁.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i =
              v₂.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)
      (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
        (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi)
        (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v

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

Premises used: ShrinkingLemma.PartialRefinement.carrier, And.left, Set.mem_insert, Not
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
⊢ ¬(fun (v₁ v₂ : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦
        v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ⊆
            v₂.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) ∧
          ∀ i ∈ v₁.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)),
            v₁.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i =
              v₂.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)
      (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
        (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi)
        (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)
      v

Tactic:
exact fun hle => hi (hle.1 <| mem_insert _ _)
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
refine_8 : IsCompact (closure vi)
⊢ IsCompact
    (closure
      (PartialRefinement.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
        (PartialRefinement.mk (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
          (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))
            i vi)
          (insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))) ⋯ ⋯ ⋯ ⋯ ⋯)
        i))

Tactic:
simp only [update_self]

Premises used: Function.update_self
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
⊢ IsCompact (closure vi)

Tactic:
hvi.2.2.2

Premises used: And.right
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
hsi :
  si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
vi : Set X
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i ∧ IsCompact (closure vi)
⊢ IsCompact (closure vi)

Tactic:
exact hvi.2.2.2

Premises used: And.right
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
⊢ Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))

Tactic:
haveI : Nonempty (PartialRefinement u s (fun w => IsCompact (closure w))) :=
    ⟨⟨u, ∅, uo, us, False.elim, False.elim, fun _ => rfl⟩⟩
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
s : Set X
inst_1 : T2Space X
inst_2 : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this : Nonempty (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))
⊢ ∀ (c : Set (PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w))),
    IsChain (fun (x1 x2 : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)), ∀ v ∈ c, v ≤ ub

Tactic:
have : ∀ c : Set (PartialRefinement u s (fun w => IsCompact (closure w))),
      IsChain (· ≤ ·) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub :=
    fun c hc ne => ⟨.chainSup c hc ne uf us, fun v hv => PartialRefinement.le_chainSup _ _ _ _ hv⟩