[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ (i : ι), v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
[PROOFSTEP]
have :=
  ParacompactSpace.locallyFinite_refinement (range u) (fun r ↦ (r : Set X)) (SetCoe.forall.2 <| forall_range_iff.2 uo)
    (by rwa [← sUnion_range, Subtype.range_coe])
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
⊢ ⋃ (a : ↑(range u)), (fun r => ↑r) a = univ
[PROOFSTEP]
rwa [← sUnion_range, Subtype.range_coe]
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
this : ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ (fun r => ↑r) a
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ (i : ι), v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
[PROOFSTEP]
simp only [SetCoe.exists, exists_range_iff', iUnion_eq_univ_iff, exists_prop] at this 
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
this : ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ (∀ (x : X), ∃ i, x ∈ t i) ∧ LocallyFinite t ∧ ∀ (b : β), ∃ i, t b ⊆ u i
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ (i : ι), v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
[PROOFSTEP]
choose α t hto hXt htf ind hind using this
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
hXt : ∀ (x : X), ∃ i, x ∈ t i
htf : LocallyFinite t
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ (i : ι), v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
[PROOFSTEP]
choose t_inv ht_inv using hXt
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
htf : LocallyFinite t
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ (i : ι), v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
[PROOFSTEP]
choose U hxU hU using htf
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ (i : ι), v i = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
[PROOFSTEP]
refine' ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, _, _, _, _⟩
[GOAL]
case refine'_1
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι), IsOpen ((fun i => ⋃ (a : α) (_ : ind a = i), t a) a)
[PROOFSTEP]
exact fun a ↦ isOpen_iUnion fun a ↦ isOpen_iUnion fun _ ↦ hto a
[GOAL]
case refine'_2
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ⋃ (i : ι), (fun i => ⋃ (a : α) (_ : ind a = i), t a) i = univ
[PROOFSTEP]
simp only [eq_univ_iff_forall, mem_iUnion]
[GOAL]
case refine'_2
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (x : X), ∃ i i_1 i, x ∈ t i_1
[PROOFSTEP]
exact fun x ↦ ⟨ind (t_inv x), _, rfl, ht_inv _⟩
[GOAL]
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ LocallyFinite fun i => ⋃ (a : α) (_ : ind a = i), t a
[PROOFSTEP]
refine' fun x ↦ ⟨U x, hxU x, ((hU x).image ind).subset _⟩
[GOAL]
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
⊢ {i | Set.Nonempty ((fun i => ⋃ (a : α) (_ : ind a = i), t a) i ∩ U x)} ⊆ ind '' {i | Set.Nonempty (t i ∩ U x)}
[PROOFSTEP]
simp only [subset_def, mem_iUnion, mem_setOf_eq, Set.Nonempty, mem_inter_iff]
[GOAL]
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
⊢ ∀ (x_1 : ι), (∃ x_2, (∃ i i_1, x_2 ∈ t i) ∧ x_2 ∈ U x) → x_1 ∈ ind '' {i | ∃ x_2, x_2 ∈ t i ∧ x_2 ∈ U x}
[PROOFSTEP]
rintro i ⟨y, ⟨a, rfl, hya⟩, hyU⟩
[GOAL]
case refine'_3.intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x y : X
hyU : y ∈ U x
a : α
hya : y ∈ t a
⊢ ind a ∈ ind '' {i | ∃ x_1, x_1 ∈ t i ∧ x_1 ∈ U x}
[PROOFSTEP]
exact mem_image_of_mem _ ⟨y, hya, hyU⟩
[GOAL]
case refine'_4
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι), (fun i => ⋃ (a : α) (_ : ind a = i), t a) a ⊆ u a
[PROOFSTEP]
simp only [subset_def, mem_iUnion]
[GOAL]
case refine'_4
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι) (x : X), (∃ i i_1, x ∈ t i) → x ∈ u a
[PROOFSTEP]
rintro i x ⟨a, rfl, hxa⟩
[GOAL]
case refine'_4.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : ⋃ (i : ι), u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
a : α
hxa : x ∈ t a
⊢ x ∈ u (ind a)
[PROOFSTEP]
exact hind _ hxa
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
[PROOFSTEP]
have uc : (iUnion fun i => Option.elim' sᶜ u i) = univ :=
  by
  apply Subset.antisymm (subset_univ _)
  · simp_rw [← compl_union_self s, Option.elim', iUnion_option]
    apply union_subset_union_right sᶜ us
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ ⋃ (i : Option ι), Option.elim' sᶜ u i = univ
[PROOFSTEP]
apply Subset.antisymm (subset_univ _)
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ univ ⊆ ⋃ (i : Option ι), Option.elim' sᶜ u i
[PROOFSTEP]
simp_rw [← compl_union_self s, Option.elim', iUnion_option]
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
⊢ sᶜ ∪ s ⊆ sᶜ ∪ ⋃ (a : ι), u a
[PROOFSTEP]
apply union_subset_union_right sᶜ us
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : ⋃ (i : Option ι), Option.elim' sᶜ u i = univ
⊢ ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
[PROOFSTEP]
rcases precise_refinement (Option.elim' sᶜ u) (Option.forall.2 ⟨isOpen_compl_iff.2 hs, uo⟩) uc with ⟨v, vo, vc, vf, vu⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : ⋃ (i : Option ι), Option.elim' sᶜ u i = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vc : ⋃ (i : Option ι), v i = univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
⊢ ∃ v, (∀ (i : ι), IsOpen (v i)) ∧ s ⊆ ⋃ (i : ι), v i ∧ LocallyFinite v ∧ ∀ (i : ι), v i ⊆ u i
[PROOFSTEP]
refine' ⟨v ∘ some, fun i ↦ vo _, _, vf.comp_injective (Option.some_injective _), fun i ↦ vu _⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : ⋃ (i : Option ι), Option.elim' sᶜ u i = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vc : ⋃ (i : Option ι), v i = univ
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i
[PROOFSTEP]
simp only [iUnion_option, ← compl_subset_iff_union] at vc 
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
s : Set X
hs : IsClosed s
u : ι → Set X
uo : ∀ (i : ι), IsOpen (u i)
us : s ⊆ ⋃ (i : ι), u i
uc : ⋃ (i : Option ι), Option.elim' sᶜ u i = univ
v : Option ι → Set X
vo : ∀ (a : Option ι), IsOpen (v a)
vf : LocallyFinite v
vu : ∀ (a : Option ι), v a ⊆ Option.elim' sᶜ u a
vc : (v none)ᶜ ⊆ ⋃ (i : ι), v (some i)
⊢ s ⊆ ⋃ (i : ι), (v ∘ some) i
[PROOFSTEP]
exact Subset.trans (subset_compl_comm.1 <| vu Option.none) vc
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
choose U hUo hU using fun a ↦ he.isOpen_iff.1 (ho a)
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
simp only [← hU] at hu ⊢
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ (a : α), e ⁻¹' U a = univ
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
[PROOFSTEP]
have heU : range e ⊆ ⋃ i, U i := by simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using hu
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ (a : α), e ⁻¹' U a = univ
⊢ range e ⊆ ⋃ (i : α), U i
[PROOFSTEP]
simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using hu
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ (a : α), e ⁻¹' U a = univ
heU : range e ⊆ ⋃ (i : α), U i
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
[PROOFSTEP]
rcases precise_refinement_set he.closed_range U hUo heU with ⟨V, hVo, heV, hVf, hVU⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ (a : α), e ⁻¹' U a = univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
[PROOFSTEP]
refine
  ⟨α, fun a ↦ e ⁻¹' (V a), fun a ↦ (hVo a).preimage he.continuous, ?_, hVf.preimage_continuous he.continuous, fun a ↦
    ⟨a, preimage_mono (hVU a)⟩⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : ⋃ (a : α), e ⁻¹' U a = univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ ⋃ (b : α), (fun a => e ⁻¹' V a) b = univ
[PROOFSTEP]
simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using heV
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have : ∀ (x : X) (y : Y), ∃ (a : α) (U : Set X) (V : Set Y), IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a :=
  fun x y ↦ (iUnion_eq_univ_iff.1 hu (x, y)).imp fun a ha ↦ isOpen_prod_iff.1 (ho a) x y ha
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
this : ∀ (x : X) (y : Y), ∃ a U V, IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
choose a U V hUo hVo hxU hyV hUV using this
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
choose T hT using fun y ↦ CompactSpace.elim_nhds_subcover (U · y) fun x ↦ (hUo x y).mem_nhds (hxU x y)
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
set W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have hWo : ∀ y, IsOpen (W y) := fun y ↦ isOpen_biInter_finset fun _ _ ↦ hVo _ _
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have hW : ∀ y, y ∈ W y := fun _ ↦ mem_iInter₂.2 fun _ _ ↦ hyV _ _
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
rcases precise_refinement W hWo (iUnion_eq_univ_iff.2 fun y ↦ ⟨y, hW y⟩) with ⟨E, hEo, hE, hEf, hEA⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
refine
  ⟨Σ y, T y, fun z ↦ U z.2.1 z.1 ×ˢ E z.1, fun _ ↦ (hUo _ _).prod (hEo _), iUnion_eq_univ_iff.2 fun (x, y) ↦ ?_,
    fun (x, y) ↦ ?_, fun ⟨y, x, hx⟩ ↦ ?_⟩
[GOAL]
case intro.intro.intro.intro.refine_1
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
⊢ ∃ i, (x, y) ∈ (fun z => U (↑z.snd) z.fst ×ˢ E z.fst) i
[PROOFSTEP]
rcases iUnion_eq_univ_iff.1 hE y with ⟨b, hb⟩
[GOAL]
case intro.intro.intro.intro.refine_1.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y b : Y
hb : y ∈ E b
⊢ ∃ i, (x, y) ∈ (fun z => U (↑z.snd) z.fst ×ˢ E z.fst) i
[PROOFSTEP]
rcases iUnion₂_eq_univ_iff.1 (hT b) x with ⟨a, ha, hx⟩
[GOAL]
case intro.intro.intro.intro.refine_1.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a✝ : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a✝ x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y b : Y
hb : y ∈ E b
a : X
ha : a ∈ T b
hx : x ∈ U a b
⊢ ∃ i, (x, y) ∈ (fun z => U (↑z.snd) z.fst ×ˢ E z.fst) i
[PROOFSTEP]
exact ⟨⟨b, a, ha⟩, hx, hb⟩
[GOAL]
case intro.intro.intro.intro.refine_2
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
⊢ ∃ t, t ∈ 𝓝 (x, y) ∧ Set.Finite {i | Set.Nonempty ((fun z => U (↑z.snd) z.fst ×ˢ E z.fst) i ∩ t)}
[PROOFSTEP]
rcases hEf y with ⟨t, ht, htf⟩
[GOAL]
case intro.intro.intro.intro.refine_2.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite {i | Set.Nonempty (E i ∩ t)}
⊢ ∃ t, t ∈ 𝓝 (x, y) ∧ Set.Finite {i | Set.Nonempty ((fun z => U (↑z.snd) z.fst ×ˢ E z.fst) i ∩ t)}
[PROOFSTEP]
refine ⟨univ ×ˢ t, prod_mem_nhds univ_mem ht, ?_⟩
[GOAL]
case intro.intro.intro.intro.refine_2.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite {i | Set.Nonempty (E i ∩ t)}
⊢ Set.Finite {i | Set.Nonempty ((fun z => U (↑z.snd) z.fst ×ˢ E z.fst) i ∩ univ ×ˢ t)}
[PROOFSTEP]
refine (htf.biUnion fun y _ ↦ finite_range (Sigma.mk y)).subset ?_
[GOAL]
case intro.intro.intro.intro.refine_2.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite {i | Set.Nonempty (E i ∩ t)}
⊢ {i | Set.Nonempty ((fun z => U (↑z.snd) z.fst ×ˢ E z.fst) i ∩ univ ×ˢ t)} ⊆
    ⋃ (i : Y) (_ : i ∈ {i | Set.Nonempty (E i ∩ t)}), range (Sigma.mk i)
[PROOFSTEP]
rintro ⟨b, a, ha⟩ ⟨⟨c, d⟩, ⟨-, hd : d ∈ E b⟩, -, hdt : d ∈ t⟩
[GOAL]
case intro.intro.intro.intro.refine_2.intro.intro.mk.mk.intro.mk.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a✝ : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a✝ x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : X × Y
x : X
y : Y
t : Set Y
ht : t ∈ 𝓝 y
htf : Set.Finite {i | Set.Nonempty (E i ∩ t)}
b : Y
a : X
ha : a ∈ T b
c : X
d : Y
hd : d ∈ E b
hdt : d ∈ t
⊢ { fst := b, snd := { val := a, property := ha } } ∈
    ⋃ (i : Y) (_ : i ∈ {i | Set.Nonempty (E i ∩ t)}), range (Sigma.mk i)
[PROOFSTEP]
exact mem_iUnion₂.2 ⟨b, ⟨d, hd, hdt⟩, mem_range_self _⟩
[GOAL]
case intro.intro.intro.intro.refine_3
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : (y : Y) × { x // x ∈ T y }
y : Y
x : X
hx : x ∈ T y
⊢ ∃ a, (fun z => U (↑z.snd) z.fst ×ˢ E z.fst) { fst := y, snd := { val := x, property := hx } } ⊆ s a
[PROOFSTEP]
refine ⟨a x y, (Set.prod_mono Subset.rfl ?_).trans (hUV x y)⟩
[GOAL]
case intro.intro.intro.intro.refine_3
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : ParacompactSpace Y
α : Type (max v w)
s : α → Set (X × Y)
ho : ∀ (a : α), IsOpen (s a)
hu : ⋃ (a : α), s a = univ
a : X → Y → α
U : X → Y → Set X
V : X → Y → Set Y
hUo : ∀ (x : X) (y : Y), IsOpen (U x y)
hVo : ∀ (x : X) (y : Y), IsOpen (V x y)
hxU : ∀ (x : X) (y : Y), x ∈ U x y
hyV : ∀ (x : X) (y : Y), y ∈ V x y
hUV : ∀ (x : X) (y : Y), U x y ×ˢ V x y ⊆ s (a x y)
T : Y → Finset X
hT : ∀ (y : Y), ⋃ (x : X) (_ : x ∈ T y), U x y = ⊤
W : Y → Set Y := fun y => ⋂ (x : X) (_ : x ∈ T y), V x y
hWo : ∀ (y : Y), IsOpen (W y)
hW : ∀ (y : Y), y ∈ W y
E : Y → Set Y
hEo : ∀ (a : Y), IsOpen (E a)
hE : ⋃ (i : Y), E i = univ
hEf : LocallyFinite E
hEA : ∀ (a : Y), E a ⊆ W a
x✝ : (y : Y) × { x // x ∈ T y }
y : Y
x : X
hx : x ∈ T y
⊢ E { fst := y, snd := { val := x, property := hx } }.fst ⊆ V x y
[PROOFSTEP]
exact (hEA _).trans (iInter₂_subset x hx)
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
⊢ ParacompactSpace X
[PROOFSTEP]
refine' ⟨fun ι s ho hu ↦ _⟩
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen (s a)
hu : ⋃ (a : ι), s a = univ
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
rcases isCompact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩
[GOAL]
case intro
ι✝ : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen (s a)
hu : ⋃ (a : ι), s a = univ
T : Finset ι
hT : univ ⊆ ⋃ (i : ι) (_ : i ∈ T), s i
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
refine' ⟨(T : Set ι), fun t ↦ s t, fun t ↦ ho _, _, locallyFinite_of_finite _, fun t ↦ ⟨t, Subset.rfl⟩⟩
[GOAL]
case intro
ι✝ : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
ι : Type v
s : ι → Set X
ho : ∀ (a : ι), IsOpen (s a)
hu : ⋃ (a : ι), s a = univ
T : Finset ι
hT : univ ⊆ ⋃ (i : ι) (_ : i ∈ T), s i
⊢ ⋃ (b : ↑↑T), (fun t => s ↑t) b = univ
[PROOFSTEP]
simpa only [iUnion_coe_set, ← univ_subset_iff]
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
classical
  -- For technical reasons we prepend two empty sets to the sequence `CompactExhaustion.choice X`
set K' : CompactExhaustion X := CompactExhaustion.choice X
set K : CompactExhaustion X := K'.shiftr.shiftr
set Kdiff := fun n ↦
  K (n + 1) \
    interior
      (K n)
        -- Now we restate some properties of `CompactExhaustion` for `K`/`Kdiff`
have hKcov : ∀ x, x ∈ Kdiff (K'.find x + 1) := by
  intro x
  simpa only [K'.find_shiftr] using diff_subset_diff_right interior_subset (K'.shiftr.mem_diff_shiftr_find x)
have Kdiffc : ∀ n, IsCompact (Kdiff n ∩ s) := fun n ↦ ((K.isCompact _).diff isOpen_interior).inter_right hs
have : ∀ (n) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 (x : X) := fun n x ↦
  IsOpen.mem_nhds (K.isClosed n).isOpen_compl fun hx' ↦ x.2.1.2 <| K.subset_interior_succ _ hx'
choose! r hrp hr using fun n (x : ↑(Kdiff (n + 1) ∩ s)) ↦ (hB x x.2.2).mem_iff.1 (this n x)
have hxr : ∀ (n x) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x := fun n x hx ↦
  (hB x hx.2).mem_of_mem (hrp _ ⟨x, hx⟩)
choose T hT using fun n ↦ (Kdiffc (n + 1)).elim_nhds_subcover' _ (hxr n)
set T' : ∀ n, Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ T n
refine' ⟨Σ n, T' n, fun a ↦ a.2, fun a ↦ r a.1 a.2, _, _, _⟩
· rintro ⟨n, x, hx⟩
  exact ⟨x.2.2, hrp _ _⟩
· refine' fun x hx ↦ mem_iUnion.2 _
  rcases mem_iUnion₂.1 (hT _ ⟨hKcov x, hx⟩) with ⟨⟨c, hc⟩, hcT, hcx⟩
  exact ⟨⟨_, ⟨c, hc⟩, hcT⟩, hcx⟩
· intro x
  refine' ⟨interior (K (K'.find x + 3)), IsOpen.mem_nhds isOpen_interior (K.subset_interior_succ _ (hKcov x).1), _⟩
  have : (⋃ k ≤ K'.find x + 2, range (Sigma.mk k) : Set (Σ n, T' n)).Finite :=
    (finite_le_nat _).biUnion fun k _ ↦ finite_range _
  apply this.subset
  rintro ⟨k, c, hc⟩
  simp only [mem_iUnion, mem_setOf_eq, mem_image, Subtype.coe_mk]
  rintro ⟨x, hxB : x ∈ B c (r k c), hxK⟩
  refine' ⟨k, _, ⟨c, hc⟩, rfl⟩
  have := (mem_compl_iff _ _).1 (hr k c hxB)
  contrapose! this with hnk
  exact K.subset hnk (interior_subset hxK)
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
set K' : CompactExhaustion X := CompactExhaustion.choice X
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
set K : CompactExhaustion X := K'.shiftr.shiftr
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
set Kdiff := fun n ↦
  K (n + 1) \
    interior
      (K n)
        -- Now we restate some properties of `CompactExhaustion` for `K`/`Kdiff`
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
have hKcov : ∀ x, x ∈ Kdiff (K'.find x + 1) := by
  intro x
  simpa only [K'.find_shiftr] using diff_subset_diff_right interior_subset (K'.shiftr.mem_diff_shiftr_find x)
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
⊢ ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
[PROOFSTEP]
intro x
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
x : X
⊢ x ∈ Kdiff (CompactExhaustion.find K' x + 1)
[PROOFSTEP]
simpa only [K'.find_shiftr] using diff_subset_diff_right interior_subset (K'.shiftr.mem_diff_shiftr_find x)
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
have Kdiffc : ∀ n, IsCompact (Kdiff n ∩ s) := fun n ↦ ((K.isCompact _).diff isOpen_interior).inter_right hs
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
have : ∀ (n) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 (x : X) := fun n x ↦
  IsOpen.mem_nhds (K.isClosed n).isOpen_compl fun hx' ↦ x.2.1.2 <| K.subset_interior_succ _ hx'
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
choose! r hrp hr using fun n (x : ↑(Kdiff (n + 1) ∩ s)) ↦ (hB x x.2.2).mem_iff.1 (this n x)
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
have hxr : ∀ (n x) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x := fun n x hx ↦
  (hB x hx.2).mem_of_mem (hrp _ ⟨x, hx⟩)
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
choose T hT using fun n ↦ (Kdiffc (n + 1)).elim_nhds_subcover' _ (hxr n)
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
set T' : ∀ n, Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ T n
[GOAL]
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
⊢ ∃ α c r, (∀ (a : α), c a ∈ s ∧ p (c a) (r a)) ∧ s ⊆ ⋃ (a : α), B (c a) (r a) ∧ LocallyFinite fun a => B (c a) (r a)
[PROOFSTEP]
refine' ⟨Σ n, T' n, fun a ↦ a.2, fun a ↦ r a.1 a.2, _, _, _⟩
[GOAL]
case refine'_1
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
⊢ ∀ (a : (n : ℕ) × ↑(T' n)), (fun a => ↑↑a.snd) a ∈ s ∧ p ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)
[PROOFSTEP]
rintro ⟨n, x, hx⟩
[GOAL]
case refine'_1.mk.mk
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
n : ℕ
x : ↑(Kdiff (n + 1) ∩ s)
hx : x ∈ T' n
⊢ (fun a => ↑↑a.snd) { fst := n, snd := { val := x, property := hx } } ∈ s ∧
    p ((fun a => ↑↑a.snd) { fst := n, snd := { val := x, property := hx } })
      ((fun a => r a.fst ↑a.snd) { fst := n, snd := { val := x, property := hx } })
[PROOFSTEP]
exact ⟨x.2.2, hrp _ _⟩
[GOAL]
case refine'_2
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
⊢ s ⊆ ⋃ (a : (n : ℕ) × ↑(T' n)), B ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)
[PROOFSTEP]
refine' fun x hx ↦ mem_iUnion.2 _
[GOAL]
case refine'_2
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
hx : x ∈ s
⊢ ∃ i, x ∈ B ((fun a => ↑↑a.snd) i) ((fun a => r a.fst ↑a.snd) i)
[PROOFSTEP]
rcases mem_iUnion₂.1 (hT _ ⟨hKcov x, hx⟩) with ⟨⟨c, hc⟩, hcT, hcx⟩
[GOAL]
case refine'_2.intro.mk.intro
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
hx : x ∈ s
c : X
hc : c ∈ Kdiff (CompactExhaustion.find K' x + 1) ∩ s
hcT : { val := c, property := hc } ∈ T (CompactExhaustion.find K' x)
hcx :
  x ∈
    B (↑{ val := c, property := hc })
      (r (CompactExhaustion.find K' x)
        { val := ↑{ val := c, property := hc },
          property := (_ : ↑{ val := c, property := hc } ∈ Kdiff (CompactExhaustion.find K' x + 1) ∩ s) })
⊢ ∃ i, x ∈ B ((fun a => ↑↑a.snd) i) ((fun a => r a.fst ↑a.snd) i)
[PROOFSTEP]
exact ⟨⟨_, ⟨c, hc⟩, hcT⟩, hcx⟩
[GOAL]
case refine'_3
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
⊢ LocallyFinite fun a => B ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)
[PROOFSTEP]
intro x
[GOAL]
case refine'_3
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun a => B ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)) i ∩ t)}
[PROOFSTEP]
refine' ⟨interior (K (K'.find x + 3)), IsOpen.mem_nhds isOpen_interior (K.subset_interior_succ _ (hKcov x).1), _⟩
[GOAL]
case refine'_3
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
⊢ Set.Finite
    {i |
      Set.Nonempty
        ((fun a => B ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)) i ∩
          interior (↑K (CompactExhaustion.find K' x + 3)))}
[PROOFSTEP]
have : (⋃ k ≤ K'.find x + 2, range (Sigma.mk k) : Set (Σ n, T' n)).Finite :=
  (finite_le_nat _).biUnion fun k _ ↦ finite_range _
[GOAL]
case refine'_3
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
this : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x + 2), range (Sigma.mk k))
⊢ Set.Finite
    {i |
      Set.Nonempty
        ((fun a => B ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)) i ∩
          interior (↑K (CompactExhaustion.find K' x + 3)))}
[PROOFSTEP]
apply this.subset
[GOAL]
case refine'_3
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
this : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x + 2), range (Sigma.mk k))
⊢ {i |
      Set.Nonempty
        ((fun a => B ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)) i ∩
          interior (↑K (CompactExhaustion.find K' x + 3)))} ⊆
    ⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x + 2), range (Sigma.mk k)
[PROOFSTEP]
rintro ⟨k, c, hc⟩
[GOAL]
case refine'_3.mk.mk
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
this : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x + 2), range (Sigma.mk k))
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
⊢ { fst := k, snd := { val := c, property := hc } } ∈
      {i |
        Set.Nonempty
          ((fun a => B ((fun a => ↑↑a.snd) a) ((fun a => r a.fst ↑a.snd) a)) i ∩
            interior (↑K (CompactExhaustion.find K' x + 3)))} →
    { fst := k, snd := { val := c, property := hc } } ∈
      ⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x + 2), range (Sigma.mk k)
[PROOFSTEP]
simp only [mem_iUnion, mem_setOf_eq, mem_image, Subtype.coe_mk]
[GOAL]
case refine'_3.mk.mk
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x : X
this : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x + 2), range (Sigma.mk k))
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
⊢ Set.Nonempty
      (B (↑c) (r k c) ∩
        interior
          (↑(CompactExhaustion.shiftr (CompactExhaustion.shiftr (CompactExhaustion.choice X)))
            (CompactExhaustion.find (CompactExhaustion.choice X) x + 3))) →
    ∃ i i_1, { fst := k, snd := { val := c, property := hc } } ∈ range (Sigma.mk i)
[PROOFSTEP]
rintro ⟨x, hxB : x ∈ B c (r k c), hxK⟩
[GOAL]
case refine'_3.mk.mk.intro.intro
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x✝ : X
this : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x✝ + 2), range (Sigma.mk k))
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
x : X
hxB : x ∈ B (↑c) (r k c)
hxK :
  x ∈
    interior
      (↑(CompactExhaustion.shiftr (CompactExhaustion.shiftr (CompactExhaustion.choice X)))
        (CompactExhaustion.find (CompactExhaustion.choice X) x✝ + 3))
⊢ ∃ i i_1, { fst := k, snd := { val := c, property := hc } } ∈ range (Sigma.mk i)
[PROOFSTEP]
refine' ⟨k, _, ⟨c, hc⟩, rfl⟩
[GOAL]
case refine'_3.mk.mk.intro.intro
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x✝ : X
this : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x✝ + 2), range (Sigma.mk k))
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
x : X
hxB : x ∈ B (↑c) (r k c)
hxK :
  x ∈
    interior
      (↑(CompactExhaustion.shiftr (CompactExhaustion.shiftr (CompactExhaustion.choice X)))
        (CompactExhaustion.find (CompactExhaustion.choice X) x✝ + 3))
⊢ k ≤ CompactExhaustion.find (CompactExhaustion.choice X) x✝ + 2
[PROOFSTEP]
have := (mem_compl_iff _ _).1 (hr k c hxB)
[GOAL]
case refine'_3.mk.mk.intro.intro
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝¹ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x✝ : X
this✝ : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x✝ + 2), range (Sigma.mk k))
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
x : X
hxB : x ∈ B (↑c) (r k c)
hxK :
  x ∈
    interior
      (↑(CompactExhaustion.shiftr (CompactExhaustion.shiftr (CompactExhaustion.choice X)))
        (CompactExhaustion.find (CompactExhaustion.choice X) x✝ + 3))
this : ¬x ∈ ↑K k
⊢ k ≤ CompactExhaustion.find (CompactExhaustion.choice X) x✝ + 2
[PROOFSTEP]
contrapose! this with hnk
[GOAL]
case refine'_3.mk.mk.intro.intro
ι✝ : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed s
hB : ∀ (x : X), x ∈ s → HasBasis (𝓝 x) (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := CompactExhaustion.shiftr (CompactExhaustion.shiftr K')
Kdiff : (n : ℕ) → (fun x => Set X) (n + 1) := fun n => ↑K (n + 1) \ interior (↑K n)
hKcov : ∀ (x : X), x ∈ Kdiff (CompactExhaustion.find K' x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (↑K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (↑K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n { val := x, property := hx }) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT :
  ∀ (n : ℕ),
    Kdiff (n + 1) ∩ s ⊆
      ⋃ (x : ↑(Kdiff (n + 1) ∩ s)) (_ : x ∈ T n), B (↑x) (r n { val := ↑x, property := (_ : ↑x ∈ Kdiff (n + 1) ∩ s) })
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n => ↑(T n)
x✝ : X
this : Set.Finite (⋃ (k : ℕ) (_ : k ≤ CompactExhaustion.find K' x✝ + 2), range (Sigma.mk k))
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
x : X
hxB : x ∈ B (↑c) (r k c)
hxK :
  x ∈
    interior
      (↑(CompactExhaustion.shiftr (CompactExhaustion.shiftr (CompactExhaustion.choice X)))
        (CompactExhaustion.find (CompactExhaustion.choice X) x✝ + 3))
hnk : CompactExhaustion.find (CompactExhaustion.choice X) x✝ + 2 < k
⊢ x ∈ ↑(CompactExhaustion.shiftr (CompactExhaustion.shiftr K')) k
[PROOFSTEP]
exact K.subset hnk (interior_subset hxK)
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
⊢ ParacompactSpace X
[PROOFSTEP]
refine' ⟨fun α s ho hc ↦ _⟩
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hc : ⋃ (a : α), s a = univ
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
choose i hi using iUnion_eq_univ_iff.1 hc
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hc : ⋃ (a : α), s a = univ
i : X → α
hi : ∀ (x : X), x ∈ s (i x)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have : ∀ x : X, (𝓝 x).HasBasis (fun t : Set X ↦ (x ∈ t ∧ IsOpen t) ∧ t ⊆ s (i x)) id := fun x : X ↦
  (nhds_basis_opens x).restrict_subset (IsOpen.mem_nhds (ho (i x)) (hi x))
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hc : ⋃ (a : α), s a = univ
i : X → α
hi : ∀ (x : X), x ∈ s (i x)
this : ∀ (x : X), HasBasis (𝓝 x) (fun t => (x ∈ t ∧ IsOpen t) ∧ t ⊆ s (i x)) id
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis this with ⟨β, c, t, hto, htc, htf⟩
[GOAL]
case intro.intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : LocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hc : ⋃ (a : α), s a = univ
i : X → α
hi : ∀ (x : X), x ∈ s (i x)
this : ∀ (x : X), HasBasis (𝓝 x) (fun t => (x ∈ t ∧ IsOpen t) ∧ t ⊆ s (i x)) id
β : Type v
c : β → X
t : β → Set X
hto : ∀ (a : β), (c a ∈ t a ∧ IsOpen (t a)) ∧ t a ⊆ s (i (c a))
htc : ⋃ (a : β), id (t a) = univ
htf : LocallyFinite fun a => id (t a)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
exact ⟨β, t, fun x ↦ (hto x).1.2, htc, htf, fun b ↦ ⟨i <| c b, (hto b).2⟩⟩
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
⊢ NormalSpace X
[PROOFSTEP]
have :
  ∀ s t : Set X,
    IsClosed s →
      IsClosed t →
        (∀ x ∈ s, ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
          ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v :=
  by
  /- For each `x ∈ s` we choose open disjoint `u x ∋ x` and `v x ⊇ t`. The sets `u x` form an
          open covering of `s`. We choose a locally finite refinement `u' : s → Set X`, then
          `⋃ i, u' i` and `(closure (⋃ i, u' i))ᶜ` are disjoint open neighborhoods of `s` and `t`. -/
  intro s t hs _ H
  choose u v hu hv hxu htv huv using SetCoe.forall'.1 H
  rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with ⟨u', hu'o, hcov', hu'fin, hsub⟩
  refine'
    ⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, isOpen_iUnion hu'o, isClosed_closure.isOpen_compl, hcov', _,
      disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩
  rw [hu'fin.closure_iUnion, compl_iUnion, subset_iInter_iff]
  refine' fun i x hxt hxu ↦ absurd (htv i hxt) (closure_minimal _ (isClosed_compl_iff.2 <| hv _) hxu)
  exact fun y hyu hyv ↦
    (huv i).le_bot
      ⟨hsub _ hyu, hyv⟩
        -- Now we apply the lemma twice: first to `s` and `t`, then to `t` and each point of `s`.
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
⊢ ∀ (s t : Set X),
    IsClosed s →
      IsClosed t →
        (∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
          ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
intro s t hs _ H
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed s
a✝ : IsClosed t
H : ∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
choose u v hu hv hxu htv huv using SetCoe.forall'.1 H
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed s
a✝ : IsClosed t
H : ∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : ↑s → Set X
hu : ∀ (x : ↑s), IsOpen (u x)
hv : ∀ (x : ↑s), IsOpen (v x)
hxu : ∀ (x : ↑s), ↑x ∈ u x
htv : ∀ (x : ↑s), t ⊆ v x
huv : ∀ (x : ↑s), Disjoint (u x) (v x)
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with ⟨u', hu'o, hcov', hu'fin, hsub⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed s
a✝ : IsClosed t
H : ∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : ↑s → Set X
hu : ∀ (x : ↑s), IsOpen (u x)
hv : ∀ (x : ↑s), IsOpen (v x)
hxu : ∀ (x : ↑s), ↑x ∈ u x
htv : ∀ (x : ↑s), t ⊆ v x
huv : ∀ (x : ↑s), Disjoint (u x) (v x)
u' : ↑s → Set X
hu'o : ∀ (i : ↑s), IsOpen (u' i)
hcov' : s ⊆ ⋃ (i : ↑s), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : ↑s), u' i ⊆ u i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
refine'
  ⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, isOpen_iUnion hu'o, isClosed_closure.isOpen_compl, hcov', _,
    disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed s
a✝ : IsClosed t
H : ∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : ↑s → Set X
hu : ∀ (x : ↑s), IsOpen (u x)
hv : ∀ (x : ↑s), IsOpen (v x)
hxu : ∀ (x : ↑s), ↑x ∈ u x
htv : ∀ (x : ↑s), t ⊆ v x
huv : ∀ (x : ↑s), Disjoint (u x) (v x)
u' : ↑s → Set X
hu'o : ∀ (i : ↑s), IsOpen (u' i)
hcov' : s ⊆ ⋃ (i : ↑s), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : ↑s), u' i ⊆ u i
⊢ t ⊆ (closure (⋃ (i : ↑s), u' i))ᶜ
[PROOFSTEP]
rw [hu'fin.closure_iUnion, compl_iUnion, subset_iInter_iff]
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed s
a✝ : IsClosed t
H : ∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : ↑s → Set X
hu : ∀ (x : ↑s), IsOpen (u x)
hv : ∀ (x : ↑s), IsOpen (v x)
hxu : ∀ (x : ↑s), ↑x ∈ u x
htv : ∀ (x : ↑s), t ⊆ v x
huv : ∀ (x : ↑s), Disjoint (u x) (v x)
u' : ↑s → Set X
hu'o : ∀ (i : ↑s), IsOpen (u' i)
hcov' : s ⊆ ⋃ (i : ↑s), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : ↑s), u' i ⊆ u i
⊢ ∀ (i : ↑s), t ⊆ (closure (u' i))ᶜ
[PROOFSTEP]
refine' fun i x hxt hxu ↦ absurd (htv i hxt) (closure_minimal _ (isClosed_compl_iff.2 <| hv _) hxu)
[GOAL]
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
s t : Set X
hs : IsClosed s
a✝ : IsClosed t
H : ∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
u v : ↑s → Set X
hu : ∀ (x : ↑s), IsOpen (u x)
hv : ∀ (x : ↑s), IsOpen (v x)
hxu✝ : ∀ (x : ↑s), ↑x ∈ u x
htv : ∀ (x : ↑s), t ⊆ v x
huv : ∀ (x : ↑s), Disjoint (u x) (v x)
u' : ↑s → Set X
hu'o : ∀ (i : ↑s), IsOpen (u' i)
hcov' : s ⊆ ⋃ (i : ↑s), u' i
hu'fin : LocallyFinite u'
hsub : ∀ (i : ↑s), u' i ⊆ u i
i : ↑s
x : X
hxt : x ∈ t
hxu : x ∈ closure (u' i)
⊢ u' i ⊆ (v i)ᶜ
[PROOFSTEP]
exact fun y hyu hyv ↦
  (huv i).le_bot
    ⟨hsub _ hyu, hyv⟩
      -- Now we apply the lemma twice: first to `s` and `t`, then to `t` and each point of `s`.
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed s →
      IsClosed t →
        (∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
          ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
⊢ NormalSpace X
[PROOFSTEP]
refine' ⟨fun s t hs ht hst ↦ this s t hs ht fun x hx ↦ _⟩
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed s →
      IsClosed t →
        (∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
          ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
s t : Set X
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
x : X
hx : x ∈ s
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
rcases this t { x } ht isClosed_singleton fun y hy ↦
    (by
      simp_rw [singleton_subset_iff]
      exact t2_separation (hst.symm.ne_of_mem hy hx)) with
  ⟨v, u, hv, hu, htv, hxu, huv⟩
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed s →
      IsClosed t →
        (∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
          ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
s t : Set X
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
x : X
hx : x ∈ s
y : X
hy : y ∈ t
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ y ∈ u ∧ {x} ⊆ v ∧ Disjoint u v
[PROOFSTEP]
simp_rw [singleton_subset_iff]
[GOAL]
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed s →
      IsClosed t →
        (∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
          ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
s t : Set X
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
x : X
hx : x ∈ s
y : X
hy : y ∈ t
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ y ∈ u ∧ x ∈ v ∧ Disjoint u v
[PROOFSTEP]
exact t2_separation (hst.symm.ne_of_mem hy hx)
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space X
inst✝ : ParacompactSpace X
this :
  ∀ (s t : Set X),
    IsClosed s →
      IsClosed t →
        (∀ (x : X), x ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
          ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
s t : Set X
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
x : X
hx : x ∈ s
v u : Set X
hv : IsOpen v
hu : IsOpen u
htv : t ⊆ v
hxu : {x} ⊆ u
huv : Disjoint v u
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
exact ⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩
