awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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_1 :
  ∀ (i_1 : ι),
    IsOpen
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1)
refine_2 :
  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
refine_3 :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) →
      closure
          (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))
            i vi i_1) ⊆
        u i_1
⊢ ∃ (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))
have refine_4 : ∀ {i_1 : ι} (hi : i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))),
  IsCompact
    (closure
      (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 ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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_1 :
  ∀ (i_1 : ι),
    IsOpen
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        i_1)
refine_2 :
  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
refine_3 :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) →
      closure
          (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))
            i vi i_1) ⊆
        u i_1
refine_4 :
  ∀ {i_1 : ι} (hi : i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)))),
    IsCompact
      (closure
        (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i
          vi i_1))
⊢ ∃ (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))
have refine_5 : ∀ {i_1 : ι},
  i_1 ∉ insert i (v.carrier (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
        i_1 =
      u i_1
Tactic: refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ⟨?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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 : ι
⊢ IsOpen
    (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
      j)
have 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)
Tactic: rcases eq_or_ne j i with (rfl | hne)
Cleared hypotheses: i, hi, si, hsi, hsic, this, hvi
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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)
⊢ IsOpen
    (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
      j)
have 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)
Tactic: rcases eq_or_ne j i with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
have 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
Tactic: refine fun x hx => mem_iUnion.2 ?_
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ ∃ (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
have 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
Tactic: by_cases! h : ∃ j ≠ i, x ∈ v j
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ ∃ (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
have 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
Tactic: by_cases! h : ∃ j ≠ i, x ∈ v j
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases h with ⟨j, hji, hj⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ ∃ (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
have h : x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi j
Tactic: use j
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ ∃ (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
have h₁ : x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi i
Tactic: use i
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ x ∈
    update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi i
have h₁ : x ∈ vi
Tactic: rw [update_self]
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ x ∈ vi
have h₁ : x ∈ si
Tactic: apply hvi.2.1
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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
⊢ x ∈ si
have h₁ : x ∈ s ∩ ⋂ (i_1 : ι), ⋂ (_ : ¬i_1 = i), (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) i_1)ᶜ
Tactic: rw [hsi]
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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)
⊢ closure
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) j vi
        j) ⊆
    u j
have refine_3 : closure vi ⊆ u j
Tactic: rw [update_self]
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (goal)
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))
⊢ closure
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        j) ⊆
    u j
have refine_3 : closure (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w)) j) ⊆ u j
Tactic: rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
-- Lean 4 proof step from Mathlib.Topology.ShrinkingLemma (hypothesis)
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)))
⊢ IsCompact
    (closure
      (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))) i vi
        j))
have hj₁ : j = i ∨ j ∈ v.carrier (u := u) (s := s) (p := fun (w : Set X) ↦ IsCompact (closure w))
Tactic: rw [mem_insert_iff] at hj
Cleared hypotheses: hj