awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s p)
v : (x : ι) → PartialRefinement u s p
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier (u := u) (s := s) (p := p)
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v j ≤ v i
j : ι
hj : x ∈ (v i).toFun (u := u) (s := s) (p := p) j
hj' : x ∈ u j
⊢ x ∈ (find (u := u) (s := s) (p := p) c ne j).toFun (u := u) (s := s) (p := p) j
have this₁ : v j ≤ v i
Tactic: have : v j ≤ v i := (hc.total (hvc _ hxi) (hvc _ hj')).elim (hmax j hj') id
-- 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
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
i : ι
hi : i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
⊢ p ((find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i)
have obtain : ∀ (v : PartialRefinement u s p)
  (hv : Membership.mem (γ := Set ι) (⋃ (_ : v ∈ c), v.carrier (u := u) (s := s) (p := p)) i),
  p ((find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i)
Tactic: obtain ⟨v, hv⟩ := Set.mem_iUnion.mp 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
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
i : ι
hi : i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
v : PartialRefinement u s p
hv : Membership.mem (γ := Set ι) (⋃ (_ : v ∈ c), v.carrier (u := u) (s := s) (p := p)) i
⊢ p ((find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i)
have hv₁ : v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)
Tactic: simp only [mem_iUnion, exists_prop] at hv
Cleared hypotheses: hv
-- 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
p : Set X → Prop
c : Set (PartialRefinement u s p)
hc : IsChain (fun (x1 x2 : PartialRefinement u s p) ↦ x1 ≤ x2) c
ne : c.Nonempty
hfin : ∀ x ∈ s, Set.Finite.{u_1} (α := ι) {i : ι | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
i : ι
hi : i ∈ chainSupCarrier (u := u) (s := s) (p := p) c
v : PartialRefinement u s p
hv : v ∈ c ∧ i ∈ v.carrier (u := u) (s := s) (p := p)
⊢ p ((find (u := u) (s := s) (p := p) c ne i).toFun (u := u) (s := s) (p := p) i)
have rw : p (v.toFun (u := u) (s := s) (p := p) i)
Tactic: rw [find_apply_of_mem hc ne hv.1 hv.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 : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)
⊢ s ∩ ⋂ (j : ι), ⋂ (_ : j ≠ i), (v.toFun (u := u) (s := s) (p := ⊤) j)ᶜ ⊆ v.toFun (u := u) (s := s) (p := ⊤) i
have simp : ∀ x ∈ s,
  (∀ (i_1 : ι) (i : i_1 ≠ i), x ∈ (v.toFun (u := u) (s := s) (p := ⊤) i_1)ᶜ) → x ∈ v.toFun (u := u) (s := s) (p := ⊤) i
Tactic: simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]
-- 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 : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)
x : X
hxs : x ∈ s
H : ∀ (i_1 : ι) (i : i_1 ≠ i), x ∈ (v.toFun (u := u) (s := s) (p := ⊤) i_1)ᶜ
⊢ x ∈ v.toFun (u := u) (s := s) (p := ⊤) i
have rcases : ∀ (j : ι) (hj : x ∈ v.toFun (u := u) (s := s) (p := ⊤) j), x ∈ v.toFun (u := u) (s := s) (p := ⊤) i
Tactic: rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩
-- 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 : NormalSpace X
v : PartialRefinement u s ⊤
hs : IsClosed s
i : ι
hi : i ∉ v.carrier (u := u) (s := s) (p := ⊤)
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have I : s ∩ ⋂ (j : ι), ⋂ (_ : j ≠ i), (v.toFun (u := u) (s := s) (p := ⊤) j)ᶜ ⊆ v.toFun (u := u) (s := s) (p := ⊤) i
Tactic: have I : (s ∩ ⋂ (j) (_ : j ≠ i), (v j)ᶜ) ⊆ v i := by
    simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]
    intro x hxs H
    rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩
    exact (em (j = i)).elim (fun h => h ▸ hj) fun h => (H j h hj).elim
-- 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 : 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
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have C : IsClosed (s ∩ ⋂ (j : ι), ⋂ (_ : j ≠ i), (v.toFun (u := u) (s := s) (p := ⊤) j)ᶜ)
Tactic: have C : IsClosed (s ∩ ⋂ (j) (_ : j ≠ i), (v j)ᶜ) :=
    IsClosed.inter hs (isClosed_biInter fun _ _ => isClosed_compl_iff.2 <| v.isOpen _)
-- 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 : 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)ᶜ)
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have rcases : ∀ (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), ∃ (v' : PartialRefinement u s ⊤), v < v'
Tactic: rcases normal_exists_closure_subset C (v.isOpen i) I with ⟨vi, ovi, hvi, cvi⟩
-- 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 : 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
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have refine_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have refine_2 : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_2 : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have refine_3 : ∀ {i_1 : ι},
  i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
    closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_2 : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
refine_3 :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1) ⊆ u i_1
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have refine_4 : ∀ {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: 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 : 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_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_2 : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
refine_3 :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1) ⊆ u i_1
refine_4 :
  ∀ {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)
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have refine_5 : ∀ {i_1 : ι},
  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 = 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 : 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_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_2 : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
refine_3 :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1) ⊆ u i_1
refine_4 :
  ∀ {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)
refine_5 :
  ∀ {i_1 : ι},
    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 = u i_1
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have refine_6 : (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 := ⊤))) sorry sorry sorry sorry sorry)
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 : 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_1 : ∀ (i_1 : ι), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1)
refine_2 : s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
refine_3 :
  ∀ {i_1 : ι},
    i_1 ∈ insert i (v.carrier (u := u) (s := s) (p := ⊤)) →
      closure (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1) ⊆ u i_1
refine_4 :
  ∀ {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)
refine_5 :
  ∀ {i_1 : ι},
    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 = u i_1
refine_6 :
  (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 := ⊤))) ⋯ ⋯ ⋯ ⋯ ⋯)
⊢ ∃ (v' : PartialRefinement u s ⊤), v < v'
have refine_7 : ¬(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 := ⊤))) sorry sorry sorry sorry sorry)
    v
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 : 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 : ι
⊢ IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi j)
have refine_1 : ∀ (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),
  IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) j vi j)
Tactic: rcases eq_or_ne j i with (rfl | hne)
Cleared hypotheses: i, hi, I, C, hvi, cvi
-- 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 : 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 : ι
refine_1 :
  ∀ (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),
    IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) j vi j)
⊢ IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi j)
have refine_1₁ : ∀ (hne : j ≠ i), IsOpen (update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 : 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
⊢ s ⊆ ⋃ (i_1 : ι), update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) 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 := ⊤)) 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 : 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
⊢ ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
have 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
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 : 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
⊢ ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
have 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
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 : 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
⊢ ∃ (i_1 : ι), x ∈ update (β := fun (a : ι) ↦ Set X) (v.toFun (u := u) (s := s) (p := ⊤)) i vi i_1
have 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
Tactic: rcases h with ⟨j, hji, hj⟩
Cleared hypotheses: h