case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
hnonempty : Set.Nonempty C
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
cases' hnonempty with y yC
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
obtain ⟨x, xC, hxy⟩ : ∃ x ∈ C, x ≠ y := by
  have := hC.acc _ yC
  rw [accPt_iff_nhds] at this
  rcases this univ univ_mem with ⟨x, xC, hxy⟩
  exact ⟨x, xC.2, hxy⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
obtain ⟨U, xU, Uop, V, yV, Vop, hUV⟩ := exists_open_nhds_disjoint_closure hxy
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ (Perfect (closure (U ∩ C)) ∧ Set.Nonempty (closure (U ∩ C)) ∧ closure (U ∩ C) ⊆ C) ∧
    (Perfect (closure (V ∩ C)) ∧ Set.Nonempty (closure (V ∩ C)) ∧ closure (V ∩ C) ⊆ C) ∧
      Disjoint (closure (U ∩ C)) (closure (V ∩ C))
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ ∃ C₀ C₁, (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁
use closure (U ∩ C), closure (V ∩ C)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ (Perfect (closure (U ∩ C)) ∧ Set.Nonempty (closure (U ∩ C))) ∧ closure (U ∩ C) ⊆ C

case intro.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ ((Perfect (closure (V ∩ C)) ∧ Set.Nonempty (closure (V ∩ C))) ∧ closure (V ∩ C) ⊆ C) ∧
    Disjoint (closure (U ∩ C)) (closure (V ∩ C))
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ (Perfect (closure (U ∩ C)) ∧ Set.Nonempty (closure (U ∩ C)) ∧ closure (U ∩ C) ⊆ C) ∧
    (Perfect (closure (V ∩ C)) ∧ Set.Nonempty (closure (V ∩ C)) ∧ closure (V ∩ C) ⊆ C) ∧
      Disjoint (closure (U ∩ C)) (closure (V ∩ C))
constructor <;> rw [← and_assoc]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ (Perfect (closure (V ∩ C)) ∧ Set.Nonempty (closure (V ∩ C))) ∧ closure (V ∩ C) ⊆ C

case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ Disjoint (closure (U ∩ C)) (closure (V ∩ C))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ ((Perfect (closure (V ∩ C)) ∧ Set.Nonempty (closure (V ∩ C))) ∧ closure (V ∩ C) ⊆ C) ∧
    Disjoint (closure (U ∩ C)) (closure (V ∩ C))
constructor
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.right
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ Disjoint (closure (U ∩ C)) (closure (V ∩ C))
apply Disjoint.mono _ _ hUV <;> apply closure_mono <;> exact inter_subset_left _ _
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : AccPt y (𝓟 C)
⊢ ∃ x, x ∈ C ∧ x ≠ y
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
⊢ ∃ x, x ∈ C ∧ x ≠ y
have := hC.acc _ yC
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ (U : Set α), U ∈ 𝓝 y → ∃ y_1, y_1 ∈ U ∩ C ∧ y_1 ≠ y
⊢ ∃ x, x ∈ C ∧ x ≠ y
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : AccPt y (𝓟 C)
⊢ ∃ x, x ∈ C ∧ x ≠ y
rw [accPt_iff_nhds] at this
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ (U : Set α), U ∈ 𝓝 y → ∃ y_1, y_1 ∈ U ∩ C ∧ y_1 ≠ y
x : α
xC : x ∈ univ ∩ C
hxy : x ≠ y
⊢ ∃ x, x ∈ C ∧ x ≠ y
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ (U : Set α), U ∈ 𝓝 y → ∃ y_1, y_1 ∈ U ∩ C ∧ y_1 ≠ y
⊢ ∃ x, x ∈ C ∧ x ≠ y
rcases this univ univ_mem with ⟨x, xC, hxy⟩
no goals
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
this : ∀ (U : Set α), U ∈ 𝓝 y → ∃ y_1, y_1 ∈ U ∩ C ∧ y_1 ≠ y
x : α
xC : x ∈ univ ∩ C
hxy : x ≠ y
⊢ ∃ x, x ∈ C ∧ x ≠ y
exact ⟨x, xC.2, hxy⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ closure (U ∩ C) ⊆ C
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ (Perfect (closure (U ∩ C)) ∧ Set.Nonempty (closure (U ∩ C))) ∧ closure (U ∩ C) ⊆ C
refine' ⟨hC.closure_nhds_inter x xC xU Uop, _⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ U ∩ C ⊆ C
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ closure (U ∩ C) ⊆ C
rw [hC.closed.closure_subset_iff]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ U ∩ C ⊆ C
exact inter_subset_right _ _
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ closure (V ∩ C) ⊆ C
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ (Perfect (closure (V ∩ C)) ∧ Set.Nonempty (closure (V ∩ C))) ∧ closure (V ∩ C) ⊆ C
refine' ⟨hC.closure_nhds_inter y yC yV Vop, _⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ V ∩ C ⊆ C
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ closure (V ∩ C) ⊆ C
rw [hC.closed.closure_subset_iff]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.right.left
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T25Space α
hC : Perfect C
y : α
yC : y ∈ C
x : α
xC : x ∈ C
hxy : x ≠ y
U : Set α
xU : x ∈ U
Uop : IsOpen U
V : Set α
yV : y ∈ V
Vop : IsOpen V
hUV : Disjoint (closure U) (closure V)
⊢ V ∩ C ⊆ C
exact inter_subset_right _ _