ι : 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
⊢ i ∈ (if hi : ∃ v, v ∈ c ∧ i ∈ v.carrier then Exists.choose hi else Set.Nonempty.some ne).carrier ↔
    i ∈ chainSupCarrier 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
⊢ i ∈ (find c ne i).carrier ↔ i ∈ chainSupCarrier 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
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier 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
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier 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
⊢ i ∈ (if hi : ∃ v, v ∈ c ∧ i ∈ v.carrier then Exists.choose hi else Set.Nonempty.some ne).carrier ↔
    i ∈ chainSupCarrier c
split_ifs with h
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
this : Exists.choose h ∈ c ∧ i ∈ (Exists.choose h).carrier
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier c
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
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier c
have := h.choose_spec
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
this : Exists.choose h ∈ c ∧ i ∈ (Exists.choose h).carrier
⊢ i ∈ (Exists.choose h).carrier ↔ i ∈ chainSupCarrier c
exact iff_of_true this.2 (mem_iUnion₂.2 ⟨_, this.1, this.2⟩)
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 : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier 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
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier c
push_neg at h
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 : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ ¬i ∈ chainSupCarrier 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 : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ i ∈ (Set.Nonempty.some ne).carrier ↔ i ∈ chainSupCarrier c
refine iff_of_false (h _ ne.some_mem) ?_
no goals
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 : PartialRefinement u s), v ∈ c → ¬i ∈ v.carrier
⊢ ¬i ∈ chainSupCarrier c
simpa only [chainSupCarrier, mem_iUnion₂, not_exists]