case intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
case intro.intro.intro.refine'_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s ⊆ s

case intro.intro.intro.refine'_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ Set.Countable ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)

case intro.intro.intro.refine'_3
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ Dense ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)

case intro.intro.intro.refine'_4
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s

case intro.intro.intro.refine'_5
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s
case intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
refine' ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, _, _, _, _, _⟩
no goals
case intro.intro.intro.refine'_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s ⊆ s

case intro.intro.intro.refine'_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ Set.Countable ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)

case intro.intro.intro.refine'_3
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ Dense ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)

case intro.intro.intro.refine'_4
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s

case intro.intro.intro.refine'_5
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s
exacts [inter_subset_right _ _,
  (htc.union ((countable_isBot α).union (countable_isTop α))).mono (inter_subset_left _ _),
  htd.mono (subset_inter (subset_union_left _ _) hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩,
  fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩]