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
x : X
hx : x ∈ si
this : ∀ (j : ι) (hj : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
obtain :
  ∀ (j : ι) (hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j),
    x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i
⊢ x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i

Tactic:
obtain ⟨j, hj⟩ := Set.mem_iUnion.mp
      (v.subset_iUnion (Set.mem_of_mem_inter_left hx))

Premises used: Set.mem_iUnion, Set.mem_of_mem_inter_left, Iff.mp, ShrinkingLemma.PartialRefinement.subset_iUnion
-- 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
x : X
hx : x ∈ si
this : ∀ (j : ι) (hj : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
j : ι
hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
by_contra! : ∀ (h : j ≠ i), False
⊢ j = i

Tactic:
by_contra! h
-- 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
x : X
hx : x ∈ si
this : ∀ (j : ι) (hj : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
j : ι
hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
h : j ≠ i
⊢ False

Tactic:
this j h 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
x : X
hx : x ∈ si
this : ∀ (j : ι) (hj : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
j : ι
hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
h : j ≠ i
⊢ False

Tactic:
exact this j h 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
x : X
hx : x ∈ si
this : ∀ (j : ι) (hj : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
j : ι
hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
obtain :
  ∀ (hi : j ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))),
    let si :=
      s ∩ (⋃ (j_1 : ι), ⋃ (_ : j_1 ≠ j), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1)ᶜ;
    ∀
      (hsi :
        si =
          s ∩ ⋂ (i : ι), ⋂ (_ : ¬i = j), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)ᶜ)
      (hsic : IsCompact si) (hx : x ∈ si)
      (this :
        ∀ (j_1 : ι) (hj : j_1 ≠ j), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1),
      x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
⊢ x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i

Tactic:
obtain rfl : j = i := by
      by_contra! h
      exact this j h hj

Premises used: 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
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
x : X
j : ι
hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
hi : j ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j_1 : ι), ⋃ (_ : j_1 ≠ j), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1)ᶜ
hsi : si = s ∩ ⋂ (i : ι), ⋂ (_ : ¬i = j), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)ᶜ
hsic : IsCompact si
hx : x ∈ si
this : ∀ (j_1 : ι) (hj : j_1 ≠ j), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1
⊢ x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j

Tactic:
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
x : X
j : ι
hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
hi : j ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j_1 : ι), ⋃ (_ : j_1 ≠ j), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1)ᶜ
hsi : si = s ∩ ⋂ (i : ι), ⋂ (_ : ¬i = j), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)ᶜ
hsic : IsCompact si
hx : x ∈ si
this : ∀ (j_1 : ι) (hj : j_1 ≠ j), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1
⊢ x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j

Tactic:
exact 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
⊢ si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i

Tactic:
have : si ⊆ v i := by
    intro x hx
    have (j) (hj : j ≠ i) : x ∉ v j := by
      rw [hsi] at hx
      apply Set.notMem_of_mem_compl
      have hsi' : x ∈ (⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ) := Set.mem_of_mem_inter_right hx
      rw [ne_eq] at hj
      rw [Set.mem_iInter₂] at hsi'
      exact hsi' j hj
    obtain ⟨j, hj⟩ := Set.mem_iUnion.mp
      (v.subset_iUnion (Set.mem_of_mem_inter_left hx))
    obtain rfl : j = i := by
      by_contra! h
      exact this j h hj
    exact 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
obtain :
  ∀ (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)),
    ∃ (v' : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)),
      v < v' ∧ IsCompact (closure (v'.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))
⊢ ∃ (v' : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)),
    v < v' ∧ IsCompact (closure (v'.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))

Tactic:
obtain ⟨vi, hvi⟩ := exists_open_between_and_isCompact_closure hsic (v.isOpen i) this

Premises used: exists_open_between_and_isCompact_closure, ShrinkingLemma.PartialRefinement.isOpen
-- 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)
⊢ ∃ (v' : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)),
    v < v' ∧ IsCompact (closure (v'.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i))

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

Premises used: Function.update, ShrinkingLemma.PartialRefinement.carrier, ShrinkingLemma.PartialRefinement.mk, Insert.insert, ShrinkingLemma.PartialRefinement.toFun, And.intro, Exists.intro
-- 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 : ι
refine_1 :
  ∀ (hi : j ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))),
    let si :=
      s ∩ (⋃ (j_1 : ι), ⋃ (_ : j_1 ≠ j), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1)ᶜ;
    ∀
      (hsi :
        si =
          s ∩ ⋂ (i : ι), ⋂ (_ : ¬i = j), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)ᶜ)
      (hsic : IsCompact si) (this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)
      (hvi :
        IsOpen vi ∧
          si ⊆ vi ∧
            closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j ∧
              IsCompact (closure vi)),
      IsOpen
        (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) j
          vi j)
refine_1₁ :
  ∀ (hne : j ≠ i),
    IsOpen
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        j)
⊢ IsOpen
    (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
      j)

Tactic:
rcases eq_or_ne j i with (rfl | hne)

Premises used: eq_or_ne, 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
v : PartialRefinement u s fun (w : Set X) ↦ IsCompact (closure w)
hs : IsCompact s
vi : Set X
j : ι
hi : j ∉ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
si : Set X :=
  s ∩ (⋃ (j_1 : ι), ⋃ (_ : j_1 ≠ j), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j_1)ᶜ
hsi : si = s ∩ ⋂ (i : ι), ⋂ (_ : ¬i = j), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
hvi :
  IsOpen vi ∧
    si ⊆ vi ∧
      closure vi ⊆ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j ∧ IsCompact (closure vi)
⊢ IsOpen
    (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) j vi
      j)

Tactic:
simp [*, v.isOpen]

Premises used: ShrinkingLemma.PartialRefinement.isOpen
-- 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 : ι
hne : j ≠ i
⊢ IsOpen
    (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
      j)

Tactic:
simp [*, v.isOpen]

Premises used: ShrinkingLemma.PartialRefinement.isOpen
-- 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)
⊢ s ⊆
    ⋃ (i_1 : ι),
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1

Tactic:
fun x hx => mem_iUnion.2 ?_

Premises used: Iff.mpr, Set.mem_iUnion, Set.Subset
-- 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_2 :
  ∀ (x : X) (hx : x ∈ s),
    ∃ (i_1 : ι),
      x ∈
        update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi i_1
⊢ s ⊆
    ⋃ (i_1 : ι),
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1

Tactic:
refine fun x hx => mem_iUnion.2 ?_

Premises used: Iff.mpr, Set.mem_iUnion
-- 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)
x : X
hx : x ∈ s
pos :
  ∀ (h : ∃ (j : ι), j ≠ i ∧ x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j),
    ∃ (i_1 : ι),
      x ∈
        update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi i_1
neg :
  ∀ (h : ∀ (j : ι) (_ : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j),
    ∃ (i_1 : ι),
      x ∈
        update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi i_1
⊢ ∃ (i_1 : ι),
    x ∈
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1

Tactic:
by_cases! h : ∃ j ≠ i, x ∈ v j
-- 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)
x : X
hx : x ∈ s
h : ∃ (j : ι), j ≠ i ∧ x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
pos :
  ∀ (j : ι) (hji : j ≠ i) (hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j),
    ∃ (i_1 : ι),
      x ∈
        update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi i_1
⊢ ∃ (i_1 : ι),
    x ∈
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1

Tactic:
rcases h with ⟨j, hji, 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)
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
h :
  x ∈
    update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi j
⊢ ∃ (i_1 : ι),
    x ∈
      update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1

Tactic:
use j
-- 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)
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj h h₁ h₂ h₃ : x ∈ v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j
⊢ x ∈
    update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi j

Tactic:
rwa [update_of_ne hji]

Premises used: Function.update_of_ne