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
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
x : X
hx : x ∈ s
pos :
  ∀ (h : ∃ (j : ι), j ≠ i ∧ x ∈ v.toFun (u := u) (s := s) (p := ⊤) j),
    ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
neg :
  ∀ (h : ∀ (j : ι) (_ : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := ⊤) j),
    ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
⊢ ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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
x : X
hx : x ∈ s
h : ∃ (j : ι), j ≠ i ∧ x ∈ v.toFun (u := u) (s := s) (p := ⊤) j
pos :
  ∀ (j : ι) (hji : j ≠ i) (hj : x ∈ v.toFun (u := u) (s := s) (p := ⊤) j),
    ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
⊢ ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj : x ∈ v.toFun (u := u) (s := s) (p := ⊤) j
h : x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi j
⊢ ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj h h₁ h₂ h₃ : x ∈ v.toFun (u := u) (s := s) (p := ⊤) j
⊢ x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi j

Tactic:
rwa [update_of_ne hji]

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 : 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
x : X
hx : x ∈ s
h : ∀ (j : ι) (_ : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := ⊤) j
h₁ : x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i
⊢ ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1

Tactic:
use i
-- 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
x : X
hx : x ∈ s
h : ∀ (j : ι) (_ : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := ⊤) j
h₁ : x ∈ vi
⊢ x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i

Tactic:
rw [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 : 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
x : X
hx : x ∈ s
h : ∀ (j : ι) (_ : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := ⊤) j
⊢ x ∈ vi

Tactic:
hvi ⟨hx, mem_biInter h⟩

Premises used: And.intro, Set.mem_biInter
-- 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
x : X
hx : x ∈ s
h : ∀ (j : ι) (_ : j ≠ i), x ∉ v.toFun (u := u) (s := s) (p := ⊤) j
⊢ x ∈ vi

Tactic:
exact hvi ⟨hx, mem_biInter h⟩

Premises used: And.intro, Set.mem_biInter
-- 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
vi : Set X
ovi : IsOpen vi
j : ι
hi : j ∉ v.carrier (u := u) (s := s) (p := ⊤)
I : s ∩ ⋂ (j_1 : ι), ⋂ (_ : j_1 ≠ j), (v.toFun (u := u) (s := s) (p := ⊤) j_1)ᶜ ⊆ v.toFun (u := u) (s := s) (p := ⊤) j
C : IsClosed (s ∩ ⋂ (j_1 : ι), ⋂ (_ : j_1 ≠ j), (v.toFun (u := u) (s := s) (p := ⊤) j_1)ᶜ)
hvi : s ∩ ⋂ (j_1 : ι), ⋂ (_ : j_1 ≠ j), (v.toFun (u := u) (s := s) (p := ⊤) j_1)ᶜ ⊆ vi
cvi : closure vi ⊆ v.toFun (u := u) (s := s) (p := ⊤) j
refine_3 : closure vi ⊆ u j
refine_3₁ refine_3₂ refine_3₃ refine_3₄ : closure vi ⊆ v.toFun (u := u) (s := s) (p := ⊤) j
⊢ closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) j vi j) ⊆ u j

Tactic:
rwa [update_self, ← v.apply_eq hi]

Premises used: ShrinkingLemma.PartialRefinement.apply_eq, 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 : 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
j : ι
hj : j ∈ v.carrier (u := u) (s := s) (p := ⊤)
refine_3 : closure (v.toFun (u := u) (s := s) (p := ⊤) j) ⊆ u j
⊢ closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi j) ⊆ u j

Tactic:
rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]

Premises used: ne_of_mem_of_not_mem, 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 : 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
j : ι
hj : j ∈ v.carrier (u := u) (s := s) (p := ⊤)
⊢ closure (v.toFun (u := u) (s := s) (p := ⊤) j) ⊆ u j

Tactic:
v.closure_subset hj

Premises used: ShrinkingLemma.PartialRefinement.closure_subset
-- 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
j : ι
hj : j ∈ v.carrier (u := u) (s := s) (p := ⊤)
⊢ closure (v.toFun (u := u) (s := s) (p := ⊤) j) ⊆ u j

Tactic:
exact v.closure_subset hj

Premises used: ShrinkingLemma.PartialRefinement.closure_subset
-- 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
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)

Tactic:
fun _ => trivial

Premises used: trivial
-- 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
⊢ ∀ {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)

Tactic:
exact fun _ => trivial

Premises used: trivial
-- 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
j : ι
hj : j ∉ insert i (v.carrier (u := u) (s := s) (p := ⊤))
⊢ ¬j = i ∧ j ∉ v.carrier (u := u) (s := s) (p := ⊤)

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 : 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
j : ι
hj : ¬j = i ∧ j ∉ v.carrier (u := u) (s := s) (p := ⊤)
refine_5 : v.toFun (u := u) (s := s) (p := ⊤) j = u j
refine_5₁ refine_5₂ : u j = u j
⊢ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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
⊢ (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 := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)

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 : 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_6 :
  ∀ (j : ι) (hj : j ∈ v.carrier (u := u) (s := s) (p := ⊤)),
    v.toFun (u := u) (s := s) (p := ⊤) j =
      toFun (u := u) (s := s) (p := ⊤)
        (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 := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
        j
⊢ (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 := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)

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 : 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
j : ι
hj : j ∈ v.carrier (u := u) (s := s) (p := ⊤)
⊢ v.toFun (u := u) (s := s) (p := ⊤) j =
    toFun (u := u) (s := s) (p := ⊤)
      (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 := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      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 : 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
j : ι
hj : j ∈ v.carrier (u := u) (s := s) (p := ⊤)
⊢ v.toFun (u := u) (s := s) (p := ⊤) j =
    toFun (u := u) (s := s) (p := ⊤)
      (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 := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
      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 : 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
⊢ ¬(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

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 : 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
⊢ ¬(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

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 : 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
⊢ Nonempty (PartialRefinement u s ⊤)

Tactic:
haveI : Nonempty (PartialRefinement u s ⊤) :=
    ⟨⟨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 : 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 : Nonempty (PartialRefinement u s ⊤)
⊢ ∀ (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

Tactic:
have : ∀ c : Set (PartialRefinement u s ⊤),
      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⟩
-- 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
rcases :
  ∀ (v : PartialRefinement u s ⊤) (hv : IsMax v),
    ∃ (v : ι → Set X), s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
⊢ ∃ (v : ι → Set X), s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
rcases zorn_le_nonempty this with ⟨v, hv⟩

Premises used: zorn_le_nonempty
-- 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
suffices : ∀ (i : ι), i ∈ v.carrier (u := u) (s := s) (p := ⊤)
⊢ ∃ (v : ι → Set X), s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
suffices ∀ i, i ∈ v.carrier from
    ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i)⟩