ι : 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'
ι : 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'
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
ι : 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'
ι : 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'
have C : IsClosed (s ∩ ⋂ (j) (_ : j ≠ i), v jᶜ) :=
  IsClosed.inter hs (isClosed_biInter fun _ _ => isClosed_compl_iff.2 <| v.isOpen _)
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'
ι : 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'
rcases normal_exists_closure_subset C (v.isOpen i) I with ⟨vi, ovi, hvi, cvi⟩
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)

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

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

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

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 := ?intro.intro.intro.refine'_1,
          subset_iUnion := ?intro.intro.intro.refine'_2, closure_subset := ?intro.intro.intro.refine'_3,
          apply_eq := ?intro.intro.intro.refine'_4 }.carrier ∧
    ∀ (i_1 : ι),
      i_1 ∈ v.carrier →
        toFun v i_1 =
          toFun
            { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine'_1,
              subset_iUnion := ?intro.intro.intro.refine'_2, closure_subset := ?intro.intro.intro.refine'_3,
              apply_eq := ?intro.intro.intro.refine'_4 }
            i_1

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 := ?intro.intro.intro.refine'_1,
            subset_iUnion := ?intro.intro.intro.refine'_2, closure_subset := ?intro.intro.intro.refine'_3,
            apply_eq := ?intro.intro.intro.refine'_4 }.carrier ⊆
        v.carrier ∧
      ∀ (i_1 : ι),
        i_1 ∈
            { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine'_1,
                subset_iUnion := ?intro.intro.intro.refine'_2, closure_subset := ?intro.intro.intro.refine'_3,
                apply_eq := ?intro.intro.intro.refine'_4 }.carrier →
          toFun
              { toFun := update v.toFun i vi, carrier := insert i v.carrier, isOpen := ?intro.intro.intro.refine'_1,
                subset_iUnion := ?intro.intro.intro.refine'_2, closure_subset := ?intro.intro.intro.refine'_3,
                apply_eq := ?intro.intro.intro.refine'_4 }
              i_1 =
            toFun v i_1)
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'
refine' ⟨⟨update v i vi, insert i v.carrier, _, _, _, _⟩, _, _⟩
ι : 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
ι : 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
simp only [subset_def, mem_inter_iff, mem_iInter, and_imp]
ι : 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
ι : 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
intro x hxs H
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
ι : 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
rcases mem_iUnion.1 (v.subset_iUnion hxs) with ⟨j, hj⟩
no goals
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
exact (em (j = i)).elim (fun h => h ▸ hj) fun h => (H j h hj).elim
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)
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)
intro j
no goals
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)
rcases eq_or_ne j i with (rfl| hne) <;> simp [*, v.isOpen]
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
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
refine' fun x hx => mem_iUnion.2 _
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

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
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
rcases em (∃ (j : _)(_ : j ≠ i), x ∈ v j) with (⟨j, hji, hj⟩ | h)
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
⊢ x ∈ update v.toFun i vi j
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
use j
no goals
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
⊢ x ∈ update v.toFun i vi j
rwa [update_noteq hji]
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
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
push_neg  at h
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
⊢ x ∈ update v.toFun i vi i
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
use i
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
⊢ x ∈ vi
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
⊢ x ∈ update v.toFun i vi i
rw [update_same]
no goals
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
⊢ x ∈ vi
exact hvi ⟨hx, mem_biInter h⟩
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

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
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
rintro j (rfl | hj)
no goals
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
rwa [update_same, ← v.apply_eq hi]
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
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
rw [update_noteq (ne_of_mem_of_not_mem hj hi)]
no goals
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
exact v.closure_subset hj
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
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
intro j hj
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
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
rw [mem_insert_iff, not_or] at hj
no goals
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
rw [update_noteq hj.1, v.apply_eq hj.2]
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
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
refine' ⟨subset_insert _ _, fun j hj => _⟩
no goals
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
exact (update_noteq (ne_of_mem_of_not_mem hj hi) _ _).symm
no goals
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)
exact fun hle => hi (hle.1 <| mem_insert _ _)