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 : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s ⊤)
this :
  ∀ (c : Set (PartialRefinement u s ⊤)),
    IsChain (fun (x1 x2 : PartialRefinement u s ⊤) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s ⊤), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
by_contra : ∀ (hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)), False
⊢ i ∈ v.carrier (u := u) (s := s) (p := ⊤)

Tactic:
by_contra hi
-- 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
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s ⊤)
this :
  ∀ (c : Set (PartialRefinement u s ⊤)),
    IsChain (fun (x1 x2 : PartialRefinement u s ⊤) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s ⊤), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)
rcases : ∀ (v' : PartialRefinement u s ⊤) (hlt : v < v'), False
⊢ False

Tactic:
rcases v.exists_gt hs i hi with ⟨v', hlt⟩

Premises used: ShrinkingLemma.PartialRefinement.exists_gt
-- 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
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s ⊤)
this :
  ∀ (c : Set (PartialRefinement u s ⊤)),
    IsChain (fun (x1 x2 : PartialRefinement u s ⊤) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s ⊤), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)
v' : PartialRefinement u s ⊤
hlt : v < v'
⊢ False

Tactic:
hv.not_lt hlt

Premises used: IsMax.not_lt
-- 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
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this_1 : Nonempty (PartialRefinement u s ⊤)
this :
  ∀ (c : Set (PartialRefinement u s ⊤)),
    IsChain (fun (x1 x2 : PartialRefinement u s ⊤) ↦ x1 ≤ x2) c →
      c.Nonempty → ∃ (ub : PartialRefinement u s ⊤), ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)
v' : PartialRefinement u s ⊤
hlt : v < v'
⊢ False

Tactic:
exact hv.not_lt hlt

Premises used: IsMax.not_lt
-- 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
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
⊢ ∃ (v : ι → Set X), s ⊆ iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i

Tactic:
let ⟨v, hsv, _, hv⟩ := exists_subset_iUnion_closure_subset hs uo uf us
  ⟨fun i => closure (v i), Subset.trans hsv (iUnion_mono fun _ => subset_closure),
    fun _ => isClosed_closure, hv⟩

Premises used: exists_subset_iUnion_closure_subset, Set.Subset.trans, subset_closure, Exists, HasSubset.Subset, And, closure, And.intro, Exists.intro, _private.0.exists_subset_iUnion_closed_subset.match_1, Set.iUnion_mono, isClosed_closure, Set.iUnion
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
inst_1 : NormalSpace X
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
uU : Eq.{u_2 + 1} (α := Set X) (⋃ (i : ι), u i) univ
⊢ ∃ (v : ι → Set X), iUnion v = univ ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
let ⟨v, vU, hv⟩ := exists_subset_iUnion_closure_subset isClosed_univ uo (fun x _ => uf x) uU.ge
  ⟨v, univ_subset_iff.1 vU, hv⟩

Premises used: isClosed_univ, Set.univ_subset_iff, Eq.ge, exists_subset_iUnion_closure_subset, Set.univ, Exists, And, And.intro, Exists.intro, Iff.mp, Eq, Set.iUnion, _private.0.exists_iUnion_eq_closure_subset.match_1
-- Module: Mathlib.Topology.ShrinkingLemma
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
u : ι → Set X
inst_1 : NormalSpace X
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
uU : Eq.{u_2 + 1} (α := Set X) (⋃ (i : ι), u i) univ
⊢ ∃ (v : ι → Set X), iUnion v = univ ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i

Tactic:
let ⟨v, vU, hv⟩ := exists_subset_iUnion_closed_subset isClosed_univ uo (fun x _ => uf x) uU.ge
  ⟨v, univ_subset_iff.1 vU, hv⟩

Premises used: isClosed_univ, Set.univ_subset_iff, Eq.ge, Set.univ, Exists, exists_subset_iUnion_closed_subset, And, _private.0.exists_iUnion_eq_closed_subset.match_1, And.intro, Exists.intro, Iff.mp, Eq, Set.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))
⊢ let si := s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ;
  si = s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ

Tactic:
set si := s ∩ (⋃ j ≠ i, v j)ᶜ with hsi

Premises used: ShrinkingLemma.PartialRefinement.toFun, Set.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 ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ
⊢ si =
    s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ

Tactic:
simp only [ne_eq, compl_iUnion] at hsi

Premises used: ne_eq, Set.compl_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)ᶜ
apply :
  IsClosed (s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ)
⊢ IsCompact si

Tactic:
apply IsCompact.of_isClosed_subset hs _ Set.inter_subset_left

Premises used: Set.inter_subset_left, IsCompact.of_isClosed_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)ᶜ
h :
  ∀ (i_1 : ι),
    Membership.mem (γ := Set ι) (fun (i_2 : ι) ↦ i_2 = i → False) i_1 →
      IsOpen (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)
⊢ IsOpen.{u_2} (X := X)
    (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)

Tactic:
apply isOpen_biUnion

Premises used: isOpen_biUnion
-- 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)ᶜ
j : ι
h :
  Membership.mem (γ := Set ι) (fun (i_1 : ι) ↦ i_1 = i → False) j →
    IsOpen (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)
⊢ Membership.mem (γ := Set ι) (fun (i_1 : ι) ↦ i_1 = i → False) j →
    IsOpen (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)

Tactic:
_
-- 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)ᶜ
j : ι
h : Membership.mem (γ := Set ι) (fun (i_1 : ι) ↦ i_1 = i → False) j
⊢ IsOpen (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)

Tactic:
v.isOpen j

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)ᶜ
j : ι
h : Membership.mem (γ := Set ι) (fun (i_1 : ι) ↦ i_1 = i → False) j
⊢ IsOpen (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)

Tactic:
exact v.isOpen j

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)ᶜ
⊢ IsOpen.{u_2} (X := X)
    (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)

Tactic:
have : IsOpen (⋃ j ≠ i, v j) := by
        apply isOpen_biUnion
        intro j _
        exact v.isOpen 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)ᶜ
this :
  IsOpen.{u_2} (X := X)
    (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)
⊢ IsClosed (s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ)

Tactic:
IsClosed.inter (IsCompact.isClosed hs) (IsOpen.isClosed_compl this)

Premises used: IsOpen.isClosed_compl, IsClosed.inter, IsCompact.isClosed
-- 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)ᶜ
this :
  IsOpen.{u_2} (X := X)
    (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)
⊢ IsClosed (s ∩ (⋃ (j : ι), ⋃ (_ : j ≠ i), v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ)

Tactic:
exact IsClosed.inter (IsCompact.isClosed hs) (IsOpen.isClosed_compl this)

Premises used: IsOpen.isClosed_compl, IsClosed.inter, IsCompact.isClosed
-- 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)ᶜ
⊢ IsCompact si

Tactic:
have hsic : IsCompact si := by
    apply IsCompact.of_isClosed_subset hs _ Set.inter_subset_left
    · have : IsOpen (⋃ j ≠ i, v j) := by
        apply isOpen_biUnion
        intro j _
        exact v.isOpen j
      exact IsClosed.inter (IsCompact.isClosed hs) (IsOpen.isClosed_compl this)
-- 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
j : ι
hj : j ≠ i
rw :
  ∀
    (hx :
      x ∈
        s ∩
          ⋂ (i_1 : ι),
            ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ)
    (j : ι) (hj : j ≠ i), 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)) j

Tactic:
rw [hsi] at hx
-- 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 ∈ s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
j : ι
hj : j ≠ i
⊢ Membership.mem (γ := Set X)
    (⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ) x

Tactic:
have hsi' : x ∈ (⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ) := Set.mem_of_mem_inter_right hx
-- 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 ∈ s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
j : ι
hj : j ≠ i
hsi' :
  Membership.mem (γ := Set X)
    (⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ) x
⊢ ¬j = i

Tactic:
rw [ne_eq] at hj

Premises used: ne_eq
-- 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 ∈ s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
j : ι
hj : j ≠ i
hsi' :
  Membership.mem (γ := Set X)
    (⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ) x
hj₁ : ¬j = i
⊢ Membership.mem (γ := Set X)
    (⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ) x

Tactic:
rw [ne_eq] at hj

Premises used: ne_eq
-- 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 ∈ s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
j : ι
hj : ¬j = i
hsi' :
  Membership.mem (γ := Set X)
    (⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ) x
⊢ ∀ (i_1 : ι) (j : ¬i_1 = i), x ∈ (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ

Tactic:
rw [Set.mem_iInter₂] at hsi'

Premises used: Set.mem_iInter₂
-- 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 ∈ s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
j : ι
hj : ¬j = i
hsi' : ∀ (i_1 : ι) (j : ¬i_1 = i), x ∈ (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
⊢ x ∈ (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ

Tactic:
hsi' 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
x : X
hx :
  x ∈ s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
j : ι
hj : ¬j = i
hsi' : ∀ (i_1 : ι) (j : ¬i_1 = i), x ∈ (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
⊢ x ∈ (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j)ᶜ

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

Tactic:
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