-- Mathlib/Topology/Perfect.lean
theorem exists_perfect_nonempty_of_isClosed_of_not_countable [SecondCountableTopology α]
    (hclosed : IsClosed C) (hunc : ¬C.Countable) : ∃ D : Set α, Perfect D ∧ D.Nonempty ∧ D ⊆ C

Proof state:
case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D

Tactic:
exact subset_union_right

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ ∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C

Tactic:
refine ⟨D, ⟨Dperf, ?_⟩⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty ∧ D ⊆ C

Proof state:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Result:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ≠ ∅

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
⊢ ∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C

Tactic:
rcases exists_countable_union_perfect_of_isClosed hclosed with ⟨V, D, Vct, Dperf, VD⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ ∃ D, Perfect D ∧ D.Nonempty ∧ D ⊆ C

Proof state:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
V : Set α
hunc : ¬V.Countable
D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C

Tactic:
rw [VD]

Result:
case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ V ∪ D

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty ∧ D ⊆ C

Tactic:
constructor

Result:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D.Nonempty

case intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ⊆ C

Proof state:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
⊢ False

Tactic:
rw [h, union_empty] at VD

Result:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Proof state:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Tactic:
rw [VD] at hunc

Result:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
V : Set α
hunc : ¬V.Countable
D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V
h : D = ∅
⊢ False

Proof state:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
⊢ D ≠ ∅

Tactic:
by_contra h

Result:
case intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
hunc : ¬C.Countable
V D : Set α
Vct : V.Countable
Dperf : Perfect D
VD : C = V ∪ D
h : D = ∅
⊢ False