case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ ∃ D, Perfect D ∧ Set.Nonempty D ∧ D ⊆ C
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
⊢ ∃ D, Perfect D ∧ Set.Nonempty D ∧ D ⊆ C
rcases exists_countable_union_perfect_of_isClosed hclosed with ⟨V, D, Vct, Dperf, VD⟩
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ Set.Nonempty D ∧ D ⊆ C
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ ∃ D, Perfect D ∧ Set.Nonempty D ∧ D ⊆ C
refine' ⟨D, ⟨Dperf, _⟩⟩
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ Set.Nonempty D

case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ Set.Nonempty D ∧ D ⊆ C
constructor
case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D
case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C
rw [VD]
no goals
case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D
exact subset_union_right _ _
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ≠ ∅
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ Set.Nonempty D
rw [nonempty_iff_ne_empty]
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
⊢ False
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ≠ ∅
by_contra h
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
⊢ False
rw [h, union_empty] at VD
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
V : Set α
hunc : ¬Set.Countable V
D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬Set.Countable C
V D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
rw [VD] at hunc
no goals
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
V : Set α
hunc : ¬Set.Countable V
D : Set α
Vct : Set.Countable V
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False
contradiction