ι : Type u_2
X : Type u_1
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
ι : Type u_2
X : Type u_1
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
rw [find]
case inl
ι : Type u_2
X : Type u_1
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 inr
ι : Type u_2
X : Type u_1
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
ι : Type u_2
X : Type u_1
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
split_ifs with h
no goals
case inl
ι : Type u_2
X : Type u_1
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 inr
ι : Type u_2
X : Type u_1
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
exacts [h.choose_spec.1, ne.some_mem]