[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ find c ne i ∈ c
[PROOFSTEP]
rw [find]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ (if hi : ∃ v, v ∈ c ∧ i ∈ v.carrier then Exists.choose hi else Set.Nonempty.some ne) ∈ c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ Exists.choose h ∈ c
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ¬∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ Set.Nonempty.some ne ∈ c
[PROOFSTEP]
exacts [h.choose_spec.1, ne.some_mem]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ i ∈ (find c ne i).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
rw [find]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
⊢ i ∈ (if hi : ∃ v, v ∈ c ∧ i ∈ v.carrier then Exists.choose hi else Set.Nonempty.some ne).carrier ↔
    i ∈ chainSupCarrier c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
have := h.choose_spec
[GOAL]
case pos
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∃ v, v ∈ c ∧ i ∈ v.carrier
this : Exists.choose h ∈ c ∧ i ∈ (Exists.choose h).carrier
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
exact iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)
[GOAL]
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ¬∃ v, v ∈ c ∧ i ∈ v.carrier
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∀ (v : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier c
[PROOFSTEP]
refine iff_of_false (h _ ne.some_mem) ?_
[GOAL]
case neg
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
i : ι
ne : Set.Nonempty c
h : ∀ (v : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ ¬i ∈ chainSupCarrier c
[PROOFSTEP]
simpa only [chainSupCarrier, mem_iUnion₂, not_exists]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
rcases em (∃ i, i ∉ chainSupCarrier c ∧ x ∈ u i) with (⟨i, hi, hxi⟩ | hx)
[GOAL]
case inl.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
i : ι
hi : ¬i ∈ chainSupCarrier c
hxi : x ∈ u i
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
use i
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
i : ι
hi : ¬i ∈ chainSupCarrier c
hxi : x ∈ u i
⊢ x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
simpa only [(find c ne i).apply_eq (mt (mem_find_carrier_iff _).1 hi)]
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ¬∃ i, ¬i ∈ chainSupCarrier c ∧ x ∈ u i
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
simp_rw [not_exists, not_and, not_imp_not, chainSupCarrier, mem_iUnion₂] at hx 
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ∀ (x_1 : ι), x ∈ u x_1 → ∃ i j, x_1 ∈ i.carrier
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
haveI : Nonempty (PartialRefinement u s) := ⟨ne.some⟩
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
hx : ∀ (x_1 : ι), x ∈ u x_1 → ∃ i j, x_1 ∈ i.carrier
this : Nonempty (PartialRefinement u s)
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
choose! v hvc hiv using hx
[GOAL]
case inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
rcases(hfin x hxs).exists_maximal_wrt v _ (mem_iUnion.1 (hU hxs)) with
  ⟨i, hxi : x ∈ u i, hmax : ∀ j, x ∈ u j → v i ≤ v j → v i = v j⟩
[GOAL]
case inr.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
rcases mem_iUnion.1 ((v i).subset_iUnion hxs) with ⟨j, hj⟩
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
⊢ ∃ i, x ∈ (fun i => toFun (find c ne i) i) i
[PROOFSTEP]
use j
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
⊢ x ∈ (fun i => toFun (find c ne i) i) j
[PROOFSTEP]
have hj' : x ∈ u j := (v i).subset _ hj
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
hj' : x ∈ u j
⊢ x ∈ (fun i => toFun (find c ne i) i) j
[PROOFSTEP]
have : v j ≤ v i := (hc.total (hvc _ hxi) (hvc _ hj')).elim (fun h => (hmax j hj' h).ge) id
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
c : Set (PartialRefinement u s)
hc : IsChain (fun x x_1 => x ≤ x_1) c
ne : Set.Nonempty c
hfin : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
hU : s ⊆ ⋃ (i : ι), u i
x : X
hxs : x ∈ s
this✝ : Nonempty (PartialRefinement u s)
v : ι → PartialRefinement u s
hvc : ∀ (x_1 : ι), x ∈ u x_1 → v x_1 ∈ c
hiv : ∀ (x_1 : ι), x ∈ u x_1 → x_1 ∈ (v x_1).carrier
i : ι
hxi : x ∈ u i
hmax : ∀ (j : ι), x ∈ u j → v i ≤ v j → v i = v j
j : ι
hj : x ∈ toFun (v i) j
hj' : x ∈ u j
this : v j ≤ v i
⊢ x ∈ (fun i => toFun (find c ne i) i) j
[PROOFSTEP]
simpa only [find_apply_of_mem hc ne (hvc _ hxi) (this.1 <| hiv _ hj')]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∃ v', v < v'
[PROOFSTEP]
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
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
⊢ s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
[PROOFSTEP]
simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∀ (x : X), x ∈ s → (∀ (i_1 : ι), i_1 ≠ i → x ∈ (toFun v i_1)ᶜ) → x ∈ toFun v i
[PROOFSTEP]
intro x hxs H
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
x : X
hxs : x ∈ s
H : ∀ (i_1 : ι), i_1 ≠ i → x ∈ (toFun v i_1)ᶜ
⊢ x ∈ toFun v i
[PROOFSTEP]
rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩
[GOAL]
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
x : X
hxs : x ∈ s
H : ∀ (i_1 : ι), i_1 ≠ i → x ∈ (toFun v i_1)ᶜ
j : ι
hj : x ∈ toFun v j
⊢ x ∈ toFun v i
[PROOFSTEP]
exact (em (j = i)).elim (fun h => h ▸ hj) fun h => (H j h hj).elim
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
⊢ ∃ v', v < v'
[PROOFSTEP]
have C : IsClosed (s ∩ ⋂ (j) (_ : j ≠ i), (v j)ᶜ) :=
  IsClosed.inter hs (isClosed_biInter fun _ _ => isClosed_compl_iff.2 <| v.isOpen _)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
⊢ ∃ v', v < v'
[PROOFSTEP]
rcases normal_exists_closure_subset C (v.isOpen i) I with ⟨vi, ovi, hvi, cvi⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∃ v', v < v'
[PROOFSTEP]
refine' ⟨⟨update v i vi, insert i v.carrier, _, _, _, _⟩, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∀ (i_1 : ι), IsOpen (update v.toFun i vi i_1)
[PROOFSTEP]
intro j
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
⊢ IsOpen (update v.toFun i vi j)
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | hne)
[GOAL]
case intro.intro.intro.refine'_1.inl
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
vi : Set X
ovi : IsOpen vi
j : ι
hi : ¬j ∈ v.carrier
I : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ toFun v j
C : IsClosed (s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ)
hvi : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v j
⊢ IsOpen (update v.toFun j vi j)
[PROOFSTEP]
simp [*, v.isOpen]
[GOAL]
case intro.intro.intro.refine'_1.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hne : j ≠ i
⊢ IsOpen (update v.toFun i vi j)
[PROOFSTEP]
simp [*, v.isOpen]
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ s ⊆ ⋃ (i_1 : ι), update v.toFun i vi i_1
[PROOFSTEP]
refine' fun x hx => mem_iUnion.2 _
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
rcases em (∃ (j : _) (_ : j ≠ i), x ∈ v j) with (⟨j, hji, hj⟩ | h)
[GOAL]
case intro.intro.intro.refine'_2.inl.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj : x ∈ toFun v j
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
use j
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
j : ι
hji : j ≠ i
hj : x ∈ toFun v j
⊢ x ∈ update v.toFun i vi j
[PROOFSTEP]
rwa [update_noteq hji]
[GOAL]
case intro.intro.intro.refine'_2.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ¬∃ j x_1, x ∈ toFun v j
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
push_neg at h 
[GOAL]
case intro.intro.intro.refine'_2.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → ¬x ∈ toFun v j
⊢ ∃ i_1, x ∈ update v.toFun i vi i_1
[PROOFSTEP]
use i
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → ¬x ∈ toFun v j
⊢ x ∈ update v.toFun i vi i
[PROOFSTEP]
rw [update_same]
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → ¬x ∈ toFun v j
⊢ x ∈ vi
[PROOFSTEP]
exact hvi ⟨hx, mem_biInter h⟩
[GOAL]
case intro.intro.intro.refine'_3
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i v.carrier → closure (update v.toFun i vi i_1) ⊆ u i_1
[PROOFSTEP]
rintro j (rfl | hj)
[GOAL]
case intro.intro.intro.refine'_3.inl
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
vi : Set X
ovi : IsOpen vi
j : ι
hi : ¬j ∈ v.carrier
I : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ toFun v j
C : IsClosed (s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ)
hvi : s ∩ ⋂ (j_1 : ι) (_ : j_1 ≠ j), (toFun v j_1)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v j
⊢ closure (update v.toFun j vi j) ⊆ u j
[PROOFSTEP]
rwa [update_same, ← v.apply_eq hi]
[GOAL]
case intro.intro.intro.refine'_3.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : j ∈ v.carrier
⊢ closure (update v.toFun i vi j) ⊆ u j
[PROOFSTEP]
rw [update_noteq (ne_of_mem_of_not_mem hj hi)]
[GOAL]
case intro.intro.intro.refine'_3.inr
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : j ∈ v.carrier
⊢ closure (toFun v j) ⊆ u j
[PROOFSTEP]
exact v.closure_subset hj
[GOAL]
case intro.intro.intro.refine'_4
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ∀ {i_1 : ι}, ¬i_1 ∈ insert i v.carrier → update v.toFun i vi i_1 = u i_1
[PROOFSTEP]
intro j hj
[GOAL]
case intro.intro.intro.refine'_4
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : ¬j ∈ insert i v.carrier
⊢ update v.toFun i vi j = u j
[PROOFSTEP]
rw [mem_insert_iff, not_or] at hj 
[GOAL]
case intro.intro.intro.refine'_4
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : ¬j = i ∧ ¬j ∈ v.carrier
⊢ update v.toFun i vi j = u j
[PROOFSTEP]
rw [update_noteq hj.1, v.apply_eq hj.2]
[GOAL]
case intro.intro.intro.refine'_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ v.carrier ⊆
      { toFun := update v.toFun i vi, carrier := insert i v.carrier,
          isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
          subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_1 : ι), update v.toFun i vi i_1),
          closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
          apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }.carrier ∧
    ∀ (i_1 : ι),
      i_1 ∈ v.carrier →
        toFun v i_1 =
          toFun
            { toFun := update v.toFun i vi, carrier := insert i v.carrier,
              isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
              subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_2 : ι), update v.toFun i vi i_2),
              closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
              apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }
            i_1
[PROOFSTEP]
refine' ⟨subset_insert _ _, fun j hj => _⟩
[GOAL]
case intro.intro.intro.refine'_5
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
j : ι
hj : j ∈ v.carrier
⊢ toFun v j =
    toFun
      { toFun := update v.toFun i vi, carrier := insert i v.carrier,
        isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
        subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_1 : ι), update v.toFun i vi i_1),
        closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
        apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }
      j
[PROOFSTEP]
exact (update_noteq (ne_of_mem_of_not_mem hj hi) _ _).symm
[GOAL]
case intro.intro.intro.refine'_6
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
v : PartialRefinement u s
hs : IsClosed s
i : ι
hi : ¬i ∈ v.carrier
I : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ toFun v i
C : IsClosed (s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ)
vi : Set X
ovi : IsOpen vi
hvi : s ∩ ⋂ (j : ι) (_ : j ≠ i), (toFun v j)ᶜ ⊆ vi
cvi : closure vi ⊆ toFun v i
⊢ ¬({ toFun := update v.toFun i vi, carrier := insert i v.carrier,
            isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
            subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_1 : ι), update v.toFun i vi i_1),
            closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
            apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }.carrier ⊆
        v.carrier ∧
      ∀ (i_1 : ι),
        i_1 ∈
            { toFun := update v.toFun i vi, carrier := insert i v.carrier,
                isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
                subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_2 : ι), update v.toFun i vi i_2),
                closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
                apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }.carrier →
          toFun
              { toFun := update v.toFun i vi, carrier := insert i v.carrier,
                isOpen := (_ : ∀ (j : ι), IsOpen (update v.toFun i vi j)),
                subset_iUnion := (_ : ∀ (x : X), x ∈ s → x ∈ ⋃ (i_2 : ι), update v.toFun i vi i_2),
                closure_subset := (_ : ∀ {j : ι}, j ∈ insert i v.carrier → closure (update v.toFun i vi j) ⊆ u j),
                apply_eq := (_ : ∀ {j : ι}, ¬j ∈ insert i v.carrier → update v.toFun i vi j = u j) }
              i_1 =
            toFun v i_1)
[PROOFSTEP]
exact fun hle => hi (hle.1 <| mem_insert _ _)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
haveI : Nonempty (PartialRefinement u s) := ⟨⟨u, ∅, uo, us, False.elim, fun _ => rfl⟩⟩
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this : Nonempty (PartialRefinement u s)
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
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⟩
[GOAL]
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
rcases zorn_nonempty_partialOrder this with ⟨v, hv⟩
[GOAL]
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
[PROOFSTEP]
suffices : ∀ i, i ∈ v.carrier
[GOAL]
case intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝¹ : Nonempty (PartialRefinement u s)
this✝ :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
this : ∀ (i : ι), i ∈ v.carrier
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
case this
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
[PROOFSTEP]
exact ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i)⟩
[GOAL]
case this
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
[PROOFSTEP]
contrapose! hv
[GOAL]
case this
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∃ i, ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
[PROOFSTEP]
rcases hv with ⟨i, hi⟩
[GOAL]
case this.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
[PROOFSTEP]
rcases v.exists_gt hs i hi with ⟨v', hlt⟩
[GOAL]
case this.intro.intro
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
v' : PartialRefinement u s
hlt : v < v'
⊢ ∃ a, v ≤ a ∧ a ≠ v
[PROOFSTEP]
exact ⟨v', hlt.le, hlt.ne'⟩
